:: On Rough Subgroup of a Group :: by Xiquan Liang and Dailu Li :: :: Received August 7, 2009 :: Copyright (c) 2009-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies GROUP_1, XBOOLE_0, SUBSET_1, GROUP_2, PRE_TOPC, RELAT_1, TARSKI, STRUCT_0; notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4; constructors REALSET2, GROUP_4; registrations XBOOLE_0, STRUCT_0, GROUP_1, GROUP_2, GROUP_3; requirements SUBSET, BOOLE; begin :: Preliminaries reserve G for Group; reserve A,B for non empty Subset of G; reserve N,H,H1,H2 for Subgroup of G; reserve x,a,b for Element of G; theorem :: GROUP_11:1 for N be normal Subgroup of G,x1,x2 be Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N; theorem :: GROUP_11:2 for G being Group,N being Subgroup of G, x, y being Element of G st y in x * N holds x * N = y * N; theorem :: GROUP_11:3 for N being Subgroup of G,H being Subgroup of G, x being Element of G st x * N meets carr(H) ex y being Element of G st y in x * N & y in H; theorem :: GROUP_11:4 for x,y being Element of G, N be normal Subgroup of G st y in N holds x * y * x" in N; theorem :: GROUP_11:5 for N be Subgroup of G st for x,y being Element of G st y in N holds x * y * x" in N holds N is normal; theorem :: GROUP_11:6 x in H1 * H2 iff ex a,b st x = a * b & a in H1 & b in H2; theorem :: GROUP_11:7 for G being Group, N1,N2 being strict normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N1 * N2; theorem :: GROUP_11:8 for G being Group, N1,N2 being strict normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N1 * N2; theorem :: GROUP_11:9 for G being Group, N,N1,N2 being Subgroup of G st the carrier of N = N1 * N2 holds N1 is Subgroup of N & N2 is Subgroup of N; theorem :: GROUP_11:10 for N,N1,N2 be normal Subgroup of G,a,b be Element of G st the carrier of N = N1 * N2 holds (a * N1) * (b * N2) = (a * b) * N; theorem :: GROUP_11:11 for N being normal Subgroup of G for x holds x * N * x" c= carr(N); definition let G be Group, A be Subset of G; let N be Subgroup of G; func N ` A -> Subset of G equals :: GROUP_11:def 1 {x where x is Element of G: x * N c= A}; func N ~ A -> Subset of G equals :: GROUP_11:def 2 {x where x is Element of G : x * N meets A}; end; theorem :: GROUP_11:12 for x being Element of G st x in N ` A holds x * N c= A; theorem :: GROUP_11:13 for x being Element of G st x * N c= A holds x in N ` A; theorem :: GROUP_11:14 for x being Element of G st x in N ~ A holds x * N meets A; theorem :: GROUP_11:15 for x being Element of G st x * N meets A holds x in N ~ A; theorem :: GROUP_11:16 N ` A c= A; theorem :: GROUP_11:17 A c= N ~ A; theorem :: GROUP_11:18 N ` A c= N ~ A; theorem :: GROUP_11:19 N ~ (A \/ B) = N ~ A \/ N ~ B; theorem :: GROUP_11:20 N ` (A /\ B) = N ` A /\ N ` B; theorem :: GROUP_11:21 A c= B implies N ` A c= N ` B; theorem :: GROUP_11:22 A c= B implies N ~ A c= N ~ B; theorem :: GROUP_11:23 N ` A \/ N ` B c= N ` (A \/ B); theorem :: GROUP_11:24 N ~ (A \/ B)= N ~ A \/ N ~ B; theorem :: GROUP_11:25 N is Subgroup of H implies H ` A c= N ` A; theorem :: GROUP_11:26 N is Subgroup of H implies N ~ A c= H ~ A; theorem :: GROUP_11:27 for G be Group, A,B be non empty Subset of G, N be normal Subgroup of G holds N ` A * N ` B c= N ` (A * B); theorem :: GROUP_11:28 for x being Element of G st x in N ~ (A * B) holds x * N meets A * B; theorem :: GROUP_11:29 for G be Group, A,B be non empty Subset of G, N be normal Subgroup of G holds N ~ A * N ~ B = N ~ (A * B); theorem :: GROUP_11:30 for x being Element of G st x in N ~ (N ` (N ~ A)) holds x * N meets N ` (N ~ A); theorem :: GROUP_11:31 for x being Element of G st x in N ` (N ~ A) holds x * N c= N ~ A; theorem :: GROUP_11:32 for x being Element of G st x in N ~ (N ~ A) holds x * N meets N ~ A; theorem :: GROUP_11:33 for x being Element of G st x in N ~ (N ` A) holds x * N meets N ` A; theorem :: GROUP_11:34 N ` (N ` A) = N ` A; theorem :: GROUP_11:35 N ~ A = N ~ (N ~ A); theorem :: GROUP_11:36 N ` (N ` A) c= N ~ (N ~ A); theorem :: GROUP_11:37 N ~ (N ` A) c= A; theorem :: GROUP_11:38 N ` (N ~ (N ` A)) = N ` A; theorem :: GROUP_11:39 A c= N ` (N ~ A) implies N ~ A c= N ~ (N `(N ~ A)); theorem :: GROUP_11:40 N ~ (N `(N ~ A)) = N ~ A; theorem :: GROUP_11:41 for x being Element of G st x in N ` (N ` A) holds x * N c= N ` A; theorem :: GROUP_11:42 N `(N ` A) = N ~ (N ` A); theorem :: GROUP_11:43 N ~ (N ~ A) = N `(N ~ A); theorem :: GROUP_11:44 for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N ~ A c= N1 ~ A /\ N2 ~ A; theorem :: GROUP_11:45 for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N1 ` A /\ N2 ` A c= N ` A; theorem :: GROUP_11:46 for N1,N2 be strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 & N ` A c= N1 ` A /\ N2 ` A; theorem :: GROUP_11:47 for N1,N2 be strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 & N1 ~ A \/ N2 ~ A c= N ~ A; theorem :: GROUP_11:48 for N1,N2 be strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1); reserve N1,N2 for Subgroup of G; definition let G be Group, H, N be Subgroup of G; func N ` H -> Subset of G equals :: GROUP_11:def 3 {x where x is Element of G: x * N c= carr(H)}; func N ~ H -> Subset of G equals :: GROUP_11:def 4 {x where x is Element of G : x * N meets carr(H)}; end; theorem :: GROUP_11:49 for x being Element of G st x in N ` H holds x * N c= carr(H); theorem :: GROUP_11:50 for x being Element of G st x * N c= carr(H) holds x in N ` H; theorem :: GROUP_11:51 for x being Element of G st x in N ~ H holds x * N meets carr(H); theorem :: GROUP_11:52 for x being Element of G st x * N meets carr(H) holds x in N ~ H; theorem :: GROUP_11:53 N ` H c= carr(H); theorem :: GROUP_11:54 carr(H) c= N ~ H; theorem :: GROUP_11:55 N ` H c= N ~ H; theorem :: GROUP_11:56 H1 is Subgroup of H2 implies N ~ H1 c= N ~ H2; theorem :: GROUP_11:57 N1 is Subgroup of N2 implies N1 ~ H c= N2 ~ H; theorem :: GROUP_11:58 N1 is Subgroup of N2 implies N1 ~ N1 c= N2 ~ N2; theorem :: GROUP_11:59 H1 is Subgroup of H2 implies N ` H1 c= N ` H2; theorem :: GROUP_11:60 N1 is Subgroup of N2 implies N2 ` H c= N1 ` H; theorem :: GROUP_11:61 N1 is Subgroup of N2 implies N2 ` N1 c= N1 ` N2; theorem :: GROUP_11:62 for N be normal Subgroup of G holds N ` H1 * N ` H2 c= N ` (H1 * H2); theorem :: GROUP_11:63 for N be normal Subgroup of G holds N ~ H1 * N ~ H2 = N ~ (H1 * H2); theorem :: GROUP_11:64 for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N ~ H c= N1 ~ H /\ N2 ~ H; theorem :: GROUP_11:65 for N,N1,N2 be Subgroup of G st N = N1 /\ N2 holds N1 ` H /\ N2 ` H c= N ` H; theorem :: GROUP_11:66 for N1,N2 be strict normal Subgroup of G holds ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 & N ` H c= N1 ` H /\ N2 ` H; theorem :: GROUP_11:67 for N1,N2 be strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 & N1 ~ H \/ N2 ~ H c= N ~ H; theorem :: GROUP_11:68 for N1,N2 be strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 & N1 ` H * N2 ` H c= N ` H; theorem :: GROUP_11:69 for N1,N2 be strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 & N1 ~ H * N2 ~ H c= N ~ H; theorem :: GROUP_11:70 for N1,N2 be strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1); theorem :: GROUP_11:71 for H being Subgroup of G, N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H; theorem :: GROUP_11:72 for H being Subgroup of G, N being normal Subgroup of G st N is Subgroup of H ex M being strict Subgroup of G st the carrier of M = N ` H; theorem :: GROUP_11:73 for H,N be normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N ~ H; theorem :: GROUP_11:74 for H,N being normal Subgroup of G st N is Subgroup of H ex M being strict normal Subgroup of G st the carrier of M = N ` H; theorem :: GROUP_11:75 for N,N1 be normal Subgroup of G st N1 is Subgroup of N ex N2,N3 being strict normal Subgroup of G st the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N; theorem :: GROUP_11:76 for N,N1 be normal Subgroup of G st N1 is Subgroup of N ex N2,N3 being strict normal Subgroup of G st the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ~ N c= N2 ~ N; theorem :: GROUP_11:77 for N,N1 be normal Subgroup of G st N1 is Subgroup of N ex N2,N3 being strict normal Subgroup of G st the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ~ N; theorem :: GROUP_11:78 for N,N1 be normal Subgroup of G st N1 is Subgroup of N ex N2,N3 being strict normal Subgroup of G st the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ` N c= N2 ~ N; theorem :: GROUP_11:79 for N,N1,N2 be normal Subgroup of G st N1 is Subgroup of N2 ex N3,N4 being strict normal Subgroup of G st the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1; theorem :: GROUP_11:80 for N,N1 be normal Subgroup of G ex N2 being strict normal Subgroup of G st the carrier of N2 = N ` N & N ` N1 c= N2 ` N1; theorem :: GROUP_11:81 for N,N1 be normal Subgroup of G ex N2 being strict normal Subgroup of G st the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1;