:: Classes of Conjugation. Normal Subgroups :: by Wojciech A. Trybulec :: :: Received August 10, 1990 :: Copyright (c) 1990-2019 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, SUBSET_1, GROUP_2, NAT_1, INT_1, RELAT_1, BINOP_1, ALGSTR_0, FUNCT_1, STRUCT_0, TARSKI, ZFMISC_1, XBOOLE_0, FINSET_1, CARD_1, NEWTON, ARYTM_3, XXREAL_0, COMPLEX1, RLSUB_1, CQC_SIM1, SETFAM_1, PRE_TOPC, GROUP_3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, CARD_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, DOMAIN_1, XXREAL_0, INT_1, INT_2; constructors SETFAM_1, WELLORD2, BINOP_1, XXREAL_0, NAT_1, INT_2, REALSET1, REAL_1, GROUP_2, RELSET_1, BINOP_2, NUMBERS; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0, INT_1, STRUCT_0, GROUP_1, GROUP_2, ORDINAL1; requirements NUMERALS, SUBSET, BOOLE; begin reserve x,y,y1,y2 for set; reserve G for Group; reserve a,b,c,d,g,h for Element of G; reserve A,B,C,D for Subset of G; reserve H,H1,H2,H3 for Subgroup of G; reserve n for Nat; reserve i for Integer; theorem :: GROUP_3:1 a * b * b" = a & a * b" * b = a & b" * b * a = a & b * b" * a = a & a * (b * b") = a & a * (b" * b) = a & b" * (b * a) = a & b * (b" * a) = a; theorem :: GROUP_3:2 G is commutative Group iff the multF of G is commutative; theorem :: GROUP_3:3 (1).G is commutative; theorem :: GROUP_3:4 A c= B & C c= D implies A * C c= B * D; theorem :: GROUP_3:5 A c= B implies a * A c= a * B & A * a c= B * a; theorem :: GROUP_3:6 H1 is Subgroup of H2 implies a * H1 c= a * H2 & H1 * a c= H2 * a; theorem :: GROUP_3:7 a * H = {a} * H; theorem :: GROUP_3:8 H * a = H * {a}; theorem :: GROUP_3:9 A * a * H = A * (a * H); theorem :: GROUP_3:10 a * H * A = a * (H * A); theorem :: GROUP_3:11 A * H * a = A * (H * a); theorem :: GROUP_3:12 H * a * A = H * (a * A); theorem :: GROUP_3:13 H1 * a * H2 = H1 * (a * H2); definition let G; func Subgroups G -> set means :: GROUP_3:def 1 for x being object holds x in it iff x is strict Subgroup of G; end; registration let G; cluster Subgroups G -> non empty; end; theorem :: GROUP_3:14 for G being strict Group holds G in Subgroups G; theorem :: GROUP_3:15 G is finite implies Subgroups G is finite; definition let G,a,b; func a |^ b -> Element of G equals :: GROUP_3:def 2 b" * a * b; end; theorem :: GROUP_3:16 a |^ g = b |^ g implies a = b; theorem :: GROUP_3:17 (1_G) |^ a = 1_G; theorem :: GROUP_3:18 a |^ b = 1_G implies a = 1_G; theorem :: GROUP_3:19 a |^ 1_G = a; theorem :: GROUP_3:20 a |^ a = a; theorem :: GROUP_3:21 a |^ a" = a & a" |^ a = a"; theorem :: GROUP_3:22 a |^ b = a iff a * b = b * a; theorem :: GROUP_3:23 (a * b) |^ g = a |^ g * (b |^ g); theorem :: GROUP_3:24 a |^ g |^ h = a |^ (g * h); theorem :: GROUP_3:25 a |^ b |^ b" = a & a |^ b" |^ b = a; theorem :: GROUP_3:26 a" |^ b = (a |^ b)"; theorem :: GROUP_3:27 (a |^ n) |^ b = (a |^ b) |^ n; theorem :: GROUP_3:28 (a |^ i) |^ b = (a |^ b) |^ i; theorem :: GROUP_3:29 G is commutative Group implies a |^ b = a; theorem :: GROUP_3:30 (for a,b holds a |^ b = a) implies G is commutative; definition let G,A,B; func A |^ B -> Subset of G equals :: GROUP_3:def 3 {g |^ h : g in A & h in B}; end; theorem :: GROUP_3:31 x in A |^ B iff ex g,h st x = g |^ h & g in A & h in B; theorem :: GROUP_3:32 A |^ B <> {} iff A <> {} & B <> {}; theorem :: GROUP_3:33 A |^ B c= B" * A * B; theorem :: GROUP_3:34 (A * B) |^ C c= A |^ C * (B |^ C); theorem :: GROUP_3:35 A |^ B |^ C = A |^ (B * C); theorem :: GROUP_3:36 A" |^ B = (A |^ B)"; theorem :: GROUP_3:37 {a} |^ {b} = {a |^ b}; theorem :: GROUP_3:38 {a} |^ {b,c} = {a |^ b,a |^ c}; theorem :: GROUP_3:39 {a,b} |^ {c} = {a |^ c,b |^ c}; theorem :: GROUP_3:40 {a,b} |^ {c,d} = {a |^ c,a |^ d,b |^ c,b |^ d}; definition let G,A,g; func A |^ g -> Subset of G equals :: GROUP_3:def 4 A |^ {g}; func g |^ A -> Subset of G equals :: GROUP_3:def 5 {g} |^ A; end; theorem :: GROUP_3:41 x in A |^ g iff ex h st x = h |^ g & h in A; theorem :: GROUP_3:42 x in g |^ A iff ex h st x = g |^ h & h in A; theorem :: GROUP_3:43 g |^ A c= A" * g * A; theorem :: GROUP_3:44 A |^ B |^ g = A |^ (B * g); theorem :: GROUP_3:45 A |^ g |^ B = A |^ (g * B); theorem :: GROUP_3:46 g |^ A |^ B = g |^ (A * B); theorem :: GROUP_3:47 A |^ a |^ b = A |^ (a * b); theorem :: GROUP_3:48 a |^ A |^ b = a |^ (A * b); theorem :: GROUP_3:49 a |^ b |^ A = a |^ (b * A); theorem :: GROUP_3:50 A |^ g = g" * A * g; theorem :: GROUP_3:51 (A * B) |^ a c= (A |^ a) * (B |^ a); theorem :: GROUP_3:52 A |^ 1_G = A; theorem :: GROUP_3:53 A <> {} implies (1_G) |^ A = {1_G}; theorem :: GROUP_3:54 A |^ a |^ a" = A & A |^ a" |^ a = A; theorem :: GROUP_3:55 G is commutative Group iff for A,B st B <> {} holds A |^ B = A; theorem :: GROUP_3:56 G is commutative Group iff for A,g holds A |^ g = A; theorem :: GROUP_3:57 G is commutative Group iff for A,g st A <> {} holds g |^ A = {g}; definition let G,H,a; func H |^ a -> strict Subgroup of G means :: GROUP_3:def 6 the carrier of it = carr(H) |^ a; end; theorem :: GROUP_3:58 x in H |^ a iff ex g st x = g |^ a & g in H; theorem :: GROUP_3:59 the carrier of H |^ a = a" * H * a; theorem :: GROUP_3:60 H |^ a |^ b = H |^ (a * b); theorem :: GROUP_3:61 for H being strict Subgroup of G holds H |^ 1_G = H; theorem :: GROUP_3:62 for H being strict Subgroup of G holds H |^ a |^ a" = H & H |^ a " |^ a = H; theorem :: GROUP_3:63 (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a); theorem :: GROUP_3:64 card H = card(H |^ a); theorem :: GROUP_3:65 H is finite iff H |^ a is finite; registration let G,a; let H be finite Subgroup of G; cluster H |^ a -> finite; end; theorem :: GROUP_3:66 for H being finite Subgroup of G holds card H = card(H |^ a); theorem :: GROUP_3:67 (1).G |^ a = (1).G; theorem :: GROUP_3:68 for H being strict Subgroup of G holds H |^ a = (1).G implies H = (1). G; theorem :: GROUP_3:69 for G being Group, a being Element of G holds (Omega).G |^ a = (Omega).G; theorem :: GROUP_3:70 for H being strict Subgroup of G holds H |^ a = G implies H = G; theorem :: GROUP_3:71 Index H = Index(H |^ a); theorem :: GROUP_3:72 Left_Cosets H is finite implies index H = index(H |^ a); theorem :: GROUP_3:73 G is commutative Group implies for H being strict Subgroup of G for a holds H |^ a = H; definition let G,a,b; pred a,b are_conjugated means :: GROUP_3:def 7 ex g st a = b |^ g; end; notation let G,a,b; antonym a,b are_not_conjugated for a,b are_conjugated; end; theorem :: GROUP_3:74 a,b are_conjugated iff ex g st b = a |^ g; theorem :: GROUP_3:75 a,a are_conjugated; theorem :: GROUP_3:76 a,b are_conjugated implies b,a are_conjugated; definition let G,a,b; redefine pred a,b are_conjugated; reflexivity; symmetry; end; theorem :: GROUP_3:77 a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated; theorem :: GROUP_3:78 a,1_G are_conjugated or 1_G,a are_conjugated implies a = 1_G; theorem :: GROUP_3:79 a |^ carr (Omega).G = {b : a,b are_conjugated}; definition let G,a; func con_class a -> Subset of G equals :: GROUP_3:def 8 a |^ carr (Omega).G; end; theorem :: GROUP_3:80 x in con_class a iff ex b st b = x & a,b are_conjugated; theorem :: GROUP_3:81 a in con_class b iff a,b are_conjugated; theorem :: GROUP_3:82 a |^ g in con_class a; theorem :: GROUP_3:83 a in con_class a; theorem :: GROUP_3:84 a in con_class b implies b in con_class a; theorem :: GROUP_3:85 con_class a = con_class b iff con_class a meets con_class b; theorem :: GROUP_3:86 con_class a = {1_G} iff a = 1_G; theorem :: GROUP_3:87 con_class a * A = A * con_class a; definition let G,A,B; pred A,B are_conjugated means :: GROUP_3:def 9 ex g st A = B |^ g; end; notation let G,A,B; antonym A,B are_not_conjugated for A,B are_conjugated; end; theorem :: GROUP_3:88 A,B are_conjugated iff ex g st B = A |^ g; theorem :: GROUP_3:89 A,A are_conjugated; theorem :: GROUP_3:90 A,B are_conjugated implies B,A are_conjugated; definition let G,A,B; redefine pred A,B are_conjugated; reflexivity; symmetry; end; theorem :: GROUP_3:91 A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated; theorem :: GROUP_3:92 {a},{b} are_conjugated iff a,b are_conjugated; theorem :: GROUP_3:93 A,carr H1 are_conjugated implies ex H2 being strict Subgroup of G st the carrier of H2 = A; definition let G,A; func con_class A -> Subset-Family of G equals :: GROUP_3:def 10 {B : A,B are_conjugated}; end; theorem :: GROUP_3:94 x in con_class A iff ex B st x = B & A,B are_conjugated; theorem :: GROUP_3:95 A in con_class B iff A,B are_conjugated; theorem :: GROUP_3:96 A |^ g in con_class A; theorem :: GROUP_3:97 A in con_class A; theorem :: GROUP_3:98 A in con_class B implies B in con_class A; theorem :: GROUP_3:99 con_class A = con_class B iff con_class A meets con_class B; theorem :: GROUP_3:100 con_class{a} = {{b} : b in con_class a}; theorem :: GROUP_3:101 G is finite implies con_class A is finite; definition let G,H1,H2; pred H1,H2 are_conjugated means :: GROUP_3:def 11 ex g st the multMagma of H1 = H2 |^ g; end; notation let G,H1,H2; antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated; end; theorem :: GROUP_3:102 for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated iff ex g st H2 = H1 |^ g; theorem :: GROUP_3:103 for H1 being strict Subgroup of G holds H1,H1 are_conjugated; theorem :: GROUP_3:104 for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated implies H2,H1 are_conjugated; definition let G; let H1,H2 be strict Subgroup of G; redefine pred H1,H2 are_conjugated; reflexivity; symmetry; end; theorem :: GROUP_3:105 for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated & H2,H3 are_conjugated implies H1,H3 are_conjugated; reserve L for Subset of Subgroups G; definition let G,H; func con_class H -> Subset of Subgroups G means :: GROUP_3:def 12 for x being object holds x in it iff ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated; end; theorem :: GROUP_3:106 x in con_class H implies x is strict Subgroup of G; theorem :: GROUP_3:107 for H1,H2 being strict Subgroup of G holds H1 in con_class H2 iff H1,H2 are_conjugated; theorem :: GROUP_3:108 for H being strict Subgroup of G holds H |^ g in con_class H; theorem :: GROUP_3:109 for H being strict Subgroup of G holds H in con_class H; theorem :: GROUP_3:110 for H1,H2 being strict Subgroup of G holds H1 in con_class H2 implies H2 in con_class H1; theorem :: GROUP_3:111 for H1,H2 being strict Subgroup of G holds con_class H1 = con_class H2 iff con_class H1 meets con_class H2; theorem :: GROUP_3:112 G is finite implies con_class H is finite; theorem :: GROUP_3:113 for H1 being strict Subgroup of G holds H1,H2 are_conjugated iff carr H1,carr H2 are_conjugated; definition let G; let IT be Subgroup of G; attr IT is normal means :: GROUP_3:def 13 for a holds IT |^ a = the multMagma of IT; end; registration let G; cluster strict normal for Subgroup of G; end; reserve N2 for normal Subgroup of G; theorem :: GROUP_3:114 (1).G is normal & (Omega).G is normal; theorem :: GROUP_3:115 for N1,N2 being strict normal Subgroup of G holds N1 /\ N2 is normal; theorem :: GROUP_3:116 for H being strict Subgroup of G holds G is commutative Group implies H is normal; theorem :: GROUP_3:117 H is normal Subgroup of G iff for a holds a * H = H * a; theorem :: GROUP_3:118 for H being Subgroup of G holds H is normal Subgroup of G iff for a holds a * H c= H * a; theorem :: GROUP_3:119 for H being Subgroup of G holds H is normal Subgroup of G iff for a holds H * a c= a * H; theorem :: GROUP_3:120 for H being Subgroup of G holds H is normal Subgroup of G iff for A holds A * H = H * A; theorem :: GROUP_3:121 for H being strict Subgroup of G holds H is normal Subgroup of G iff for a holds H is Subgroup of H |^ a; theorem :: GROUP_3:122 for H being strict Subgroup of G holds H is normal Subgroup of G iff for a holds H |^ a is Subgroup of H; theorem :: GROUP_3:123 for H being strict Subgroup of G holds H is normal Subgroup of G iff con_class H = {H}; theorem :: GROUP_3:124 for H being strict Subgroup of G holds H is normal Subgroup of G iff for a st a in H holds con_class a c= carr H; theorem :: GROUP_3:125 for N1,N2 being strict normal Subgroup of G holds carr N1 * carr N2 = carr N2 * carr N1; theorem :: GROUP_3:126 for N1,N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = carr N1 * carr N2; theorem :: GROUP_3:127 for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N; theorem :: GROUP_3:128 for H being Subgroup of G holds Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G; definition let G; let A; func Normalizer A -> strict Subgroup of G means :: GROUP_3:def 14 the carrier of it = {h : A |^ h = A}; end; theorem :: GROUP_3:129 x in Normalizer A iff ex h st x = h & A |^ h = A; theorem :: GROUP_3:130 card con_class A = Index Normalizer A; theorem :: GROUP_3:131 con_class A is finite or Left_Cosets Normalizer A is finite implies ex C being finite set st C = con_class A & card C = index Normalizer A; theorem :: GROUP_3:132 card con_class a = Index Normalizer{a}; theorem :: GROUP_3:133 con_class a is finite or Left_Cosets Normalizer{a} is finite implies ex C being finite set st C = con_class a & card C = index Normalizer{a}; definition let G; let H; func Normalizer H -> strict Subgroup of G equals :: GROUP_3:def 15 Normalizer carr H; end; theorem :: GROUP_3:134 for H being strict Subgroup of G holds x in Normalizer H iff ex h st x = h & H |^ h = H; theorem :: GROUP_3:135 for H being strict Subgroup of G holds card con_class H = Index Normalizer H; theorem :: GROUP_3:136 for H being strict Subgroup of G holds con_class H is finite or Left_Cosets Normalizer H is finite implies ex C being finite set st C = con_class H & card C = index Normalizer H; theorem :: GROUP_3:137 for G being strict Group, H being strict Subgroup of G holds H is normal Subgroup of G iff Normalizer H = G; theorem :: GROUP_3:138 for G being strict Group holds Normalizer (1).G = G; theorem :: GROUP_3:139 for G being strict Group holds Normalizer (Omega).G = G;