:: GROUP_3 semantic presentation begin theorem Th1: :: GROUP_3:1 for G being Group for a, b being Element of G holds ( (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 ) proof let G be Group; ::_thesis: for a, b being Element of G holds ( (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 ) let a, b be Element of G; ::_thesis: ( (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 ) thus A1: (a * b) * (b ") = a * (b * (b ")) by GROUP_1:def_3 .= a * (1_ G) by GROUP_1:def_5 .= a by GROUP_1:def_4 ; ::_thesis: ( (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 ) thus A2: (a * (b ")) * b = a * ((b ") * b) by GROUP_1:def_3 .= a * (1_ G) by GROUP_1:def_5 .= a by GROUP_1:def_4 ; ::_thesis: ( ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a ) thus A3: ((b ") * b) * a = (1_ G) * a by GROUP_1:def_5 .= a by GROUP_1:def_4 ; ::_thesis: ( (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a ) thus (b * (b ")) * a = (1_ G) * a by GROUP_1:def_5 .= a by GROUP_1:def_4 ; ::_thesis: ( a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a ) hence ( a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a ) by A1, A2, A3, GROUP_1:def_3; ::_thesis: verum end; Lm1: for A being commutative Group for a, b being Element of A holds a * b = b * a ; theorem :: GROUP_3:2 for G being Group holds ( G is commutative Group iff the multF of G is commutative ) proof let G be Group; ::_thesis: ( G is commutative Group iff the multF of G is commutative ) thus ( G is commutative Group implies the multF of G is commutative ) ::_thesis: ( the multF of G is commutative implies G is commutative Group ) proof assume A1: G is commutative Group ; ::_thesis: the multF of G is commutative let a be Element of G; :: according to BINOP_1:def_2 ::_thesis: for b1 being Element of the carrier of G holds the multF of G . (a,b1) = the multF of G . (b1,a) let b be Element of G; ::_thesis: the multF of G . (a,b) = the multF of G . (b,a) thus the multF of G . (a,b) = a * b .= b * a by A1, Lm1 .= the multF of G . (b,a) ; ::_thesis: verum end; assume A2: the multF of G is commutative ; ::_thesis: G is commutative Group G is commutative proof let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a let b be Element of G; ::_thesis: a * b = b * a thus a * b = b * a by A2, BINOP_1:def_2; ::_thesis: verum end; hence G is commutative Group ; ::_thesis: verum end; theorem :: GROUP_3:3 for G being Group holds (1). G is commutative proof let G be Group; ::_thesis: (1). G is commutative let a, b be Element of ((1). G); :: according to GROUP_1:def_12 ::_thesis: a * b = b * a a in the carrier of ((1). G) ; then a in {(1_ G)} by GROUP_2:def_7; then A1: a = 1_ G by TARSKI:def_1; b in the carrier of ((1). G) ; then b in {(1_ G)} by GROUP_2:def_7; hence a * b = b * a by A1, TARSKI:def_1; ::_thesis: verum end; theorem Th4: :: GROUP_3:4 for G being Group for A, B, C, D being Subset of G st A c= B & C c= D holds A * C c= B * D proof let G be Group; ::_thesis: for A, B, C, D being Subset of G st A c= B & C c= D holds A * C c= B * D let A, B, C, D be Subset of G; ::_thesis: ( A c= B & C c= D implies A * C c= B * D ) assume A1: ( A c= B & C c= D ) ; ::_thesis: A * C c= B * D let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * C or x in B * D ) assume x in A * C ; ::_thesis: x in B * D then ex a, c being Element of G st ( x = a * c & a in A & c in C ) ; hence x in B * D by A1; ::_thesis: verum end; theorem :: GROUP_3:5 for G being Group for a being Element of G for A, B being Subset of G st A c= B holds ( a * A c= a * B & A * a c= B * a ) by Th4; theorem Th6: :: GROUP_3:6 for G being Group for a being Element of G for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds ( a * H1 c= a * H2 & H1 * a c= H2 * a ) proof let G be Group; ::_thesis: for a being Element of G for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds ( a * H1 c= a * H2 & H1 * a c= H2 * a ) let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds ( a * H1 c= a * H2 & H1 * a c= H2 * a ) let H1, H2 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies ( a * H1 c= a * H2 & H1 * a c= H2 * a ) ) assume H1 is Subgroup of H2 ; ::_thesis: ( a * H1 c= a * H2 & H1 * a c= H2 * a ) then the carrier of H1 c= the carrier of H2 by GROUP_2:def_5; hence ( a * H1 c= a * H2 & H1 * a c= H2 * a ) by Th4; ::_thesis: verum end; theorem :: GROUP_3:7 for G being Group for a being Element of G for H being Subgroup of G holds a * H = {a} * H ; theorem :: GROUP_3:8 for G being Group for a being Element of G for H being Subgroup of G holds H * a = H * {a} ; theorem Th9: :: GROUP_3:9 for G being Group for a being Element of G for A being Subset of G for H being Subgroup of G holds (A * a) * H = A * (a * H) proof let G be Group; ::_thesis: for a being Element of G for A being Subset of G for H being Subgroup of G holds (A * a) * H = A * (a * H) let a be Element of G; ::_thesis: for A being Subset of G for H being Subgroup of G holds (A * a) * H = A * (a * H) let A be Subset of G; ::_thesis: for H being Subgroup of G holds (A * a) * H = A * (a * H) let H be Subgroup of G; ::_thesis: (A * a) * H = A * (a * H) thus (A * a) * H = A * ({a} * H) by GROUP_2:96 .= A * (a * H) ; ::_thesis: verum end; theorem :: GROUP_3:10 for G being Group for a being Element of G for A being Subset of G for H being Subgroup of G holds (a * H) * A = a * (H * A) proof let G be Group; ::_thesis: for a being Element of G for A being Subset of G for H being Subgroup of G holds (a * H) * A = a * (H * A) let a be Element of G; ::_thesis: for A being Subset of G for H being Subgroup of G holds (a * H) * A = a * (H * A) let A be Subset of G; ::_thesis: for H being Subgroup of G holds (a * H) * A = a * (H * A) let H be Subgroup of G; ::_thesis: (a * H) * A = a * (H * A) thus (a * H) * A = ({a} * H) * A .= a * (H * A) by GROUP_2:97 ; ::_thesis: verum end; theorem :: GROUP_3:11 for G being Group for a being Element of G for A being Subset of G for H being Subgroup of G holds (A * H) * a = A * (H * a) proof let G be Group; ::_thesis: for a being Element of G for A being Subset of G for H being Subgroup of G holds (A * H) * a = A * (H * a) let a be Element of G; ::_thesis: for A being Subset of G for H being Subgroup of G holds (A * H) * a = A * (H * a) let A be Subset of G; ::_thesis: for H being Subgroup of G holds (A * H) * a = A * (H * a) let H be Subgroup of G; ::_thesis: (A * H) * a = A * (H * a) thus (A * H) * a = A * (H * {a}) by GROUP_2:97 .= A * (H * a) ; ::_thesis: verum end; theorem :: GROUP_3:12 for G being Group for a being Element of G for A being Subset of G for H being Subgroup of G holds (H * a) * A = H * (a * A) proof let G be Group; ::_thesis: for a being Element of G for A being Subset of G for H being Subgroup of G holds (H * a) * A = H * (a * A) let a be Element of G; ::_thesis: for A being Subset of G for H being Subgroup of G holds (H * a) * A = H * (a * A) let A be Subset of G; ::_thesis: for H being Subgroup of G holds (H * a) * A = H * (a * A) let H be Subgroup of G; ::_thesis: (H * a) * A = H * (a * A) thus (H * a) * A = (H * {a}) * A .= H * (a * A) by GROUP_2:98 ; ::_thesis: verum end; theorem :: GROUP_3:13 for G being Group for a being Element of G for H1, H2 being Subgroup of G holds (H1 * a) * H2 = H1 * (a * H2) by Th9; definition let G be Group; func Subgroups G -> set means :Def1: :: GROUP_3:def 1 for x being set holds ( x in it iff x is strict Subgroup of G ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict Subgroup of G ) proof defpred S1[ set , set ] means ex H being strict Subgroup of G st ( \$2 = H & \$1 = the carrier of H ); defpred S2[ set ] means ex H being strict Subgroup of G st \$1 = the carrier of H; consider B being set such that A1: for x being set holds ( x in B iff ( x in bool the carrier of G & S2[x] ) ) from XBOOLE_0:sch_1(); A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds y1 = y2 by GROUP_2:59; consider f being Function such that A3: for x, y being set holds ( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch_1(A2); for x being set holds ( x in B iff ex y being set st [x,y] in f ) proof let x be set ; ::_thesis: ( x in B iff ex y being set st [x,y] in f ) thus ( x in B implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in B ) proof assume A4: x in B ; ::_thesis: ex y being set st [x,y] in f then consider H being strict Subgroup of G such that A5: x = the carrier of H by A1; reconsider y = H as set ; take y ; ::_thesis: [x,y] in f thus [x,y] in f by A3, A4, A5; ::_thesis: verum end; given y being set such that A6: [x,y] in f ; ::_thesis: x in B thus x in B by A3, A6; ::_thesis: verum end; then A7: B = dom f by XTUPLE_0:def_12; for y being set holds ( y in rng f iff y is strict Subgroup of G ) proof let y be set ; ::_thesis: ( y in rng f iff y is strict Subgroup of G ) thus ( y in rng f implies y is strict Subgroup of G ) ::_thesis: ( y is strict Subgroup of G implies y in rng f ) proof assume y in rng f ; ::_thesis: y is strict Subgroup of G then consider x being set such that A8: ( x in dom f & y = f . x ) by FUNCT_1:def_3; [x,y] in f by A8, FUNCT_1:def_2; then ex H being strict Subgroup of G st ( y = H & x = the carrier of H ) by A3; hence y is strict Subgroup of G ; ::_thesis: verum end; assume y is strict Subgroup of G ; ::_thesis: y in rng f then reconsider H = y as strict Subgroup of G ; reconsider x = the carrier of H as set ; the carrier of H c= the carrier of G by GROUP_2:def_5; then A9: x in dom f by A1, A7; then [x,y] in f by A3, A7; then y = f . x by A9, FUNCT_1:def_2; hence y in rng f by A9, FUNCT_1:def_3; ::_thesis: verum end; hence ex b1 being set st for x being set holds ( x in b1 iff x is strict Subgroup of G ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict Subgroup of G ) ) & ( for x being set holds ( x in b2 iff x is strict Subgroup of G ) ) holds b1 = b2 proof defpred S1[ set ] means \$1 is strict Subgroup of G; let A1, A2 be set ; ::_thesis: ( ( for x being set holds ( x in A1 iff x is strict Subgroup of G ) ) & ( for x being set holds ( x in A2 iff x is strict Subgroup of G ) ) implies A1 = A2 ) assume A10: for x being set holds ( x in A1 iff S1[x] ) ; ::_thesis: ( ex x being set st ( ( x in A2 implies x is strict Subgroup of G ) implies ( x is strict Subgroup of G & not x in A2 ) ) or A1 = A2 ) assume A11: for x being set holds ( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2 thus A1 = A2 from XBOOLE_0:sch_2(A10, A11); ::_thesis: verum end; end; :: deftheorem Def1 defines Subgroups GROUP_3:def_1_:_ for G being Group for b2 being set holds ( b2 = Subgroups G iff for x being set holds ( x in b2 iff x is strict Subgroup of G ) ); registration let G be Group; cluster Subgroups G -> non empty ; coherence not Subgroups G is empty proof set x = the strict Subgroup of G; the strict Subgroup of G in Subgroups G by Def1; hence not Subgroups G is empty ; ::_thesis: verum end; end; theorem :: GROUP_3:14 for G being strict Group holds G in Subgroups G proof let G be strict Group; ::_thesis: G in Subgroups G G is Subgroup of G by GROUP_2:54; hence G in Subgroups G by Def1; ::_thesis: verum end; theorem Th15: :: GROUP_3:15 for G being Group st G is finite holds Subgroups G is finite proof let G be Group; ::_thesis: ( G is finite implies Subgroups G is finite ) defpred S1[ set , set ] means ex H being strict Subgroup of G st ( \$1 = H & \$2 = the carrier of H ); assume A1: G is finite ; ::_thesis: Subgroups G is finite A2: for x being set st x in Subgroups G holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Subgroups G implies ex y being set st S1[x,y] ) assume x in Subgroups G ; ::_thesis: ex y being set st S1[x,y] then reconsider F = x as strict Subgroup of G by Def1; reconsider y = the carrier of F as set ; take y ; ::_thesis: S1[x,y] take F ; ::_thesis: ( x = F & y = the carrier of F ) thus ( x = F & y = the carrier of F ) ; ::_thesis: verum end; consider f being Function such that A3: dom f = Subgroups G and A4: for x being set st x in Subgroups G holds S1[x,f . x] from CLASSES1:sch_1(A2); A5: rng f c= bool the carrier of G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in bool the carrier of G ) assume x in rng f ; ::_thesis: x in bool the carrier of G then consider y being set such that A6: ( y in dom f & f . y = x ) by FUNCT_1:def_3; consider H being strict Subgroup of G such that y = H and A7: x = the carrier of H by A3, A4, A6; the carrier of H c= the carrier of G by GROUP_2:def_5; hence x in bool the carrier of G by A7; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A8: ( x in dom f & y in dom f ) and A9: f . x = f . y ; ::_thesis: x = y ( ex H1 being strict Subgroup of G st ( x = H1 & f . x = the carrier of H1 ) & ex H2 being strict Subgroup of G st ( y = H2 & f . y = the carrier of H2 ) ) by A3, A4, A8; hence x = y by A9, GROUP_2:59; ::_thesis: verum end; then card (Subgroups G) c= card (bool the carrier of G) by A3, A5, CARD_1:10; hence Subgroups G is finite by A1, CARD_2:49; ::_thesis: verum end; definition let G be Group; let a, b be Element of G; funca |^ b -> Element of G equals :: GROUP_3:def 2 ((b ") * a) * b; correctness coherence ((b ") * a) * b is Element of G; ; end; :: deftheorem defines |^ GROUP_3:def_2_:_ for G being Group for a, b being Element of G holds a |^ b = ((b ") * a) * b; theorem Th16: :: GROUP_3:16 for G being Group for a, g, b being Element of G st a |^ g = b |^ g holds a = b proof let G be Group; ::_thesis: for a, g, b being Element of G st a |^ g = b |^ g holds a = b let a, g, b be Element of G; ::_thesis: ( a |^ g = b |^ g implies a = b ) assume a |^ g = b |^ g ; ::_thesis: a = b then (g ") * a = (g ") * b by GROUP_1:6; hence a = b by GROUP_1:6; ::_thesis: verum end; theorem Th17: :: GROUP_3:17 for G being Group for a being Element of G holds (1_ G) |^ a = 1_ G proof let G be Group; ::_thesis: for a being Element of G holds (1_ G) |^ a = 1_ G let a be Element of G; ::_thesis: (1_ G) |^ a = 1_ G thus (1_ G) |^ a = (a ") * a by GROUP_1:def_4 .= 1_ G by GROUP_1:def_5 ; ::_thesis: verum end; theorem Th18: :: GROUP_3:18 for G being Group for a, b being Element of G st a |^ b = 1_ G holds a = 1_ G proof let G be Group; ::_thesis: for a, b being Element of G st a |^ b = 1_ G holds a = 1_ G let a, b be Element of G; ::_thesis: ( a |^ b = 1_ G implies a = 1_ G ) assume a |^ b = 1_ G ; ::_thesis: a = 1_ G then b " = (b ") * a by GROUP_1:12; hence a = 1_ G by GROUP_1:7; ::_thesis: verum end; theorem Th19: :: GROUP_3:19 for G being Group for a being Element of G holds a |^ (1_ G) = a proof let G be Group; ::_thesis: for a being Element of G holds a |^ (1_ G) = a let a be Element of G; ::_thesis: a |^ (1_ G) = a thus a |^ (1_ G) = ((1_ G) ") * a by GROUP_1:def_4 .= (1_ G) * a by GROUP_1:8 .= a by GROUP_1:def_4 ; ::_thesis: verum end; theorem Th20: :: GROUP_3:20 for G being Group for a being Element of G holds a |^ a = a proof let G be Group; ::_thesis: for a being Element of G holds a |^ a = a let a be Element of G; ::_thesis: a |^ a = a thus a |^ a = (1_ G) * a by GROUP_1:def_5 .= a by GROUP_1:def_4 ; ::_thesis: verum end; theorem :: GROUP_3:21 for G being Group for a being Element of G holds ( a |^ (a ") = a & (a ") |^ a = a " ) by Th1; theorem Th22: :: GROUP_3:22 for G being Group for a, b being Element of G holds ( a |^ b = a iff a * b = b * a ) proof let G be Group; ::_thesis: for a, b being Element of G holds ( a |^ b = a iff a * b = b * a ) let a, b be Element of G; ::_thesis: ( a |^ b = a iff a * b = b * a ) thus ( a |^ b = a implies a * b = b * a ) ::_thesis: ( a * b = b * a implies a |^ b = a ) proof assume a |^ b = a ; ::_thesis: a * b = b * a then a = (b ") * (a * b) by GROUP_1:def_3; hence a * b = b * a by GROUP_1:13; ::_thesis: verum end; assume a * b = b * a ; ::_thesis: a |^ b = a then a = (b ") * (a * b) by GROUP_1:13; hence a |^ b = a by GROUP_1:def_3; ::_thesis: verum end; theorem Th23: :: GROUP_3:23 for G being Group for a, b, g being Element of G holds (a * b) |^ g = (a |^ g) * (b |^ g) proof let G be Group; ::_thesis: for a, b, g being Element of G holds (a * b) |^ g = (a |^ g) * (b |^ g) let a, b, g be Element of G; ::_thesis: (a * b) |^ g = (a |^ g) * (b |^ g) thus (a * b) |^ g = ((g ") * ((a * (1_ G)) * b)) * g by GROUP_1:def_4 .= ((g ") * ((a * (g * (g "))) * b)) * g by GROUP_1:def_5 .= ((g ") * (((a * g) * (g ")) * b)) * g by GROUP_1:def_3 .= ((g ") * ((a * g) * ((g ") * b))) * g by GROUP_1:def_3 .= (((g ") * (a * g)) * ((g ") * b)) * g by GROUP_1:def_3 .= ((a |^ g) * ((g ") * b)) * g by GROUP_1:def_3 .= (a |^ g) * (b |^ g) by GROUP_1:def_3 ; ::_thesis: verum end; theorem Th24: :: GROUP_3:24 for G being Group for a, g, h being Element of G holds (a |^ g) |^ h = a |^ (g * h) proof let G be Group; ::_thesis: for a, g, h being Element of G holds (a |^ g) |^ h = a |^ (g * h) let a, g, h be Element of G; ::_thesis: (a |^ g) |^ h = a |^ (g * h) thus (a |^ g) |^ h = (((h ") * ((g ") * a)) * g) * h by GROUP_1:def_3 .= ((((h ") * (g ")) * a) * g) * h by GROUP_1:def_3 .= ((((g * h) ") * a) * g) * h by GROUP_1:17 .= a |^ (g * h) by GROUP_1:def_3 ; ::_thesis: verum end; theorem Th25: :: GROUP_3:25 for G being Group for a, b being Element of G holds ( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a ) proof let G be Group; ::_thesis: for a, b being Element of G holds ( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a ) let a, b be Element of G; ::_thesis: ( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a ) thus (a |^ b) |^ (b ") = a |^ (b * (b ")) by Th24 .= a |^ (1_ G) by GROUP_1:def_5 .= a by Th19 ; ::_thesis: (a |^ (b ")) |^ b = a thus (a |^ (b ")) |^ b = a |^ ((b ") * b) by Th24 .= a |^ (1_ G) by GROUP_1:def_5 .= a by Th19 ; ::_thesis: verum end; theorem Th26: :: GROUP_3:26 for G being Group for a, b being Element of G holds (a ") |^ b = (a |^ b) " proof let G be Group; ::_thesis: for a, b being Element of G holds (a ") |^ b = (a |^ b) " let a, b be Element of G; ::_thesis: (a ") |^ b = (a |^ b) " thus (a ") |^ b = ((a * b) ") * b by GROUP_1:17 .= ((a * b) ") * ((b ") ") .= ((b ") * (a * b)) " by GROUP_1:17 .= (a |^ b) " by GROUP_1:def_3 ; ::_thesis: verum end; Lm2: now__::_thesis:_for_G_being_Group for_a,_b_being_Element_of_G_holds_(a_|^_0)_|^_b_=_(a_|^_b)_|^_0 let G be Group; ::_thesis: for a, b being Element of G holds (a |^ 0) |^ b = (a |^ b) |^ 0 let a, b be Element of G; ::_thesis: (a |^ 0) |^ b = (a |^ b) |^ 0 thus (a |^ 0) |^ b = (1_ G) |^ b by GROUP_1:25 .= 1_ G by Th17 .= (a |^ b) |^ 0 by GROUP_1:25 ; ::_thesis: verum end; Lm3: now__::_thesis:_for_n_being_Nat_st_(_for_G_being_Group for_a,_b_being_Element_of_G_holds_(a_|^_n)_|^_b_=_(a_|^_b)_|^_n_)_holds_ for_G_being_Group for_a,_b_being_Element_of_G_holds_(a_|^_(n_+_1))_|^_b_=_(a_|^_b)_|^_(n_+_1) let n be Nat; ::_thesis: ( ( for G being Group for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ) implies for G being Group for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1) ) assume A1: for G being Group for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ; ::_thesis: for G being Group for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1) let G be Group; ::_thesis: for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1) let a, b be Element of G; ::_thesis: (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1) thus (a |^ (n + 1)) |^ b = ((a |^ n) * a) |^ b by GROUP_1:34 .= ((a |^ n) |^ b) * (a |^ b) by Th23 .= ((a |^ b) |^ n) * (a |^ b) by A1 .= (a |^ b) |^ (n + 1) by GROUP_1:34 ; ::_thesis: verum end; Lm4: for n being Nat for G being Group for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n proof defpred S1[ Nat] means for G being Group for a, b being Element of G holds (a |^ \$1) |^ b = (a |^ b) |^ \$1; A1: for k being Nat st S1[k] holds S1[k + 1] by Lm3; A2: S1[ 0 ] by Lm2; for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1); hence for n being Nat for G being Group for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ; ::_thesis: verum end; theorem :: GROUP_3:27 for G being Group for a, b being Element of G for n being Nat holds (a |^ n) |^ b = (a |^ b) |^ n by Lm4; theorem :: GROUP_3:28 for G being Group for a, b being Element of G for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i proof let G be Group; ::_thesis: for a, b being Element of G for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i let a, b be Element of G; ::_thesis: for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i let i be Integer; ::_thesis: (a |^ i) |^ b = (a |^ b) |^ i percases ( i >= 0 or i < 0 ) ; suppose i >= 0 ; ::_thesis: (a |^ i) |^ b = (a |^ b) |^ i then i = abs i by ABSVALUE:def_1; hence (a |^ i) |^ b = (a |^ b) |^ i by Lm4; ::_thesis: verum end; supposeA1: i < 0 ; ::_thesis: (a |^ i) |^ b = (a |^ b) |^ i hence (a |^ i) |^ b = ((a |^ (abs i)) ") |^ b by GROUP_1:30 .= ((a |^ (abs i)) |^ b) " by Th26 .= ((a |^ b) |^ (abs i)) " by Lm4 .= (a |^ b) |^ i by A1, GROUP_1:30 ; ::_thesis: verum end; end; end; theorem Th29: :: GROUP_3:29 for G being Group for a, b being Element of G st G is commutative Group holds a |^ b = a proof let G be Group; ::_thesis: for a, b being Element of G st G is commutative Group holds a |^ b = a let a, b be Element of G; ::_thesis: ( G is commutative Group implies a |^ b = a ) assume G is commutative Group ; ::_thesis: a |^ b = a hence a |^ b = (a * (b ")) * b by Lm1 .= a by Th1 ; ::_thesis: verum end; theorem Th30: :: GROUP_3:30 for G being Group st ( for a, b being Element of G holds a |^ b = a ) holds G is commutative proof let G be Group; ::_thesis: ( ( for a, b being Element of G holds a |^ b = a ) implies G is commutative ) assume A1: for a, b being Element of G holds a |^ b = a ; ::_thesis: G is commutative let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a let b be Element of G; ::_thesis: a * b = b * a a |^ b = a by A1; hence a * b = b * a by Th22; ::_thesis: verum end; definition let G be Group; let A, B be Subset of G; funcA |^ B -> Subset of G equals :: GROUP_3:def 3 { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ; coherence { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G proof set X = { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ; { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } c= the carrier of G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } or x in the carrier of G ) assume x in { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ; ::_thesis: x in the carrier of G then ex g, h being Element of G st ( x = g |^ h & g in A & h in B ) ; hence x in the carrier of G ; ::_thesis: verum end; hence { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G ; ::_thesis: verum end; end; :: deftheorem defines |^ GROUP_3:def_3_:_ for G being Group for A, B being Subset of G holds A |^ B = { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ; theorem Th31: :: GROUP_3:31 for x being set for G being Group for A, B being Subset of G holds ( x in A |^ B iff ex g, h being Element of G st ( x = g |^ h & g in A & h in B ) ) ; theorem Th32: :: GROUP_3:32 for G being Group for A, B being Subset of G holds ( A |^ B <> {} iff ( A <> {} & B <> {} ) ) proof let G be Group; ::_thesis: for A, B being Subset of G holds ( A |^ B <> {} iff ( A <> {} & B <> {} ) ) let A, B be Subset of G; ::_thesis: ( A |^ B <> {} iff ( A <> {} & B <> {} ) ) set x = the Element of A; set y = the Element of B; thus ( A |^ B <> {} implies ( A <> {} & B <> {} ) ) ::_thesis: ( A <> {} & B <> {} implies A |^ B <> {} ) proof set x = the Element of A |^ B; assume A |^ B <> {} ; ::_thesis: ( A <> {} & B <> {} ) then ex a, b being Element of G st ( the Element of A |^ B = a |^ b & a in A & b in B ) by Th31; hence ( A <> {} & B <> {} ) ; ::_thesis: verum end; assume A1: A <> {} ; ::_thesis: ( not B <> {} or A |^ B <> {} ) assume A2: B <> {} ; ::_thesis: A |^ B <> {} then reconsider x = the Element of A, y = the Element of B as Element of G by A1, TARSKI:def_3; x |^ y in A |^ B by A1, A2; hence A |^ B <> {} ; ::_thesis: verum end; theorem Th33: :: GROUP_3:33 for G being Group for A, B being Subset of G holds A |^ B c= ((B ") * A) * B proof let G be Group; ::_thesis: for A, B being Subset of G holds A |^ B c= ((B ") * A) * B let A, B be Subset of G; ::_thesis: A |^ B c= ((B ") * A) * B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ B or x in ((B ") * A) * B ) assume x in A |^ B ; ::_thesis: x in ((B ") * A) * B then consider a, b being Element of G such that A1: x = a |^ b and A2: a in A and A3: b in B ; b " in B " by A3; then (b ") * a in (B ") * A by A2; hence x in ((B ") * A) * B by A1, A3; ::_thesis: verum end; theorem Th34: :: GROUP_3:34 for G being Group for A, B, C being Subset of G holds (A * B) |^ C c= (A |^ C) * (B |^ C) proof let G be Group; ::_thesis: for A, B, C being Subset of G holds (A * B) |^ C c= (A |^ C) * (B |^ C) let A, B, C be Subset of G; ::_thesis: (A * B) |^ C c= (A |^ C) * (B |^ C) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) |^ C or x in (A |^ C) * (B |^ C) ) assume x in (A * B) |^ C ; ::_thesis: x in (A |^ C) * (B |^ C) then consider a, b being Element of G such that A1: x = a |^ b and A2: a in A * B and A3: b in C ; consider g, h being Element of G such that A4: ( a = g * h & g in A ) and A5: h in B by A2; A6: h |^ b in B |^ C by A3, A5; ( x = (g |^ b) * (h |^ b) & g |^ b in A |^ C ) by A1, A3, A4, Th23; hence x in (A |^ C) * (B |^ C) by A6; ::_thesis: verum end; theorem Th35: :: GROUP_3:35 for G being Group for A, B, C being Subset of G holds (A |^ B) |^ C = A |^ (B * C) proof let G be Group; ::_thesis: for A, B, C being Subset of G holds (A |^ B) |^ C = A |^ (B * C) let A, B, C be Subset of G; ::_thesis: (A |^ B) |^ C = A |^ (B * C) thus (A |^ B) |^ C c= A |^ (B * C) :: according to XBOOLE_0:def_10 ::_thesis: A |^ (B * C) c= (A |^ B) |^ C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ B) |^ C or x in A |^ (B * C) ) assume x in (A |^ B) |^ C ; ::_thesis: x in A |^ (B * C) then consider a, c being Element of G such that A1: x = a |^ c and A2: a in A |^ B and A3: c in C ; consider g, h being Element of G such that A4: a = g |^ h and A5: g in A and A6: h in B by A2; ( x = g |^ (h * c) & h * c in B * C ) by A1, A3, A4, A6, Th24; hence x in A |^ (B * C) by A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (B * C) or x in (A |^ B) |^ C ) assume x in A |^ (B * C) ; ::_thesis: x in (A |^ B) |^ C then consider a, b being Element of G such that A7: ( x = a |^ b & a in A ) and A8: b in B * C ; consider g, h being Element of G such that A9: ( b = g * h & g in B ) and A10: h in C by A8; ( a |^ g in A |^ B & x = (a |^ g) |^ h ) by A7, A9, Th24; hence x in (A |^ B) |^ C by A10; ::_thesis: verum end; theorem :: GROUP_3:36 for G being Group for A, B being Subset of G holds (A ") |^ B = (A |^ B) " proof let G be Group; ::_thesis: for A, B being Subset of G holds (A ") |^ B = (A |^ B) " let A, B be Subset of G; ::_thesis: (A ") |^ B = (A |^ B) " thus (A ") |^ B c= (A |^ B) " :: according to XBOOLE_0:def_10 ::_thesis: (A |^ B) " c= (A ") |^ B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ") |^ B or x in (A |^ B) " ) assume x in (A ") |^ B ; ::_thesis: x in (A |^ B) " then consider a, b being Element of G such that A1: x = a |^ b and A2: a in A " and A3: b in B ; consider c being Element of G such that A4: ( a = c " & c in A ) by A2; ( x = (c |^ b) " & c |^ b in A |^ B ) by A1, A3, A4, Th26; hence x in (A |^ B) " ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ B) " or x in (A ") |^ B ) assume x in (A |^ B) " ; ::_thesis: x in (A ") |^ B then consider a being Element of G such that A5: x = a " and A6: a in A |^ B ; consider b, c being Element of G such that A7: a = b |^ c and A8: b in A and A9: c in B by A6; A10: b " in A " by A8; x = (b ") |^ c by A5, A7, Th26; hence x in (A ") |^ B by A9, A10; ::_thesis: verum end; theorem Th37: :: GROUP_3:37 for G being Group for a, b being Element of G holds {a} |^ {b} = {(a |^ b)} proof let G be Group; ::_thesis: for a, b being Element of G holds {a} |^ {b} = {(a |^ b)} let a, b be Element of G; ::_thesis: {a} |^ {b} = {(a |^ b)} A1: (({b} ") * {a}) * {b} = ({(b ")} * {a}) * {b} by GROUP_2:3 .= {((b ") * a)} * {b} by GROUP_2:18 .= {(a |^ b)} by GROUP_2:18 ; ( {a} |^ {b} c= (({b} ") * {a}) * {b} & {a} |^ {b} <> {} ) by Th32, Th33; hence {a} |^ {b} = {(a |^ b)} by A1, ZFMISC_1:33; ::_thesis: verum end; theorem :: GROUP_3:38 for G being Group for a, b, c being Element of G holds {a} |^ {b,c} = {(a |^ b),(a |^ c)} proof let G be Group; ::_thesis: for a, b, c being Element of G holds {a} |^ {b,c} = {(a |^ b),(a |^ c)} let a, b, c be Element of G; ::_thesis: {a} |^ {b,c} = {(a |^ b),(a |^ c)} thus {a} |^ {b,c} c= {(a |^ b),(a |^ c)} :: according to XBOOLE_0:def_10 ::_thesis: {(a |^ b),(a |^ c)} c= {a} |^ {b,c} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} |^ {b,c} or x in {(a |^ b),(a |^ c)} ) assume x in {a} |^ {b,c} ; ::_thesis: x in {(a |^ b),(a |^ c)} then consider g, h being Element of G such that A1: x = g |^ h and A2: g in {a} and A3: h in {b,c} ; A4: ( h = b or h = c ) by A3, TARSKI:def_2; g = a by A2, TARSKI:def_1; hence x in {(a |^ b),(a |^ c)} by A1, A4, TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(a |^ b),(a |^ c)} or x in {a} |^ {b,c} ) A5: c in {b,c} by TARSKI:def_2; assume x in {(a |^ b),(a |^ c)} ; ::_thesis: x in {a} |^ {b,c} then A6: ( x = a |^ b or x = a |^ c ) by TARSKI:def_2; ( a in {a} & b in {b,c} ) by TARSKI:def_1, TARSKI:def_2; hence x in {a} |^ {b,c} by A6, A5; ::_thesis: verum end; theorem :: GROUP_3:39 for G being Group for a, b, c being Element of G holds {a,b} |^ {c} = {(a |^ c),(b |^ c)} proof let G be Group; ::_thesis: for a, b, c being Element of G holds {a,b} |^ {c} = {(a |^ c),(b |^ c)} let a, b, c be Element of G; ::_thesis: {a,b} |^ {c} = {(a |^ c),(b |^ c)} thus {a,b} |^ {c} c= {(a |^ c),(b |^ c)} :: according to XBOOLE_0:def_10 ::_thesis: {(a |^ c),(b |^ c)} c= {a,b} |^ {c} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} |^ {c} or x in {(a |^ c),(b |^ c)} ) assume x in {a,b} |^ {c} ; ::_thesis: x in {(a |^ c),(b |^ c)} then consider g, h being Element of G such that A1: x = g |^ h and A2: g in {a,b} and A3: h in {c} ; A4: ( g = b or g = a ) by A2, TARSKI:def_2; h = c by A3, TARSKI:def_1; hence x in {(a |^ c),(b |^ c)} by A1, A4, TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(a |^ c),(b |^ c)} or x in {a,b} |^ {c} ) A5: c in {c} by TARSKI:def_1; assume x in {(a |^ c),(b |^ c)} ; ::_thesis: x in {a,b} |^ {c} then A6: ( x = a |^ c or x = b |^ c ) by TARSKI:def_2; ( a in {a,b} & b in {a,b} ) by TARSKI:def_2; hence x in {a,b} |^ {c} by A6, A5; ::_thesis: verum end; theorem :: GROUP_3:40 for G being Group for a, b, c, d being Element of G holds {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} proof let G be Group; ::_thesis: for a, b, c, d being Element of G holds {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} let a, b, c, d be Element of G; ::_thesis: {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} thus {a,b} |^ {c,d} c= {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} :: according to XBOOLE_0:def_10 ::_thesis: {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} c= {a,b} |^ {c,d} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} |^ {c,d} or x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} ) assume x in {a,b} |^ {c,d} ; ::_thesis: x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} then consider g, h being Element of G such that A1: x = g |^ h and A2: g in {a,b} and A3: h in {c,d} ; A4: ( h = c or h = d ) by A3, TARSKI:def_2; ( g = a or g = b ) by A2, TARSKI:def_2; hence x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} by A1, A4, ENUMSET1:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} or x in {a,b} |^ {c,d} ) A5: ( c in {c,d} & d in {c,d} ) by TARSKI:def_2; assume x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} ; ::_thesis: x in {a,b} |^ {c,d} then A6: ( x = a |^ c or x = a |^ d or x = b |^ c or x = b |^ d ) by ENUMSET1:def_2; ( a in {a,b} & b in {a,b} ) by TARSKI:def_2; hence x in {a,b} |^ {c,d} by A6, A5; ::_thesis: verum end; definition let G be Group; let A be Subset of G; let g be Element of G; funcA |^ g -> Subset of G equals :: GROUP_3:def 4 A |^ {g}; correctness coherence A |^ {g} is Subset of G; ; funcg |^ A -> Subset of G equals :: GROUP_3:def 5 {g} |^ A; correctness coherence {g} |^ A is Subset of G; ; end; :: deftheorem defines |^ GROUP_3:def_4_:_ for G being Group for A being Subset of G for g being Element of G holds A |^ g = A |^ {g}; :: deftheorem defines |^ GROUP_3:def_5_:_ for G being Group for A being Subset of G for g being Element of G holds g |^ A = {g} |^ A; theorem Th41: :: GROUP_3:41 for x being set for G being Group for g being Element of G for A being Subset of G holds ( x in A |^ g iff ex h being Element of G st ( x = h |^ g & h in A ) ) proof let x be set ; ::_thesis: for G being Group for g being Element of G for A being Subset of G holds ( x in A |^ g iff ex h being Element of G st ( x = h |^ g & h in A ) ) let G be Group; ::_thesis: for g being Element of G for A being Subset of G holds ( x in A |^ g iff ex h being Element of G st ( x = h |^ g & h in A ) ) let g be Element of G; ::_thesis: for A being Subset of G holds ( x in A |^ g iff ex h being Element of G st ( x = h |^ g & h in A ) ) let A be Subset of G; ::_thesis: ( x in A |^ g iff ex h being Element of G st ( x = h |^ g & h in A ) ) thus ( x in A |^ g implies ex h being Element of G st ( x = h |^ g & h in A ) ) ::_thesis: ( ex h being Element of G st ( x = h |^ g & h in A ) implies x in A |^ g ) proof assume x in A |^ g ; ::_thesis: ex h being Element of G st ( x = h |^ g & h in A ) then consider a, b being Element of G such that A1: ( x = a |^ b & a in A ) and A2: b in {g} ; b = g by A2, TARSKI:def_1; hence ex h being Element of G st ( x = h |^ g & h in A ) by A1; ::_thesis: verum end; given h being Element of G such that A3: ( x = h |^ g & h in A ) ; ::_thesis: x in A |^ g g in {g} by TARSKI:def_1; hence x in A |^ g by A3; ::_thesis: verum end; theorem Th42: :: GROUP_3:42 for x being set for G being Group for g being Element of G for A being Subset of G holds ( x in g |^ A iff ex h being Element of G st ( x = g |^ h & h in A ) ) proof let x be set ; ::_thesis: for G being Group for g being Element of G for A being Subset of G holds ( x in g |^ A iff ex h being Element of G st ( x = g |^ h & h in A ) ) let G be Group; ::_thesis: for g being Element of G for A being Subset of G holds ( x in g |^ A iff ex h being Element of G st ( x = g |^ h & h in A ) ) let g be Element of G; ::_thesis: for A being Subset of G holds ( x in g |^ A iff ex h being Element of G st ( x = g |^ h & h in A ) ) let A be Subset of G; ::_thesis: ( x in g |^ A iff ex h being Element of G st ( x = g |^ h & h in A ) ) thus ( x in g |^ A implies ex h being Element of G st ( x = g |^ h & h in A ) ) ::_thesis: ( ex h being Element of G st ( x = g |^ h & h in A ) implies x in g |^ A ) proof assume x in g |^ A ; ::_thesis: ex h being Element of G st ( x = g |^ h & h in A ) then consider a, b being Element of G such that A1: x = a |^ b and A2: a in {g} and A3: b in A ; a = g by A2, TARSKI:def_1; hence ex h being Element of G st ( x = g |^ h & h in A ) by A1, A3; ::_thesis: verum end; given h being Element of G such that A4: ( x = g |^ h & h in A ) ; ::_thesis: x in g |^ A g in {g} by TARSKI:def_1; hence x in g |^ A by A4; ::_thesis: verum end; theorem :: GROUP_3:43 for G being Group for g being Element of G for A being Subset of G holds g |^ A c= ((A ") * g) * A proof let G be Group; ::_thesis: for g being Element of G for A being Subset of G holds g |^ A c= ((A ") * g) * A let g be Element of G; ::_thesis: for A being Subset of G holds g |^ A c= ((A ") * g) * A let A be Subset of G; ::_thesis: g |^ A c= ((A ") * g) * A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g |^ A or x in ((A ") * g) * A ) assume x in g |^ A ; ::_thesis: x in ((A ") * g) * A then consider a being Element of G such that A1: x = g |^ a and A2: a in A by Th42; a " in A " by A2; then (a ") * g in (A ") * g by GROUP_2:28; hence x in ((A ") * g) * A by A1, A2; ::_thesis: verum end; theorem :: GROUP_3:44 for G being Group for g being Element of G for A, B being Subset of G holds (A |^ B) |^ g = A |^ (B * g) by Th35; theorem :: GROUP_3:45 for G being Group for g being Element of G for A, B being Subset of G holds (A |^ g) |^ B = A |^ (g * B) by Th35; theorem :: GROUP_3:46 for G being Group for g being Element of G for A, B being Subset of G holds (g |^ A) |^ B = g |^ (A * B) by Th35; theorem Th47: :: GROUP_3:47 for G being Group for a, b being Element of G for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b) proof let G be Group; ::_thesis: for a, b being Element of G for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b) let a, b be Element of G; ::_thesis: for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b) let A be Subset of G; ::_thesis: (A |^ a) |^ b = A |^ (a * b) thus (A |^ a) |^ b = A |^ (a * {b}) by Th35 .= A |^ (a * b) by GROUP_2:18 ; ::_thesis: verum end; theorem :: GROUP_3:48 for G being Group for a, b being Element of G for A being Subset of G holds (a |^ A) |^ b = a |^ (A * b) by Th35; theorem :: GROUP_3:49 for G being Group for a, b being Element of G for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A) proof let G be Group; ::_thesis: for a, b being Element of G for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A) let a, b be Element of G; ::_thesis: for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A) let A be Subset of G; ::_thesis: (a |^ b) |^ A = a |^ (b * A) thus (a |^ b) |^ A = ({a} |^ {b}) |^ A by Th37 .= a |^ (b * A) by Th35 ; ::_thesis: verum end; theorem Th50: :: GROUP_3:50 for G being Group for g being Element of G for A being Subset of G holds A |^ g = ((g ") * A) * g proof let G be Group; ::_thesis: for g being Element of G for A being Subset of G holds A |^ g = ((g ") * A) * g let g be Element of G; ::_thesis: for A being Subset of G holds A |^ g = ((g ") * A) * g let A be Subset of G; ::_thesis: A |^ g = ((g ") * A) * g A |^ g c= (({g} ") * A) * {g} by Th33; hence A |^ g c= ((g ") * A) * g by GROUP_2:3; :: according to XBOOLE_0:def_10 ::_thesis: ((g ") * A) * g c= A |^ g let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((g ") * A) * g or x in A |^ g ) assume x in ((g ") * A) * g ; ::_thesis: x in A |^ g then consider a being Element of G such that A1: x = a * g and A2: a in (g ") * A by GROUP_2:28; consider b being Element of G such that A3: a = (g ") * b and A4: b in A by A2, GROUP_2:27; x = b |^ g by A1, A3; hence x in A |^ g by A4, Th41; ::_thesis: verum end; theorem :: GROUP_3:51 for G being Group for a being Element of G for A, B being Subset of G holds (A * B) |^ a c= (A |^ a) * (B |^ a) by Th34; theorem Th52: :: GROUP_3:52 for G being Group for A being Subset of G holds A |^ (1_ G) = A proof let G be Group; ::_thesis: for A being Subset of G holds A |^ (1_ G) = A let A be Subset of G; ::_thesis: A |^ (1_ G) = A thus A |^ (1_ G) = (((1_ G) ") * A) * (1_ G) by Th50 .= ((1_ G) ") * A by GROUP_2:37 .= (1_ G) * A by GROUP_1:8 .= A by GROUP_2:37 ; ::_thesis: verum end; theorem :: GROUP_3:53 for G being Group for A being Subset of G st A <> {} holds (1_ G) |^ A = {(1_ G)} proof let G be Group; ::_thesis: for A being Subset of G st A <> {} holds (1_ G) |^ A = {(1_ G)} let A be Subset of G; ::_thesis: ( A <> {} implies (1_ G) |^ A = {(1_ G)} ) set y = the Element of A; assume A1: A <> {} ; ::_thesis: (1_ G) |^ A = {(1_ G)} then reconsider y = the Element of A as Element of G by TARSKI:def_3; thus (1_ G) |^ A c= {(1_ G)} :: according to XBOOLE_0:def_10 ::_thesis: {(1_ G)} c= (1_ G) |^ A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (1_ G) |^ A or x in {(1_ G)} ) assume x in (1_ G) |^ A ; ::_thesis: x in {(1_ G)} then ex a being Element of G st ( x = (1_ G) |^ a & a in A ) by Th42; then x = 1_ G by Th17; hence x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(1_ G)} or x in (1_ G) |^ A ) assume x in {(1_ G)} ; ::_thesis: x in (1_ G) |^ A then x = 1_ G by TARSKI:def_1; then (1_ G) |^ y = x by Th17; hence x in (1_ G) |^ A by A1, Th42; ::_thesis: verum end; theorem Th54: :: GROUP_3:54 for G being Group for a being Element of G for A being Subset of G holds ( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A ) proof let G be Group; ::_thesis: for a being Element of G for A being Subset of G holds ( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A ) let a be Element of G; ::_thesis: for A being Subset of G holds ( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A ) let A be Subset of G; ::_thesis: ( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A ) thus (A |^ a) |^ (a ") = A |^ (a * (a ")) by Th47 .= A |^ (1_ G) by GROUP_1:def_5 .= A by Th52 ; ::_thesis: (A |^ (a ")) |^ a = A thus (A |^ (a ")) |^ a = A |^ ((a ") * a) by Th47 .= A |^ (1_ G) by GROUP_1:def_5 .= A by Th52 ; ::_thesis: verum end; theorem Th55: :: GROUP_3:55 for G being Group holds ( G is commutative Group iff for A, B being Subset of G st B <> {} holds A |^ B = A ) proof let G be Group; ::_thesis: ( G is commutative Group iff for A, B being Subset of G st B <> {} holds A |^ B = A ) thus ( G is commutative Group implies for A, B being Subset of G st B <> {} holds A |^ B = A ) ::_thesis: ( ( for A, B being Subset of G st B <> {} holds A |^ B = A ) implies G is commutative Group ) proof assume A1: G is commutative Group ; ::_thesis: for A, B being Subset of G st B <> {} holds A |^ B = A let A, B be Subset of G; ::_thesis: ( B <> {} implies A |^ B = A ) set y = the Element of B; assume A2: B <> {} ; ::_thesis: A |^ B = A then reconsider y = the Element of B as Element of G by TARSKI:def_3; thus A |^ B c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= A |^ B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ B or x in A ) assume x in A |^ B ; ::_thesis: x in A then ex a, b being Element of G st ( x = a |^ b & a in A & b in B ) ; hence x in A by A1, Th29; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A |^ B ) assume A3: x in A ; ::_thesis: x in A |^ B then reconsider a = x as Element of G ; a |^ y = x by A1, Th29; hence x in A |^ B by A2, A3; ::_thesis: verum end; assume A4: for A, B being Subset of G st B <> {} holds A |^ B = A ; ::_thesis: G is commutative Group now__::_thesis:_for_a,_b_being_Element_of_G_holds_a_=_a_|^_b let a, b be Element of G; ::_thesis: a = a |^ b {a} = {a} |^ {b} by A4 .= {(a |^ b)} by Th37 ; hence a = a |^ b by ZFMISC_1:3; ::_thesis: verum end; hence G is commutative Group by Th30; ::_thesis: verum end; theorem :: GROUP_3:56 for G being Group holds ( G is commutative Group iff for A being Subset of G for g being Element of G holds A |^ g = A ) proof let G be Group; ::_thesis: ( G is commutative Group iff for A being Subset of G for g being Element of G holds A |^ g = A ) thus ( G is commutative Group implies for A being Subset of G for g being Element of G holds A |^ g = A ) by Th55; ::_thesis: ( ( for A being Subset of G for g being Element of G holds A |^ g = A ) implies G is commutative Group ) assume A1: for A being Subset of G for g being Element of G holds A |^ g = A ; ::_thesis: G is commutative Group now__::_thesis:_for_a,_b_being_Element_of_G_holds_a_=_a_|^_b let a, b be Element of G; ::_thesis: a = a |^ b {a} = {a} |^ b by A1 .= {(a |^ b)} by Th37 ; hence a = a |^ b by ZFMISC_1:3; ::_thesis: verum end; hence G is commutative Group by Th30; ::_thesis: verum end; theorem :: GROUP_3:57 for G being Group holds ( G is commutative Group iff for A being Subset of G for g being Element of G st A <> {} holds g |^ A = {g} ) proof let G be Group; ::_thesis: ( G is commutative Group iff for A being Subset of G for g being Element of G st A <> {} holds g |^ A = {g} ) thus ( G is commutative Group implies for A being Subset of G for g being Element of G st A <> {} holds g |^ A = {g} ) by Th55; ::_thesis: ( ( for A being Subset of G for g being Element of G st A <> {} holds g |^ A = {g} ) implies G is commutative Group ) assume A1: for A being Subset of G for g being Element of G st A <> {} holds g |^ A = {g} ; ::_thesis: G is commutative Group now__::_thesis:_for_a,_b_being_Element_of_G_holds_a_=_a_|^_b let a, b be Element of G; ::_thesis: a = a |^ b {a} = a |^ {b} by A1 .= {(a |^ b)} by Th37 ; hence a = a |^ b by ZFMISC_1:3; ::_thesis: verum end; hence G is commutative Group by Th30; ::_thesis: verum end; definition let G be Group; let H be Subgroup of G; let a be Element of G; funcH |^ a -> strict Subgroup of G means :Def6: :: GROUP_3:def 6 the carrier of it = (carr H) |^ a; existence ex b1 being strict Subgroup of G st the carrier of b1 = (carr H) |^ a proof consider H1 being strict Subgroup of G such that A1: the carrier of H1 = ((a ") * H) * ((a ") ") by GROUP_2:127; the carrier of H1 = ((a ") * (carr H)) * a by A1 .= (carr H) |^ a by Th50 ; hence ex b1 being strict Subgroup of G st the carrier of b1 = (carr H) |^ a ; ::_thesis: verum end; correctness uniqueness for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H) |^ a & the carrier of b2 = (carr H) |^ a holds b1 = b2; by GROUP_2:59; end; :: deftheorem Def6 defines |^ GROUP_3:def_6_:_ for G being Group for H being Subgroup of G for a being Element of G for b4 being strict Subgroup of G holds ( b4 = H |^ a iff the carrier of b4 = (carr H) |^ a ); theorem Th58: :: GROUP_3:58 for x being set for G being Group for a being Element of G for H being Subgroup of G holds ( x in H |^ a iff ex g being Element of G st ( x = g |^ a & g in H ) ) proof let x be set ; ::_thesis: for G being Group for a being Element of G for H being Subgroup of G holds ( x in H |^ a iff ex g being Element of G st ( x = g |^ a & g in H ) ) let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( x in H |^ a iff ex g being Element of G st ( x = g |^ a & g in H ) ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( x in H |^ a iff ex g being Element of G st ( x = g |^ a & g in H ) ) let H be Subgroup of G; ::_thesis: ( x in H |^ a iff ex g being Element of G st ( x = g |^ a & g in H ) ) thus ( x in H |^ a implies ex g being Element of G st ( x = g |^ a & g in H ) ) ::_thesis: ( ex g being Element of G st ( x = g |^ a & g in H ) implies x in H |^ a ) proof assume x in H |^ a ; ::_thesis: ex g being Element of G st ( x = g |^ a & g in H ) then x in the carrier of (H |^ a) by STRUCT_0:def_5; then x in (carr H) |^ a by Def6; then consider b being Element of G such that A1: ( x = b |^ a & b in carr H ) by Th41; take b ; ::_thesis: ( x = b |^ a & b in H ) thus ( x = b |^ a & b in H ) by A1, STRUCT_0:def_5; ::_thesis: verum end; given g being Element of G such that A2: x = g |^ a and A3: g in H ; ::_thesis: x in H |^ a g in carr H by A3, STRUCT_0:def_5; then x in (carr H) |^ a by A2, Th41; then x in the carrier of (H |^ a) by Def6; hence x in H |^ a by STRUCT_0:def_5; ::_thesis: verum end; theorem Th59: :: GROUP_3:59 for G being Group for a being Element of G for H being Subgroup of G holds the carrier of (H |^ a) = ((a ") * H) * a proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds the carrier of (H |^ a) = ((a ") * H) * a let a be Element of G; ::_thesis: for H being Subgroup of G holds the carrier of (H |^ a) = ((a ") * H) * a let H be Subgroup of G; ::_thesis: the carrier of (H |^ a) = ((a ") * H) * a thus the carrier of (H |^ a) = (carr H) |^ a by Def6 .= ((a ") * H) * a by Th50 ; ::_thesis: verum end; theorem Th60: :: GROUP_3:60 for G being Group for a, b being Element of G for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b) proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b) let a, b be Element of G; ::_thesis: for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b) let H be Subgroup of G; ::_thesis: (H |^ a) |^ b = H |^ (a * b) the carrier of ((H |^ a) |^ b) = (carr (H |^ a)) |^ b by Def6 .= ((carr H) |^ a) |^ b by Def6 .= (carr H) |^ (a * b) by Th47 .= the carrier of (H |^ (a * b)) by Def6 ; hence (H |^ a) |^ b = H |^ (a * b) by GROUP_2:59; ::_thesis: verum end; theorem Th61: :: GROUP_3:61 for G being Group for H being strict Subgroup of G holds H |^ (1_ G) = H proof let G be Group; ::_thesis: for H being strict Subgroup of G holds H |^ (1_ G) = H let H be strict Subgroup of G; ::_thesis: H |^ (1_ G) = H the carrier of (H |^ (1_ G)) = (carr H) |^ (1_ G) by Def6 .= the carrier of H by Th52 ; hence H |^ (1_ G) = H by GROUP_2:59; ::_thesis: verum end; theorem Th62: :: GROUP_3:62 for G being Group for a being Element of G for H being strict Subgroup of G holds ( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H ) proof let G be Group; ::_thesis: for a being Element of G for H being strict Subgroup of G holds ( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H ) let a be Element of G; ::_thesis: for H being strict Subgroup of G holds ( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H ) let H be strict Subgroup of G; ::_thesis: ( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H ) thus (H |^ a) |^ (a ") = H |^ (a * (a ")) by Th60 .= H |^ (1_ G) by GROUP_1:def_5 .= H by Th61 ; ::_thesis: (H |^ (a ")) |^ a = H thus (H |^ (a ")) |^ a = H |^ ((a ") * a) by Th60 .= H |^ (1_ G) by GROUP_1:def_5 .= H by Th61 ; ::_thesis: verum end; theorem Th63: :: GROUP_3:63 for G being Group for a being Element of G for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a) proof let G be Group; ::_thesis: for a being Element of G for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a) let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a) let H1, H2 be Subgroup of G; ::_thesis: (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a) let g be Element of G; :: according to GROUP_2:def_6 ::_thesis: ( ( not g in (H1 /\ H2) |^ a or g in (H1 |^ a) /\ (H2 |^ a) ) & ( not g in (H1 |^ a) /\ (H2 |^ a) or g in (H1 /\ H2) |^ a ) ) thus ( g in (H1 /\ H2) |^ a implies g in (H1 |^ a) /\ (H2 |^ a) ) ::_thesis: ( not g in (H1 |^ a) /\ (H2 |^ a) or g in (H1 /\ H2) |^ a ) proof assume g in (H1 /\ H2) |^ a ; ::_thesis: g in (H1 |^ a) /\ (H2 |^ a) then consider h being Element of G such that A1: g = h |^ a and A2: h in H1 /\ H2 by Th58; h in H2 by A2, GROUP_2:82; then A3: g in H2 |^ a by A1, Th58; h in H1 by A2, GROUP_2:82; then g in H1 |^ a by A1, Th58; hence g in (H1 |^ a) /\ (H2 |^ a) by A3, GROUP_2:82; ::_thesis: verum end; assume A4: g in (H1 |^ a) /\ (H2 |^ a) ; ::_thesis: g in (H1 /\ H2) |^ a then g in H1 |^ a by GROUP_2:82; then consider b being Element of G such that A5: g = b |^ a and A6: b in H1 by Th58; g in H2 |^ a by A4, GROUP_2:82; then consider c being Element of G such that A7: g = c |^ a and A8: c in H2 by Th58; b = c by A5, A7, Th16; then b in H1 /\ H2 by A6, A8, GROUP_2:82; hence g in (H1 /\ H2) |^ a by A5, Th58; ::_thesis: verum end; theorem Th64: :: GROUP_3:64 for G being Group for a being Element of G for H being Subgroup of G holds card H = card (H |^ a) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds card H = card (H |^ a) let a be Element of G; ::_thesis: for H being Subgroup of G holds card H = card (H |^ a) let H be Subgroup of G; ::_thesis: card H = card (H |^ a) deffunc H1( Element of G) -> Element of G = \$1 |^ a; consider f being Function of the carrier of G, the carrier of G such that A1: for g being Element of G holds f . g = H1(g) from FUNCT_2:sch_4(); set g = f | the carrier of H; A2: ( dom f = the carrier of G & the carrier of H c= the carrier of G ) by FUNCT_2:def_1, GROUP_2:def_5; then A3: dom (f | the carrier of H) = the carrier of H by RELAT_1:62; A4: rng (f | the carrier of H) = the carrier of (H |^ a) proof thus rng (f | the carrier of H) c= the carrier of (H |^ a) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (H |^ a) c= rng (f | the carrier of H) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f | the carrier of H) or x in the carrier of (H |^ a) ) assume x in rng (f | the carrier of H) ; ::_thesis: x in the carrier of (H |^ a) then consider y being set such that A5: y in dom (f | the carrier of H) and A6: (f | the carrier of H) . y = x by FUNCT_1:def_3; reconsider y = y as Element of H by A2, A5, RELAT_1:62; reconsider y = y as Element of G by GROUP_2:42; A7: f . y = (f | the carrier of H) . y by A5, FUNCT_1:47; f . y = y |^ a by A1; then x in (carr H) |^ a by A6, A7, Th41; hence x in the carrier of (H |^ a) by Def6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (H |^ a) or x in rng (f | the carrier of H) ) assume x in the carrier of (H |^ a) ; ::_thesis: x in rng (f | the carrier of H) then x in (carr H) |^ a by Def6; then consider b being Element of G such that A8: x = b |^ a and A9: b in carr H by Th41; A10: f . b = b |^ a by A1; (f | the carrier of H) . b = f . b by A3, A9, FUNCT_1:47; hence x in rng (f | the carrier of H) by A3, A8, A9, A10, FUNCT_1:def_3; ::_thesis: verum end; f | the carrier of H is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom (f | the carrier of H) or not b1 in dom (f | the carrier of H) or not (f | the carrier of H) . x = (f | the carrier of H) . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom (f | the carrier of H) or not y in dom (f | the carrier of H) or not (f | the carrier of H) . x = (f | the carrier of H) . y or x = y ) assume that A11: x in dom (f | the carrier of H) and A12: y in dom (f | the carrier of H) and A13: (f | the carrier of H) . x = (f | the carrier of H) . y ; ::_thesis: x = y reconsider b = x, c = y as Element of H by A2, A11, A12, RELAT_1:62; reconsider b = b, c = c as Element of G by GROUP_2:42; A14: ( f . x = b |^ a & f . y = c |^ a ) by A1; f . x = (f | the carrier of H) . x by A11, FUNCT_1:47; hence x = y by A12, A13, A14, Th16, FUNCT_1:47; ::_thesis: verum end; then the carrier of H, the carrier of (H |^ a) are_equipotent by A3, A4, WELLORD2:def_4; hence card H = card (H |^ a) by CARD_1:5; ::_thesis: verum end; theorem Th65: :: GROUP_3:65 for G being Group for a being Element of G for H being Subgroup of G holds ( H is finite iff H |^ a is finite ) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( H is finite iff H |^ a is finite ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( H is finite iff H |^ a is finite ) let H be Subgroup of G; ::_thesis: ( H is finite iff H |^ a is finite ) card H = card (H |^ a) by Th64; then the carrier of H, the carrier of (H |^ a) are_equipotent by CARD_1:5; hence ( H is finite iff H |^ a is finite ) by CARD_1:38; ::_thesis: verum end; registration let G be Group; let a be Element of G; let H be finite Subgroup of G; clusterH |^ a -> finite strict ; coherence H |^ a is finite by Th65; end; theorem :: GROUP_3:66 for G being Group for a being Element of G for H being finite Subgroup of G holds card H = card (H |^ a) by Th64; theorem Th67: :: GROUP_3:67 for G being Group for a being Element of G holds ((1). G) |^ a = (1). G proof let G be Group; ::_thesis: for a being Element of G holds ((1). G) |^ a = (1). G let a be Element of G; ::_thesis: ((1). G) |^ a = (1). G A1: the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7; the carrier of (((1). G) |^ a) = (carr ((1). G)) |^ a by Def6 .= {((1_ G) |^ a)} by A1, Th37 .= {(1_ G)} by Th17 ; hence ((1). G) |^ a = (1). G by GROUP_2:def_7; ::_thesis: verum end; theorem :: GROUP_3:68 for G being Group for a being Element of G for H being strict Subgroup of G st H |^ a = (1). G holds H = (1). G proof let G be Group; ::_thesis: for a being Element of G for H being strict Subgroup of G st H |^ a = (1). G holds H = (1). G let a be Element of G; ::_thesis: for H being strict Subgroup of G st H |^ a = (1). G holds H = (1). G let H be strict Subgroup of G; ::_thesis: ( H |^ a = (1). G implies H = (1). G ) assume A1: H |^ a = (1). G ; ::_thesis: H = (1). G then reconsider H = H as finite Subgroup of G by Th65; card ((1). G) = 1 by GROUP_2:69; then card H = 1 by A1, Th64; hence H = (1). G by GROUP_2:70; ::_thesis: verum end; theorem Th69: :: GROUP_3:69 for G being Group for a being Element of G holds ((Omega). G) |^ a = (Omega). G proof let G be Group; ::_thesis: for a being Element of G holds ((Omega). G) |^ a = (Omega). G let a be Element of G; ::_thesis: ((Omega). G) |^ a = (Omega). G let h be Element of G; :: according to GROUP_2:def_6 ::_thesis: ( ( not h in ((Omega). G) |^ a or h in (Omega). G ) & ( not h in (Omega). G or h in ((Omega). G) |^ a ) ) (h |^ (a ")) |^ a = h |^ ((a ") * a) by Th24 .= h |^ (1_ G) by GROUP_1:def_5 .= h by Th19 ; hence ( ( not h in ((Omega). G) |^ a or h in (Omega). G ) & ( not h in (Omega). G or h in ((Omega). G) |^ a ) ) by Th58, STRUCT_0:def_5; ::_thesis: verum end; theorem :: GROUP_3:70 for G being Group for a being Element of G for H being strict Subgroup of G st H |^ a = G holds H = G proof let G be Group; ::_thesis: for a being Element of G for H being strict Subgroup of G st H |^ a = G holds H = G let a be Element of G; ::_thesis: for H being strict Subgroup of G st H |^ a = G holds H = G let H be strict Subgroup of G; ::_thesis: ( H |^ a = G implies H = G ) assume A1: H |^ a = G ; ::_thesis: H = G now__::_thesis:_for_g_being_Element_of_G_holds_g_in_H let g be Element of G; ::_thesis: g in H assume A2: not g in H ; ::_thesis: contradiction now__::_thesis:_not_g_|^_a_in_H_|^_a assume g |^ a in H |^ a ; ::_thesis: contradiction then ex h being Element of G st ( g |^ a = h |^ a & h in H ) by Th58; hence contradiction by A2, Th16; ::_thesis: verum end; hence contradiction by A1, STRUCT_0:def_5; ::_thesis: verum end; hence H = G by A1, GROUP_2:62; ::_thesis: verum end; theorem Th71: :: GROUP_3:71 for G being Group for a being Element of G for H being Subgroup of G holds Index H = Index (H |^ a) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds Index H = Index (H |^ a) let a be Element of G; ::_thesis: for H being Subgroup of G holds Index H = Index (H |^ a) let H be Subgroup of G; ::_thesis: Index H = Index (H |^ a) defpred S1[ set , set ] means ex b being Element of G st ( \$1 = b * H & \$2 = (b |^ a) * (H |^ a) ); A1: for x being set st x in Left_Cosets H holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Left_Cosets H implies ex y being set st S1[x,y] ) assume x in Left_Cosets H ; ::_thesis: ex y being set st S1[x,y] then consider b being Element of G such that A2: x = b * H by GROUP_2:def_15; reconsider y = (b |^ a) * (H |^ a) as set ; take y ; ::_thesis: S1[x,y] take b ; ::_thesis: ( x = b * H & y = (b |^ a) * (H |^ a) ) thus ( x = b * H & y = (b |^ a) * (H |^ a) ) by A2; ::_thesis: verum end; consider f being Function such that A3: dom f = Left_Cosets H and A4: for x being set st x in Left_Cosets H holds S1[x,f . x] from CLASSES1:sch_1(A1); A5: for x, y1, y2 being set st x in Left_Cosets H & S1[x,y1] & S1[x,y2] holds y1 = y2 proof set A = carr H; let x, y1, y2 be set ; ::_thesis: ( x in Left_Cosets H & S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume x in Left_Cosets H ; ::_thesis: ( not S1[x,y1] or not S1[x,y2] or y1 = y2 ) given b being Element of G such that A6: x = b * H and A7: y1 = (b |^ a) * (H |^ a) ; ::_thesis: ( not S1[x,y2] or y1 = y2 ) given c being Element of G such that A8: x = c * H and A9: y2 = (c |^ a) * (H |^ a) ; ::_thesis: y1 = y2 thus y1 = (((a ") * b) * a) * (((a ") * H) * a) by A7, Th59 .= ((((a ") * b) * a) * ((a ") * (carr H))) * a by GROUP_2:33 .= (((a ") * b) * (a * ((a ") * (carr H)))) * a by GROUP_2:32 .= (((a ") * b) * ((a * (a ")) * (carr H))) * a by GROUP_2:32 .= (((a ") * b) * ((1_ G) * (carr H))) * a by GROUP_1:def_5 .= (((a ") * b) * (carr H)) * a by GROUP_2:37 .= ((a ") * (c * H)) * a by A6, A8, GROUP_2:32 .= (((a ") * c) * (carr H)) * a by GROUP_2:32 .= (((a ") * c) * ((1_ G) * (carr H))) * a by GROUP_2:37 .= (((a ") * c) * ((a * (a ")) * (carr H))) * a by GROUP_1:def_5 .= (((a ") * c) * (a * ((a ") * (carr H)))) * a by GROUP_2:32 .= ((((a ") * c) * a) * ((a ") * (carr H))) * a by GROUP_2:32 .= (((a ") * c) * a) * (((a ") * H) * a) by GROUP_2:33 .= y2 by A9, Th59 ; ::_thesis: verum end; A10: rng f = Left_Cosets (H |^ a) proof thus rng f c= Left_Cosets (H |^ a) :: according to XBOOLE_0:def_10 ::_thesis: Left_Cosets (H |^ a) c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Left_Cosets (H |^ a) ) assume x in rng f ; ::_thesis: x in Left_Cosets (H |^ a) then consider y being set such that A11: ( y in dom f & f . y = x ) by FUNCT_1:def_3; ex b being Element of G st ( y = b * H & x = (b |^ a) * (H |^ a) ) by A3, A4, A11; hence x in Left_Cosets (H |^ a) by GROUP_2:def_15; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets (H |^ a) or x in rng f ) assume x in Left_Cosets (H |^ a) ; ::_thesis: x in rng f then consider b being Element of G such that A12: x = b * (H |^ a) by GROUP_2:def_15; set c = b |^ (a "); A13: x = ((b |^ (a ")) |^ a) * (H |^ a) by A12, Th25; A14: (b |^ (a ")) * H in Left_Cosets H by GROUP_2:def_15; then consider d being Element of G such that A15: (b |^ (a ")) * H = d * H and A16: f . ((b |^ (a ")) * H) = (d |^ a) * (H |^ a) by A4; ((b |^ (a ")) |^ a) * (H |^ a) = (d |^ a) * (H |^ a) by A5, A14, A15; hence x in rng f by A3, A13, A14, A16, FUNCT_1:def_3; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A17: x in dom f and A18: y in dom f and A19: f . x = f . y ; ::_thesis: x = y consider c being Element of G such that A20: y = c * H and A21: f . y = (c |^ a) * (H |^ a) by A3, A4, A18; consider b being Element of G such that A22: x = b * H and A23: f . x = (b |^ a) * (H |^ a) by A3, A4, A17; A24: ((c |^ a) ") * (b |^ a) = ((c ") |^ a) * (b |^ a) by Th26 .= ((c ") * b) |^ a by Th23 ; ((c |^ a) ") * (b |^ a) in H |^ a by A19, A23, A21, GROUP_2:114; then consider d being Element of G such that A25: ((c ") * b) |^ a = d |^ a and A26: d in H by A24, Th58; (c ") * b = d by A25, Th16; hence x = y by A22, A20, A26, GROUP_2:114; ::_thesis: verum end; then Left_Cosets H, Left_Cosets (H |^ a) are_equipotent by A3, A10, WELLORD2:def_4; hence Index H = Index (H |^ a) by CARD_1:5; ::_thesis: verum end; theorem :: GROUP_3:72 for G being Group for a being Element of G for H being Subgroup of G st Left_Cosets H is finite holds index H = index (H |^ a) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G st Left_Cosets H is finite holds index H = index (H |^ a) let a be Element of G; ::_thesis: for H being Subgroup of G st Left_Cosets H is finite holds index H = index (H |^ a) let H be Subgroup of G; ::_thesis: ( Left_Cosets H is finite implies index H = index (H |^ a) ) assume A1: Left_Cosets H is finite ; ::_thesis: index H = index (H |^ a) then A2: ex B being finite set st ( B = Left_Cosets H & index H = card B ) by GROUP_2:def_18; A3: Index H = Index (H |^ a) by Th71; then Left_Cosets H, Left_Cosets (H |^ a) are_equipotent by CARD_1:5; then Left_Cosets (H |^ a) is finite by A1, CARD_1:38; hence index H = index (H |^ a) by A2, A3, GROUP_2:def_18; ::_thesis: verum end; theorem Th73: :: GROUP_3:73 for G being Group st G is commutative Group holds for H being strict Subgroup of G for a being Element of G holds H |^ a = H proof let G be Group; ::_thesis: ( G is commutative Group implies for H being strict Subgroup of G for a being Element of G holds H |^ a = H ) assume A1: G is commutative Group ; ::_thesis: for H being strict Subgroup of G for a being Element of G holds H |^ a = H let H be strict Subgroup of G; ::_thesis: for a being Element of G holds H |^ a = H let a be Element of G; ::_thesis: H |^ a = H the carrier of (H |^ a) = ((a ") * H) * a by Th59 .= (H * (a ")) * a by A1, GROUP_2:112 .= H * ((a ") * a) by GROUP_2:107 .= H * (1_ G) by GROUP_1:def_5 .= the carrier of H by GROUP_2:109 ; hence H |^ a = H by GROUP_2:59; ::_thesis: verum end; definition let G be Group; let a, b be Element of G; preda,b are_conjugated means :Def7: :: GROUP_3:def 7 ex g being Element of G st a = b |^ g; end; :: deftheorem Def7 defines are_conjugated GROUP_3:def_7_:_ for G being Group for a, b being Element of G holds ( a,b are_conjugated iff ex g being Element of G st a = b |^ g ); notation let G be Group; let a, b be Element of G; antonym a,b are_not_conjugated for a,b are_conjugated ; end; theorem Th74: :: GROUP_3:74 for G being Group for a, b being Element of G holds ( a,b are_conjugated iff ex g being Element of G st b = a |^ g ) proof let G be Group; ::_thesis: for a, b being Element of G holds ( a,b are_conjugated iff ex g being Element of G st b = a |^ g ) let a, b be Element of G; ::_thesis: ( a,b are_conjugated iff ex g being Element of G st b = a |^ g ) thus ( a,b are_conjugated implies ex g being Element of G st b = a |^ g ) ::_thesis: ( ex g being Element of G st b = a |^ g implies a,b are_conjugated ) proof given g being Element of G such that A1: a = b |^ g ; :: according to GROUP_3:def_7 ::_thesis: ex g being Element of G st b = a |^ g a |^ (g ") = b by A1, Th25; hence ex g being Element of G st b = a |^ g ; ::_thesis: verum end; given g being Element of G such that A2: b = a |^ g ; ::_thesis: a,b are_conjugated a = b |^ (g ") by A2, Th25; hence a,b are_conjugated by Def7; ::_thesis: verum end; theorem Th75: :: GROUP_3:75 for G being Group for a being Element of G holds a,a are_conjugated proof let G be Group; ::_thesis: for a being Element of G holds a,a are_conjugated let a be Element of G; ::_thesis: a,a are_conjugated take 1_ G ; :: according to GROUP_3:def_7 ::_thesis: a = a |^ (1_ G) thus a = a |^ (1_ G) by Th19; ::_thesis: verum end; theorem Th76: :: GROUP_3:76 for G being Group for a, b being Element of G st a,b are_conjugated holds b,a are_conjugated proof let G be Group; ::_thesis: for a, b being Element of G st a,b are_conjugated holds b,a are_conjugated let a, b be Element of G; ::_thesis: ( a,b are_conjugated implies b,a are_conjugated ) given g being Element of G such that A1: a = b |^ g ; :: according to GROUP_3:def_7 ::_thesis: b,a are_conjugated b = a |^ (g ") by A1, Th25; hence b,a are_conjugated by Def7; ::_thesis: verum end; definition let G be Group; let a, b be Element of G; :: original: are_conjugated redefine preda,b are_conjugated ; reflexivity for a being Element of G holds (G,b1,b1) by Th75; symmetry for a, b being Element of G st (G,b1,b2) holds (G,b2,b1) by Th76; end; theorem Th77: :: GROUP_3:77 for G being Group for a, b, c being Element of G st a,b are_conjugated & b,c are_conjugated holds a,c are_conjugated proof let G be Group; ::_thesis: for a, b, c being Element of G st a,b are_conjugated & b,c are_conjugated holds a,c are_conjugated let a, b, c be Element of G; ::_thesis: ( a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated ) given g being Element of G such that A1: a = b |^ g ; :: according to GROUP_3:def_7 ::_thesis: ( not b,c are_conjugated or a,c are_conjugated ) given h being Element of G such that A2: b = c |^ h ; :: according to GROUP_3:def_7 ::_thesis: a,c are_conjugated a = c |^ (h * g) by A1, A2, Th24; hence a,c are_conjugated by Def7; ::_thesis: verum end; theorem Th78: :: GROUP_3:78 for G being Group for a being Element of G st ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) holds a = 1_ G proof let G be Group; ::_thesis: for a being Element of G st ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) holds a = 1_ G let a be Element of G; ::_thesis: ( ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) implies a = 1_ G ) assume A1: ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) ; ::_thesis: a = 1_ G now__::_thesis:_a_=_1__G percases ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) by A1; suppose a, 1_ G are_conjugated ; ::_thesis: a = 1_ G then ex g being Element of G st 1_ G = a |^ g by Th74; hence a = 1_ G by Th18; ::_thesis: verum end; suppose 1_ G,a are_conjugated ; ::_thesis: a = 1_ G then ex g being Element of G st 1_ G = a |^ g by Def7; hence a = 1_ G by Th18; ::_thesis: verum end; end; end; hence a = 1_ G ; ::_thesis: verum end; theorem Th79: :: GROUP_3:79 for G being Group for a being Element of G holds a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated } proof let G be Group; ::_thesis: for a being Element of G holds a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated } let a be Element of G; ::_thesis: a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated } set A = a |^ (carr ((Omega). G)); set B = { b where b is Element of G : a,b are_conjugated } ; thus a |^ (carr ((Omega). G)) c= { b where b is Element of G : a,b are_conjugated } :: according to XBOOLE_0:def_10 ::_thesis: { b where b is Element of G : a,b are_conjugated } c= a |^ (carr ((Omega). G)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a |^ (carr ((Omega). G)) or x in { b where b is Element of G : a,b are_conjugated } ) assume A1: x in a |^ (carr ((Omega). G)) ; ::_thesis: x in { b where b is Element of G : a,b are_conjugated } then reconsider b = x as Element of G ; ex g being Element of G st ( x = a |^ g & g in carr ((Omega). G) ) by A1, Th42; then b,a are_conjugated by Def7; hence x in { b where b is Element of G : a,b are_conjugated } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { b where b is Element of G : a,b are_conjugated } or x in a |^ (carr ((Omega). G)) ) assume x in { b where b is Element of G : a,b are_conjugated } ; ::_thesis: x in a |^ (carr ((Omega). G)) then consider b being Element of G such that A2: x = b and A3: a,b are_conjugated ; ex g being Element of G st b = a |^ g by A3, Def7; hence x in a |^ (carr ((Omega). G)) by A2, Th42; ::_thesis: verum end; definition let G be Group; let a be Element of G; func con_class a -> Subset of G equals :: GROUP_3:def 8 a |^ (carr ((Omega). G)); correctness coherence a |^ (carr ((Omega). G)) is Subset of G; ; end; :: deftheorem defines con_class GROUP_3:def_8_:_ for G being Group for a being Element of G holds con_class a = a |^ (carr ((Omega). G)); theorem Th80: :: GROUP_3:80 for x being set for G being Group for a being Element of G holds ( x in con_class a iff ex b being Element of G st ( b = x & a,b are_conjugated ) ) proof let x be set ; ::_thesis: for G being Group for a being Element of G holds ( x in con_class a iff ex b being Element of G st ( b = x & a,b are_conjugated ) ) let G be Group; ::_thesis: for a being Element of G holds ( x in con_class a iff ex b being Element of G st ( b = x & a,b are_conjugated ) ) let a be Element of G; ::_thesis: ( x in con_class a iff ex b being Element of G st ( b = x & a,b are_conjugated ) ) thus ( x in con_class a implies ex b being Element of G st ( b = x & a,b are_conjugated ) ) ::_thesis: ( ex b being Element of G st ( b = x & a,b are_conjugated ) implies x in con_class a ) proof assume x in con_class a ; ::_thesis: ex b being Element of G st ( b = x & a,b are_conjugated ) then x in { b where b is Element of G : a,b are_conjugated } by Th79; hence ex b being Element of G st ( b = x & a,b are_conjugated ) ; ::_thesis: verum end; given b being Element of G such that A1: ( b = x & a,b are_conjugated ) ; ::_thesis: x in con_class a x in { c where c is Element of G : a,c are_conjugated } by A1; hence x in con_class a by Th79; ::_thesis: verum end; theorem Th81: :: GROUP_3:81 for G being Group for a, b being Element of G holds ( a in con_class b iff a,b are_conjugated ) proof let G be Group; ::_thesis: for a, b being Element of G holds ( a in con_class b iff a,b are_conjugated ) let a, b be Element of G; ::_thesis: ( a in con_class b iff a,b are_conjugated ) thus ( a in con_class b implies a,b are_conjugated ) ::_thesis: ( a,b are_conjugated implies a in con_class b ) proof assume a in con_class b ; ::_thesis: a,b are_conjugated then ex c being Element of G st ( a = c & b,c are_conjugated ) by Th80; hence a,b are_conjugated ; ::_thesis: verum end; assume a,b are_conjugated ; ::_thesis: a in con_class b hence a in con_class b by Th80; ::_thesis: verum end; theorem Th82: :: GROUP_3:82 for G being Group for a, g being Element of G holds a |^ g in con_class a proof let G be Group; ::_thesis: for a, g being Element of G holds a |^ g in con_class a let a, g be Element of G; ::_thesis: a |^ g in con_class a a,a |^ g are_conjugated by Th74; hence a |^ g in con_class a by Th80; ::_thesis: verum end; theorem :: GROUP_3:83 for G being Group for a being Element of G holds a in con_class a by Th81; theorem :: GROUP_3:84 for G being Group for a, b being Element of G st a in con_class b holds b in con_class a proof let G be Group; ::_thesis: for a, b being Element of G st a in con_class b holds b in con_class a let a, b be Element of G; ::_thesis: ( a in con_class b implies b in con_class a ) assume a in con_class b ; ::_thesis: b in con_class a then a,b are_conjugated by Th81; hence b in con_class a by Th81; ::_thesis: verum end; theorem :: GROUP_3:85 for G being Group for a, b being Element of G holds ( con_class a = con_class b iff con_class a meets con_class b ) proof let G be Group; ::_thesis: for a, b being Element of G holds ( con_class a = con_class b iff con_class a meets con_class b ) let a, b be Element of G; ::_thesis: ( con_class a = con_class b iff con_class a meets con_class b ) thus ( con_class a = con_class b implies con_class a meets con_class b ) ::_thesis: ( con_class a meets con_class b implies con_class a = con_class b ) proof assume A1: con_class a = con_class b ; ::_thesis: con_class a meets con_class b a in con_class a by Th81; hence con_class a meets con_class b by A1, XBOOLE_0:3; ::_thesis: verum end; assume con_class a meets con_class b ; ::_thesis: con_class a = con_class b then consider x being set such that A2: x in con_class a and A3: x in con_class b by XBOOLE_0:3; reconsider x = x as Element of G by A2; A4: a,x are_conjugated by A2, Th81; thus con_class a c= con_class b :: according to XBOOLE_0:def_10 ::_thesis: con_class b c= con_class a proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class a or y in con_class b ) assume y in con_class a ; ::_thesis: y in con_class b then consider g being Element of G such that A5: g = y and A6: a,g are_conjugated by Th80; A7: b,x are_conjugated by A3, Th81; x,a are_conjugated by A2, Th81; then x,g are_conjugated by A6, Th77; then b,g are_conjugated by A7, Th77; hence y in con_class b by A5, Th80; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class b or y in con_class a ) assume y in con_class b ; ::_thesis: y in con_class a then consider g being Element of G such that A8: g = y and A9: b,g are_conjugated by Th80; x,b are_conjugated by A3, Th81; then x,g are_conjugated by A9, Th77; then a,g are_conjugated by A4, Th77; hence y in con_class a by A8, Th80; ::_thesis: verum end; theorem :: GROUP_3:86 for G being Group for a being Element of G holds ( con_class a = {(1_ G)} iff a = 1_ G ) proof let G be Group; ::_thesis: for a being Element of G holds ( con_class a = {(1_ G)} iff a = 1_ G ) let a be Element of G; ::_thesis: ( con_class a = {(1_ G)} iff a = 1_ G ) thus ( con_class a = {(1_ G)} implies a = 1_ G ) ::_thesis: ( a = 1_ G implies con_class a = {(1_ G)} ) proof assume A1: con_class a = {(1_ G)} ; ::_thesis: a = 1_ G a in con_class a by Th81; hence a = 1_ G by A1, TARSKI:def_1; ::_thesis: verum end; assume A2: a = 1_ G ; ::_thesis: con_class a = {(1_ G)} thus con_class a c= {(1_ G)} :: according to XBOOLE_0:def_10 ::_thesis: {(1_ G)} c= con_class a proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class a or x in {(1_ G)} ) assume x in con_class a ; ::_thesis: x in {(1_ G)} then consider b being Element of G such that A3: b = x and A4: a,b are_conjugated by Th80; b = 1_ G by A2, A4, Th78; hence x in {(1_ G)} by A3, TARSKI:def_1; ::_thesis: verum end; 1_ G in con_class a by A2, Th81; hence {(1_ G)} c= con_class a by ZFMISC_1:31; ::_thesis: verum end; theorem :: GROUP_3:87 for G being Group for a being Element of G for A being Subset of G holds (con_class a) * A = A * (con_class a) proof let G be Group; ::_thesis: for a being Element of G for A being Subset of G holds (con_class a) * A = A * (con_class a) let a be Element of G; ::_thesis: for A being Subset of G holds (con_class a) * A = A * (con_class a) let A be Subset of G; ::_thesis: (con_class a) * A = A * (con_class a) thus (con_class a) * A c= A * (con_class a) :: according to XBOOLE_0:def_10 ::_thesis: A * (con_class a) c= (con_class a) * A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (con_class a) * A or x in A * (con_class a) ) assume x in (con_class a) * A ; ::_thesis: x in A * (con_class a) then consider b, c being Element of G such that A1: x = b * c and A2: b in con_class a and A3: c in A ; reconsider h = x as Element of G by A1; b,a are_conjugated by A2, Th81; then consider g being Element of G such that A4: b = a |^ g by Def7; h |^ (c ") = (c * ((a |^ g) * c)) * (c ") by A1, A4 .= c * (((a |^ g) * c) * (c ")) by GROUP_1:def_3 .= c * (a |^ g) by Th1 ; then A5: x = (c * (a |^ g)) |^ c by Th25 .= (c |^ c) * ((a |^ g) |^ c) by Th23 .= c * ((a |^ g) |^ c) by Th20 .= c * (a |^ (g * c)) by Th24 ; a |^ (g * c) in con_class a by Th82; hence x in A * (con_class a) by A3, A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (con_class a) or x in (con_class a) * A ) assume x in A * (con_class a) ; ::_thesis: x in (con_class a) * A then consider b, c being Element of G such that A6: x = b * c and A7: b in A and A8: c in con_class a ; reconsider h = x as Element of G by A6; c,a are_conjugated by A8, Th81; then consider g being Element of G such that A9: c = a |^ g by Def7; h |^ b = (a |^ g) * b by A6, A9, Th1; then A10: x = ((a |^ g) * b) |^ (b ") by Th25 .= ((a |^ g) |^ (b ")) * (b |^ (b ")) by Th23 .= (a |^ (g * (b "))) * (b |^ (b ")) by Th24 .= (a |^ (g * (b "))) * b by Th1 ; a |^ (g * (b ")) in con_class a by Th82; hence x in (con_class a) * A by A7, A10; ::_thesis: verum end; definition let G be Group; let A, B be Subset of G; predA,B are_conjugated means :Def9: :: GROUP_3:def 9 ex g being Element of G st A = B |^ g; end; :: deftheorem Def9 defines are_conjugated GROUP_3:def_9_:_ for G being Group for A, B being Subset of G holds ( A,B are_conjugated iff ex g being Element of G st A = B |^ g ); notation let G be Group; let A, B be Subset of G; antonym A,B are_not_conjugated for A,B are_conjugated ; end; theorem Th88: :: GROUP_3:88 for G being Group for A, B being Subset of G holds ( A,B are_conjugated iff ex g being Element of G st B = A |^ g ) proof let G be Group; ::_thesis: for A, B being Subset of G holds ( A,B are_conjugated iff ex g being Element of G st B = A |^ g ) let A, B be Subset of G; ::_thesis: ( A,B are_conjugated iff ex g being Element of G st B = A |^ g ) thus ( A,B are_conjugated implies ex g being Element of G st B = A |^ g ) ::_thesis: ( ex g being Element of G st B = A |^ g implies A,B are_conjugated ) proof given g being Element of G such that A1: A = B |^ g ; :: according to GROUP_3:def_9 ::_thesis: ex g being Element of G st B = A |^ g A |^ (g ") = B by A1, Th54; hence ex g being Element of G st B = A |^ g ; ::_thesis: verum end; given g being Element of G such that A2: B = A |^ g ; ::_thesis: A,B are_conjugated A = B |^ (g ") by A2, Th54; hence A,B are_conjugated by Def9; ::_thesis: verum end; theorem Th89: :: GROUP_3:89 for G being Group for A being Subset of G holds A,A are_conjugated proof let G be Group; ::_thesis: for A being Subset of G holds A,A are_conjugated let A be Subset of G; ::_thesis: A,A are_conjugated take 1_ G ; :: according to GROUP_3:def_9 ::_thesis: A = A |^ (1_ G) thus A = A |^ (1_ G) by Th52; ::_thesis: verum end; theorem Th90: :: GROUP_3:90 for G being Group for A, B being Subset of G st A,B are_conjugated holds B,A are_conjugated proof let G be Group; ::_thesis: for A, B being Subset of G st A,B are_conjugated holds B,A are_conjugated let A, B be Subset of G; ::_thesis: ( A,B are_conjugated implies B,A are_conjugated ) given g being Element of G such that A1: A = B |^ g ; :: according to GROUP_3:def_9 ::_thesis: B,A are_conjugated B = A |^ (g ") by A1, Th54; hence B,A are_conjugated by Def9; ::_thesis: verum end; definition let G be Group; let A, B be Subset of G; :: original: are_conjugated redefine predA,B are_conjugated ; reflexivity for A being Subset of G holds (G,b1,b1) by Th89; symmetry for A, B being Subset of G st (G,b1,b2) holds (G,b2,b1) by Th90; end; theorem Th91: :: GROUP_3:91 for G being Group for A, B, C being Subset of G st A,B are_conjugated & B,C are_conjugated holds A,C are_conjugated proof let G be Group; ::_thesis: for A, B, C being Subset of G st A,B are_conjugated & B,C are_conjugated holds A,C are_conjugated let A, B, C be Subset of G; ::_thesis: ( A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated ) given g being Element of G such that A1: A = B |^ g ; :: according to GROUP_3:def_9 ::_thesis: ( not B,C are_conjugated or A,C are_conjugated ) given h being Element of G such that A2: B = C |^ h ; :: according to GROUP_3:def_9 ::_thesis: A,C are_conjugated A = C |^ (h * g) by A1, A2, Th47; hence A,C are_conjugated by Def9; ::_thesis: verum end; theorem Th92: :: GROUP_3:92 for G being Group for a, b being Element of G holds ( {a},{b} are_conjugated iff a,b are_conjugated ) proof let G be Group; ::_thesis: for a, b being Element of G holds ( {a},{b} are_conjugated iff a,b are_conjugated ) let a, b be Element of G; ::_thesis: ( {a},{b} are_conjugated iff a,b are_conjugated ) thus ( {a},{b} are_conjugated implies a,b are_conjugated ) ::_thesis: ( a,b are_conjugated implies {a},{b} are_conjugated ) proof assume {a},{b} are_conjugated ; ::_thesis: a,b are_conjugated then consider g being Element of G such that A1: {a} |^ g = {b} by Th88; {b} = {(a |^ g)} by A1, Th37; then b = a |^ g by ZFMISC_1:3; hence a,b are_conjugated by Th74; ::_thesis: verum end; assume a,b are_conjugated ; ::_thesis: {a},{b} are_conjugated then consider g being Element of G such that A2: a |^ g = b by Th74; {b} = {a} |^ g by A2, Th37; hence {a},{b} are_conjugated by Th88; ::_thesis: verum end; theorem Th93: :: GROUP_3:93 for G being Group for A being Subset of G for H1 being Subgroup of G st A, carr H1 are_conjugated holds ex H2 being strict Subgroup of G st the carrier of H2 = A proof let G be Group; ::_thesis: for A being Subset of G for H1 being Subgroup of G st A, carr H1 are_conjugated holds ex H2 being strict Subgroup of G st the carrier of H2 = A let A be Subset of G; ::_thesis: for H1 being Subgroup of G st A, carr H1 are_conjugated holds ex H2 being strict Subgroup of G st the carrier of H2 = A let H1 be Subgroup of G; ::_thesis: ( A, carr H1 are_conjugated implies ex H2 being strict Subgroup of G st the carrier of H2 = A ) assume A, carr H1 are_conjugated ; ::_thesis: ex H2 being strict Subgroup of G st the carrier of H2 = A then consider g being Element of G such that A1: A = (carr H1) |^ g by Def9; A = the carrier of (H1 |^ g) by A1, Def6; hence ex H2 being strict Subgroup of G st the carrier of H2 = A ; ::_thesis: verum end; definition let G be Group; let A be Subset of G; func con_class A -> Subset-Family of G equals :: GROUP_3:def 10 { B where B is Subset of G : A,B are_conjugated } ; coherence { B where B is Subset of G : A,B are_conjugated } is Subset-Family of G proof set X = { B where B is Subset of G : A,B are_conjugated } ; { B where B is Subset of G : A,B are_conjugated } c= bool the carrier of G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Subset of G : A,B are_conjugated } or x in bool the carrier of G ) assume x in { B where B is Subset of G : A,B are_conjugated } ; ::_thesis: x in bool the carrier of G then ex B being Subset of G st ( x = B & A,B are_conjugated ) ; hence x in bool the carrier of G ; ::_thesis: verum end; hence { B where B is Subset of G : A,B are_conjugated } is Subset-Family of G ; ::_thesis: verum end; end; :: deftheorem defines con_class GROUP_3:def_10_:_ for G being Group for A being Subset of G holds con_class A = { B where B is Subset of G : A,B are_conjugated } ; theorem :: GROUP_3:94 for x being set for G being Group for A being Subset of G holds ( x in con_class A iff ex B being Subset of G st ( x = B & A,B are_conjugated ) ) ; theorem Th95: :: GROUP_3:95 for G being Group for A, B being Subset of G holds ( A in con_class B iff A,B are_conjugated ) proof let G be Group; ::_thesis: for A, B being Subset of G holds ( A in con_class B iff A,B are_conjugated ) let A, B be Subset of G; ::_thesis: ( A in con_class B iff A,B are_conjugated ) thus ( A in con_class B implies A,B are_conjugated ) ::_thesis: ( A,B are_conjugated implies A in con_class B ) proof assume A in con_class B ; ::_thesis: A,B are_conjugated then ex C being Subset of G st ( A = C & B,C are_conjugated ) ; hence A,B are_conjugated ; ::_thesis: verum end; assume A,B are_conjugated ; ::_thesis: A in con_class B hence A in con_class B ; ::_thesis: verum end; theorem :: GROUP_3:96 for G being Group for g being Element of G for A being Subset of G holds A |^ g in con_class A proof let G be Group; ::_thesis: for g being Element of G for A being Subset of G holds A |^ g in con_class A let g be Element of G; ::_thesis: for A being Subset of G holds A |^ g in con_class A let A be Subset of G; ::_thesis: A |^ g in con_class A A,A |^ g are_conjugated by Th88; hence A |^ g in con_class A ; ::_thesis: verum end; theorem :: GROUP_3:97 for G being Group for A being Subset of G holds A in con_class A ; theorem :: GROUP_3:98 for G being Group for A, B being Subset of G st A in con_class B holds B in con_class A proof let G be Group; ::_thesis: for A, B being Subset of G st A in con_class B holds B in con_class A let A, B be Subset of G; ::_thesis: ( A in con_class B implies B in con_class A ) assume A in con_class B ; ::_thesis: B in con_class A then A,B are_conjugated by Th95; hence B in con_class A ; ::_thesis: verum end; theorem :: GROUP_3:99 for G being Group for A, B being Subset of G holds ( con_class A = con_class B iff con_class A meets con_class B ) proof let G be Group; ::_thesis: for A, B being Subset of G holds ( con_class A = con_class B iff con_class A meets con_class B ) let A, B be Subset of G; ::_thesis: ( con_class A = con_class B iff con_class A meets con_class B ) thus ( con_class A = con_class B implies con_class A meets con_class B ) ::_thesis: ( con_class A meets con_class B implies con_class A = con_class B ) proof A1: A in con_class A ; assume con_class A = con_class B ; ::_thesis: con_class A meets con_class B hence con_class A meets con_class B by A1, XBOOLE_0:3; ::_thesis: verum end; assume con_class A meets con_class B ; ::_thesis: con_class A = con_class B then consider x being set such that A2: x in con_class A and A3: x in con_class B by XBOOLE_0:3; reconsider x = x as Subset of G by A2; A4: A,x are_conjugated by A2, Th95; thus con_class A c= con_class B :: according to XBOOLE_0:def_10 ::_thesis: con_class B c= con_class A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class A or y in con_class B ) assume y in con_class A ; ::_thesis: y in con_class B then consider C being Subset of G such that A5: C = y and A6: A,C are_conjugated ; A7: B,x are_conjugated by A3, Th95; x,A are_conjugated by A2, Th95; then x,C are_conjugated by A6, Th91; then B,C are_conjugated by A7, Th91; hence y in con_class B by A5; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class B or y in con_class A ) assume y in con_class B ; ::_thesis: y in con_class A then consider C being Subset of G such that A8: C = y and A9: B,C are_conjugated ; x,B are_conjugated by A3, Th95; then x,C are_conjugated by A9, Th91; then A,C are_conjugated by A4, Th91; hence y in con_class A by A8; ::_thesis: verum end; theorem Th100: :: GROUP_3:100 for G being Group for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a } proof let G be Group; ::_thesis: for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a } let a be Element of G; ::_thesis: con_class {a} = { {b} where b is Element of G : b in con_class a } set A = { {b} where b is Element of G : b in con_class a } ; thus con_class {a} c= { {b} where b is Element of G : b in con_class a } :: according to XBOOLE_0:def_10 ::_thesis: { {b} where b is Element of G : b in con_class a } c= con_class {a} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class {a} or x in { {b} where b is Element of G : b in con_class a } ) assume x in con_class {a} ; ::_thesis: x in { {b} where b is Element of G : b in con_class a } then consider B being Subset of G such that A1: x = B and A2: {a},B are_conjugated ; consider b being Element of G such that A3: {a} |^ b = B by A2, Th88; a,a |^ b are_conjugated by Th74; then A4: a |^ b in con_class a by Th81; B = {(a |^ b)} by A3, Th37; hence x in { {b} where b is Element of G : b in con_class a } by A1, A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {b} where b is Element of G : b in con_class a } or x in con_class {a} ) assume x in { {b} where b is Element of G : b in con_class a } ; ::_thesis: x in con_class {a} then consider b being Element of G such that A5: x = {b} and A6: b in con_class a ; b,a are_conjugated by A6, Th81; then {b},{a} are_conjugated by Th92; hence x in con_class {a} by A5; ::_thesis: verum end; theorem :: GROUP_3:101 for G being Group for A being Subset of G st G is finite holds con_class A is finite ; definition let G be Group; let H1, H2 be Subgroup of G; predH1,H2 are_conjugated means :Def11: :: GROUP_3:def 11 ex g being Element of G st multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g; end; :: deftheorem Def11 defines are_conjugated GROUP_3:def_11_:_ for G being Group for H1, H2 being Subgroup of G holds ( H1,H2 are_conjugated iff ex g being Element of G st multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g ); notation let G be Group; let H1, H2 be Subgroup of G; antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated ; end; theorem Th102: :: GROUP_3:102 for G being Group for H1, H2 being strict Subgroup of G holds ( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g ) proof let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds ( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g ) let H1, H2 be strict Subgroup of G; ::_thesis: ( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g ) thus ( H1,H2 are_conjugated implies ex g being Element of G st H2 = H1 |^ g ) ::_thesis: ( ex g being Element of G st H2 = H1 |^ g implies H1,H2 are_conjugated ) proof given g being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def_11 ::_thesis: ex g being Element of G st H2 = H1 |^ g H1 |^ (g ") = H2 by A1, Th62; hence ex g being Element of G st H2 = H1 |^ g ; ::_thesis: verum end; given g being Element of G such that A2: H2 = H1 |^ g ; ::_thesis: H1,H2 are_conjugated H1 = H2 |^ (g ") by A2, Th62; hence H1,H2 are_conjugated by Def11; ::_thesis: verum end; theorem Th103: :: GROUP_3:103 for G being Group for H1 being strict Subgroup of G holds H1,H1 are_conjugated proof let G be Group; ::_thesis: for H1 being strict Subgroup of G holds H1,H1 are_conjugated let H1 be strict Subgroup of G; ::_thesis: H1,H1 are_conjugated take 1_ G ; :: according to GROUP_3:def_11 ::_thesis: multMagma(# the carrier of H1, the multF of H1 #) = H1 |^ (1_ G) thus multMagma(# the carrier of H1, the multF of H1 #) = H1 |^ (1_ G) by Th61; ::_thesis: verum end; theorem Th104: :: GROUP_3:104 for G being Group for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds H2,H1 are_conjugated proof let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds H2,H1 are_conjugated let H1, H2 be strict Subgroup of G; ::_thesis: ( H1,H2 are_conjugated implies H2,H1 are_conjugated ) given g being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def_11 ::_thesis: H2,H1 are_conjugated H2 = H1 |^ (g ") by A1, Th62; hence H2,H1 are_conjugated by Def11; ::_thesis: verum end; definition let G be Group; let H1, H2 be strict Subgroup of G; :: original: are_conjugated redefine predH1,H2 are_conjugated ; reflexivity for H1 being strict Subgroup of G holds (G,b1,b1) by Th103; symmetry for H1, H2 being strict Subgroup of G st (G,b1,b2) holds (G,b2,b1) by Th104; end; theorem Th105: :: GROUP_3:105 for G being Group for H3 being Subgroup of G for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds H1,H3 are_conjugated proof let G be Group; ::_thesis: for H3 being Subgroup of G for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds H1,H3 are_conjugated let H3 be Subgroup of G; ::_thesis: for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds H1,H3 are_conjugated let H1, H2 be strict Subgroup of G; ::_thesis: ( H1,H2 are_conjugated & H2,H3 are_conjugated implies H1,H3 are_conjugated ) given g being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def_11 ::_thesis: ( not H2,H3 are_conjugated or H1,H3 are_conjugated ) given h being Element of G such that A2: multMagma(# the carrier of H2, the multF of H2 #) = H3 |^ h ; :: according to GROUP_3:def_11 ::_thesis: H1,H3 are_conjugated H1 = H3 |^ (h * g) by A1, A2, Th60; hence H1,H3 are_conjugated by Def11; ::_thesis: verum end; definition let G be Group; let H be Subgroup of G; func con_class H -> Subset of (Subgroups G) means :Def12: :: GROUP_3:def 12 for x being set holds ( x in it iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ); existence ex b1 being Subset of (Subgroups G) st for x being set holds ( x in b1 iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) proof defpred S1[ set ] means ex H1 being strict Subgroup of G st ( \$1 = H1 & H,H1 are_conjugated ); consider L being Subset of (Subgroups G) such that A1: for x being set holds ( x in L iff ( x in Subgroups G & S1[x] ) ) from SUBSET_1:sch_1(); take L ; ::_thesis: for x being set holds ( x in L iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) let x be set ; ::_thesis: ( x in L iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) thus ( x in L implies ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) by A1; ::_thesis: ( ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) implies x in L ) given H1 being strict Subgroup of G such that A2: x = H1 and A3: H,H1 are_conjugated ; ::_thesis: x in L x in Subgroups G by A2, Def1; hence x in L by A1, A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (Subgroups G) st ( for x being set holds ( x in b1 iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being set holds ( x in b2 iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex H3 being strict Subgroup of G st ( \$1 = H3 & H,H3 are_conjugated ); let A1, A2 be Subset of (Subgroups G); ::_thesis: ( ( for x being set holds ( x in A1 iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being set holds ( x in A2 iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) ) implies A1 = A2 ) assume A4: for x being set holds ( x in A1 iff S1[x] ) ; ::_thesis: ( ex x being set st ( ( x in A2 implies ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) implies ( ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) & not x in A2 ) ) or A1 = A2 ) assume A5: for x being set holds ( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2 thus A1 = A2 from XBOOLE_0:sch_2(A4, A5); ::_thesis: verum end; end; :: deftheorem Def12 defines con_class GROUP_3:def_12_:_ for G being Group for H being Subgroup of G for b3 being Subset of (Subgroups G) holds ( b3 = con_class H iff for x being set holds ( x in b3 iff ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) ) ); theorem Th106: :: GROUP_3:106 for x being set for G being Group for H being Subgroup of G st x in con_class H holds x is strict Subgroup of G proof let x be set ; ::_thesis: for G being Group for H being Subgroup of G st x in con_class H holds x is strict Subgroup of G let G be Group; ::_thesis: for H being Subgroup of G st x in con_class H holds x is strict Subgroup of G let H be Subgroup of G; ::_thesis: ( x in con_class H implies x is strict Subgroup of G ) assume x in con_class H ; ::_thesis: x is strict Subgroup of G then ex H1 being strict Subgroup of G st ( x = H1 & H,H1 are_conjugated ) by Def12; hence x is strict Subgroup of G ; ::_thesis: verum end; theorem Th107: :: GROUP_3:107 for G being Group for H1, H2 being strict Subgroup of G holds ( H1 in con_class H2 iff H1,H2 are_conjugated ) proof let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds ( H1 in con_class H2 iff H1,H2 are_conjugated ) let H1, H2 be strict Subgroup of G; ::_thesis: ( H1 in con_class H2 iff H1,H2 are_conjugated ) thus ( H1 in con_class H2 implies H1,H2 are_conjugated ) ::_thesis: ( H1,H2 are_conjugated implies H1 in con_class H2 ) proof assume H1 in con_class H2 ; ::_thesis: H1,H2 are_conjugated then ex H3 being strict Subgroup of G st ( H1 = H3 & H2,H3 are_conjugated ) by Def12; hence H1,H2 are_conjugated ; ::_thesis: verum end; assume H1,H2 are_conjugated ; ::_thesis: H1 in con_class H2 hence H1 in con_class H2 by Def12; ::_thesis: verum end; theorem Th108: :: GROUP_3:108 for G being Group for g being Element of G for H being strict Subgroup of G holds H |^ g in con_class H proof let G be Group; ::_thesis: for g being Element of G for H being strict Subgroup of G holds H |^ g in con_class H let g be Element of G; ::_thesis: for H being strict Subgroup of G holds H |^ g in con_class H let H be strict Subgroup of G; ::_thesis: H |^ g in con_class H H,H |^ g are_conjugated by Th102; hence H |^ g in con_class H by Def12; ::_thesis: verum end; theorem Th109: :: GROUP_3:109 for G being Group for H being strict Subgroup of G holds H in con_class H proof let G be Group; ::_thesis: for H being strict Subgroup of G holds H in con_class H let H be strict Subgroup of G; ::_thesis: H in con_class H H,H are_conjugated ; hence H in con_class H by Def12; ::_thesis: verum end; theorem :: GROUP_3:110 for G being Group for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds H2 in con_class H1 proof let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds H2 in con_class H1 let H1, H2 be strict Subgroup of G; ::_thesis: ( H1 in con_class H2 implies H2 in con_class H1 ) assume H1 in con_class H2 ; ::_thesis: H2 in con_class H1 then H1,H2 are_conjugated by Th107; hence H2 in con_class H1 by Th107; ::_thesis: verum end; theorem :: GROUP_3:111 for G being Group for H1, H2 being strict Subgroup of G holds ( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 ) proof let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds ( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 ) let H1, H2 be strict Subgroup of G; ::_thesis: ( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 ) thus ( con_class H1 = con_class H2 implies con_class H1 meets con_class H2 ) ::_thesis: ( con_class H1 meets con_class H2 implies con_class H1 = con_class H2 ) proof assume A1: con_class H1 = con_class H2 ; ::_thesis: con_class H1 meets con_class H2 H1 in con_class H1 by Th109; hence con_class H1 meets con_class H2 by A1, XBOOLE_0:3; ::_thesis: verum end; assume con_class H1 meets con_class H2 ; ::_thesis: con_class H1 = con_class H2 then consider x being set such that A2: x in con_class H1 and A3: x in con_class H2 by XBOOLE_0:3; reconsider x = x as strict Subgroup of G by A2, Th106; A4: H1,x are_conjugated by A2, Th107; thus con_class H1 c= con_class H2 :: according to XBOOLE_0:def_10 ::_thesis: con_class H2 c= con_class H1 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class H1 or y in con_class H2 ) assume y in con_class H1 ; ::_thesis: y in con_class H2 then consider H3 being strict Subgroup of G such that A5: H3 = y and A6: H1,H3 are_conjugated by Def12; A7: H2,x are_conjugated by A3, Th107; x,H1 are_conjugated by A2, Th107; then x,H3 are_conjugated by A6, Th105; then H2,H3 are_conjugated by A7, Th105; hence y in con_class H2 by A5, Def12; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class H2 or y in con_class H1 ) assume y in con_class H2 ; ::_thesis: y in con_class H1 then consider H3 being strict Subgroup of G such that A8: H3 = y and A9: H2,H3 are_conjugated by Def12; x,H2 are_conjugated by A3, Th107; then x,H3 are_conjugated by A9, Th105; then H1,H3 are_conjugated by A4, Th105; hence y in con_class H1 by A8, Def12; ::_thesis: verum end; theorem :: GROUP_3:112 for G being Group for H being Subgroup of G st G is finite holds con_class H is finite by Th15, FINSET_1:1; theorem Th113: :: GROUP_3:113 for G being Group for H2 being Subgroup of G for H1 being strict Subgroup of G holds ( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated ) proof let G be Group; ::_thesis: for H2 being Subgroup of G for H1 being strict Subgroup of G holds ( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated ) let H2 be Subgroup of G; ::_thesis: for H1 being strict Subgroup of G holds ( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated ) let H1 be strict Subgroup of G; ::_thesis: ( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated ) thus ( H1,H2 are_conjugated implies carr H1, carr H2 are_conjugated ) ::_thesis: ( carr H1, carr H2 are_conjugated implies H1,H2 are_conjugated ) proof given a being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ a ; :: according to GROUP_3:def_11 ::_thesis: carr H1, carr H2 are_conjugated carr H1 = (carr H2) |^ a by A1, Def6; hence carr H1, carr H2 are_conjugated by Def9; ::_thesis: verum end; given a being Element of G such that A2: carr H1 = (carr H2) |^ a ; :: according to GROUP_3:def_9 ::_thesis: H1,H2 are_conjugated H1 = H2 |^ a by A2, Def6; hence H1,H2 are_conjugated by Def11; ::_thesis: verum end; definition let G be Group; let IT be Subgroup of G; attrIT is normal means :Def13: :: GROUP_3:def 13 for a being Element of G holds IT |^ a = multMagma(# the carrier of IT, the multF of IT #); end; :: deftheorem Def13 defines normal GROUP_3:def_13_:_ for G being Group for IT being Subgroup of G holds ( IT is normal iff for a being Element of G holds IT |^ a = multMagma(# the carrier of IT, the multF of IT #) ); registration let G be Group; cluster non empty strict unital Group-like associative normal for Subgroup of G; existence ex b1 being Subgroup of G st ( b1 is strict & b1 is normal ) proof for a being Element of G holds ((1). G) |^ a = (1). G by Th67; then (1). G is normal by Def13; hence ex b1 being Subgroup of G st ( b1 is strict & b1 is normal ) ; ::_thesis: verum end; end; theorem Th114: :: GROUP_3:114 for G being Group holds ( (1). G is normal & (Omega). G is normal ) proof let G be Group; ::_thesis: ( (1). G is normal & (Omega). G is normal ) thus for a being Element of G holds ((1). G) |^ a = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) by Th67; :: according to GROUP_3:def_13 ::_thesis: (Omega). G is normal thus for a being Element of G holds ((Omega). G) |^ a = multMagma(# the carrier of ((Omega). G), the multF of ((Omega). G) #) by Th69; :: according to GROUP_3:def_13 ::_thesis: verum end; theorem :: GROUP_3:115 for G being Group for N1, N2 being strict normal Subgroup of G holds N1 /\ N2 is normal proof let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G holds N1 /\ N2 is normal let N1, N2 be strict normal Subgroup of G; ::_thesis: N1 /\ N2 is normal let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: (N1 /\ N2) |^ a = multMagma(# the carrier of (N1 /\ N2), the multF of (N1 /\ N2) #) thus (N1 /\ N2) |^ a = (N1 |^ a) /\ (N2 |^ a) by Th63 .= N1 /\ (N2 |^ a) by Def13 .= multMagma(# the carrier of (N1 /\ N2), the multF of (N1 /\ N2) #) by Def13 ; ::_thesis: verum end; theorem :: GROUP_3:116 for G being Group for H being strict Subgroup of G st G is commutative Group holds H is normal proof let G be Group; ::_thesis: for H being strict Subgroup of G st G is commutative Group holds H is normal let H be strict Subgroup of G; ::_thesis: ( G is commutative Group implies H is normal ) assume G is commutative Group ; ::_thesis: H is normal hence for a being Element of G holds H |^ a = multMagma(# the carrier of H, the multF of H #) by Th73; :: according to GROUP_3:def_13 ::_thesis: verum end; theorem Th117: :: GROUP_3:117 for G being Group for H being Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a ) proof let G be Group; ::_thesis: for H being Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a ) let H be Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a ) thus ( H is normal Subgroup of G implies for a being Element of G holds a * H = H * a ) ::_thesis: ( ( for a being Element of G holds a * H = H * a ) implies H is normal Subgroup of G ) proof assume A1: H is normal Subgroup of G ; ::_thesis: for a being Element of G holds a * H = H * a let a be Element of G; ::_thesis: a * H = H * a A2: carr (H |^ a) = ((a ") * H) * a by Th59; carr (H |^ a) = the carrier of multMagma(# the carrier of H, the multF of H #) by A1, Def13 .= carr H ; hence a * H = (a * ((a ") * H)) * a by A2, GROUP_2:33 .= ((a * (a ")) * H) * a by GROUP_2:105 .= ((1_ G) * H) * a by GROUP_1:def_5 .= H * a by GROUP_2:37 ; ::_thesis: verum end; assume A3: for a being Element of G holds a * H = H * a ; ::_thesis: H is normal Subgroup of G H is normal proof let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: H |^ a = multMagma(# the carrier of H, the multF of H #) the carrier of (H |^ a) = ((a ") * H) * a by Th59 .= (H * (a ")) * a by A3 .= H * ((a ") * a) by GROUP_2:107 .= H * (1_ G) by GROUP_1:def_5 .= the carrier of H by GROUP_2:109 ; hence H |^ a = multMagma(# the carrier of H, the multF of H #) by GROUP_2:59; ::_thesis: verum end; hence H is normal Subgroup of G ; ::_thesis: verum end; theorem Th118: :: GROUP_3:118 for G being Group for H being Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds a * H c= H * a ) proof let G be Group; ::_thesis: for H being Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds a * H c= H * a ) let H be Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds a * H c= H * a ) thus ( H is normal Subgroup of G implies for a being Element of G holds a * H c= H * a ) by Th117; ::_thesis: ( ( for a being Element of G holds a * H c= H * a ) implies H is normal Subgroup of G ) assume A1: for a being Element of G holds a * H c= H * a ; ::_thesis: H is normal Subgroup of G A2: now__::_thesis:_for_a_being_Element_of_G_holds_H_*_a_c=_a_*_H let a be Element of G; ::_thesis: H * a c= a * H (a ") * H c= H * (a ") by A1; then a * ((a ") * H) c= a * (H * (a ")) by Th4; then (a * (a ")) * H c= a * (H * (a ")) by GROUP_2:105; then (1_ G) * H c= a * (H * (a ")) by GROUP_1:def_5; then carr H c= a * (H * (a ")) by GROUP_2:109; then carr H c= (a * H) * (a ") by GROUP_2:106; then (carr H) * a c= ((a * H) * (a ")) * a by Th4; then H * a c= (a * H) * ((a ") * a) by GROUP_2:34; then H * a c= (a * H) * (1_ G) by GROUP_1:def_5; hence H * a c= a * H by GROUP_2:37; ::_thesis: verum end; now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_=_H_*_a let a be Element of G; ::_thesis: a * H = H * a ( a * H c= H * a & H * a c= a * H ) by A1, A2; hence a * H = H * a by XBOOLE_0:def_10; ::_thesis: verum end; hence H is normal Subgroup of G by Th117; ::_thesis: verum end; theorem Th119: :: GROUP_3:119 for G being Group for H being Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H ) proof let G be Group; ::_thesis: for H being Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H ) let H be Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H ) thus ( H is normal Subgroup of G implies for a being Element of G holds H * a c= a * H ) by Th117; ::_thesis: ( ( for a being Element of G holds H * a c= a * H ) implies H is normal Subgroup of G ) assume A1: for a being Element of G holds H * a c= a * H ; ::_thesis: H is normal Subgroup of G A2: now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_c=_H_*_a let a be Element of G; ::_thesis: a * H c= H * a H * (a ") c= (a ") * H by A1; then a * (H * (a ")) c= a * ((a ") * H) by Th4; then a * (H * (a ")) c= (a * (a ")) * H by GROUP_2:105; then a * (H * (a ")) c= (1_ G) * H by GROUP_1:def_5; then a * (H * (a ")) c= carr H by GROUP_2:109; then (a * H) * (a ") c= carr H by GROUP_2:106; then ((a * H) * (a ")) * a c= (carr H) * a by Th4; then (a * H) * ((a ") * a) c= H * a by GROUP_2:34; then (a * H) * (1_ G) c= H * a by GROUP_1:def_5; hence a * H c= H * a by GROUP_2:37; ::_thesis: verum end; now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_=_H_*_a let a be Element of G; ::_thesis: a * H = H * a ( a * H c= H * a & H * a c= a * H ) by A1, A2; hence a * H = H * a by XBOOLE_0:def_10; ::_thesis: verum end; hence H is normal Subgroup of G by Th117; ::_thesis: verum end; theorem :: GROUP_3:120 for G being Group for H being Subgroup of G holds ( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A ) proof let G be Group; ::_thesis: for H being Subgroup of G holds ( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A ) let H be Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A ) thus ( H is normal Subgroup of G implies for A being Subset of G holds A * H = H * A ) ::_thesis: ( ( for A being Subset of G holds A * H = H * A ) implies H is normal Subgroup of G ) proof assume A1: H is normal Subgroup of G ; ::_thesis: for A being Subset of G holds A * H = H * A let A be Subset of G; ::_thesis: A * H = H * A thus A * H c= H * A :: according to XBOOLE_0:def_10 ::_thesis: H * A c= A * H proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * H or x in H * A ) assume x in A * H ; ::_thesis: x in H * A then consider a, h being Element of G such that A2: x = a * h and A3: a in A and A4: h in H by GROUP_2:94; x in a * H by A2, A4, GROUP_2:103; then x in H * a by A1, Th117; then ex g being Element of G st ( x = g * a & g in H ) by GROUP_2:104; hence x in H * A by A3, GROUP_2:95; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H * A or x in A * H ) assume x in H * A ; ::_thesis: x in A * H then consider h, a being Element of G such that A5: ( x = h * a & h in H ) and A6: a in A by GROUP_2:95; x in H * a by A5, GROUP_2:104; then x in a * H by A1, Th117; then ex g being Element of G st ( x = a * g & g in H ) by GROUP_2:103; hence x in A * H by A6, GROUP_2:94; ::_thesis: verum end; assume A7: for A being Subset of G holds A * H = H * A ; ::_thesis: H is normal Subgroup of G now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_=_H_*_a let a be Element of G; ::_thesis: a * H = H * a thus a * H = {a} * H .= H * {a} by A7 .= H * a ; ::_thesis: verum end; hence H is normal Subgroup of G by Th117; ::_thesis: verum end; theorem :: GROUP_3:121 for G being Group for H being strict Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a ) proof let G be Group; ::_thesis: for H being strict Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a ) let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a ) thus ( H is normal Subgroup of G implies for a being Element of G holds H is Subgroup of H |^ a ) ::_thesis: ( ( for a being Element of G holds H is Subgroup of H |^ a ) implies H is normal Subgroup of G ) proof assume A1: H is normal Subgroup of G ; ::_thesis: for a being Element of G holds H is Subgroup of H |^ a let a be Element of G; ::_thesis: H is Subgroup of H |^ a H |^ a = multMagma(# the carrier of H, the multF of H #) by A1, Def13; hence H is Subgroup of H |^ a by GROUP_2:54; ::_thesis: verum end; assume A2: for a being Element of G holds H is Subgroup of H |^ a ; ::_thesis: H is normal Subgroup of G now__::_thesis:_for_a_being_Element_of_G_holds_H_*_a_c=_a_*_H let a be Element of G; ::_thesis: H * a c= a * H A3: (H |^ (a ")) * a = ((((a ") ") * H) * (a ")) * a by Th59 .= (((a ") ") * H) * ((a ") * a) by GROUP_2:34 .= (((a ") ") * H) * (1_ G) by GROUP_1:def_5 .= ((a ") ") * H by GROUP_2:37 .= a * H ; H is Subgroup of H |^ (a ") by A2; hence H * a c= a * H by A3, Th6; ::_thesis: verum end; hence H is normal Subgroup of G by Th119; ::_thesis: verum end; theorem :: GROUP_3:122 for G being Group for H being strict Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds H |^ a is Subgroup of H ) proof let G be Group; ::_thesis: for H being strict Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G holds H |^ a is Subgroup of H ) let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds H |^ a is Subgroup of H ) thus ( H is normal Subgroup of G implies for a being Element of G holds H |^ a is Subgroup of H ) ::_thesis: ( ( for a being Element of G holds H |^ a is Subgroup of H ) implies H is normal Subgroup of G ) proof assume A1: H is normal Subgroup of G ; ::_thesis: for a being Element of G holds H |^ a is Subgroup of H let a be Element of G; ::_thesis: H |^ a is Subgroup of H H |^ a = multMagma(# the carrier of H, the multF of H #) by A1, Def13; hence H |^ a is Subgroup of H by GROUP_2:54; ::_thesis: verum end; assume A2: for a being Element of G holds H |^ a is Subgroup of H ; ::_thesis: H is normal Subgroup of G now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_c=_H_*_a let a be Element of G; ::_thesis: a * H c= H * a A3: (H |^ (a ")) * a = ((((a ") ") * H) * (a ")) * a by Th59 .= (((a ") ") * H) * ((a ") * a) by GROUP_2:34 .= (((a ") ") * H) * (1_ G) by GROUP_1:def_5 .= ((a ") ") * H by GROUP_2:37 .= a * H ; H |^ (a ") is Subgroup of H by A2; hence a * H c= H * a by A3, Th6; ::_thesis: verum end; hence H is normal Subgroup of G by Th118; ::_thesis: verum end; theorem :: GROUP_3:123 for G being Group for H being strict Subgroup of G holds ( H is normal Subgroup of G iff con_class H = {H} ) proof let G be Group; ::_thesis: for H being strict Subgroup of G holds ( H is normal Subgroup of G iff con_class H = {H} ) let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff con_class H = {H} ) thus ( H is normal Subgroup of G implies con_class H = {H} ) ::_thesis: ( con_class H = {H} implies H is normal Subgroup of G ) proof assume A1: H is normal Subgroup of G ; ::_thesis: con_class H = {H} thus con_class H c= {H} :: according to XBOOLE_0:def_10 ::_thesis: {H} c= con_class H proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class H or x in {H} ) assume x in con_class H ; ::_thesis: x in {H} then consider H1 being strict Subgroup of G such that A2: x = H1 and A3: H,H1 are_conjugated by Def12; ex g being Element of G st H1 = H |^ g by A3, Th102; then x = H by A1, A2, Def13; hence x in {H} by TARSKI:def_1; ::_thesis: verum end; H in con_class H by Th109; hence {H} c= con_class H by ZFMISC_1:31; ::_thesis: verum end; assume A4: con_class H = {H} ; ::_thesis: H is normal Subgroup of G H is normal proof let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: H |^ a = multMagma(# the carrier of H, the multF of H #) H |^ a in con_class H by Th108; hence H |^ a = multMagma(# the carrier of H, the multF of H #) by A4, TARSKI:def_1; ::_thesis: verum end; hence H is normal Subgroup of G ; ::_thesis: verum end; theorem :: GROUP_3:124 for G being Group for H being strict Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G st a in H holds con_class a c= carr H ) proof let G be Group; ::_thesis: for H being strict Subgroup of G holds ( H is normal Subgroup of G iff for a being Element of G st a in H holds con_class a c= carr H ) let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G st a in H holds con_class a c= carr H ) thus ( H is normal Subgroup of G implies for a being Element of G st a in H holds con_class a c= carr H ) ::_thesis: ( ( for a being Element of G st a in H holds con_class a c= carr H ) implies H is normal Subgroup of G ) proof assume A1: H is normal Subgroup of G ; ::_thesis: for a being Element of G st a in H holds con_class a c= carr H let a be Element of G; ::_thesis: ( a in H implies con_class a c= carr H ) assume A2: a in H ; ::_thesis: con_class a c= carr H let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class a or x in carr H ) assume x in con_class a ; ::_thesis: x in carr H then consider b being Element of G such that A3: x = b and A4: a,b are_conjugated by Th80; consider c being Element of G such that A5: b = a |^ c by A4, Th74; x in H |^ c by A2, A3, A5, Th58; then x in H by A1, Def13; hence x in carr H by STRUCT_0:def_5; ::_thesis: verum end; assume A6: for a being Element of G st a in H holds con_class a c= carr H ; ::_thesis: H is normal Subgroup of G H is normal proof let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: H |^ a = multMagma(# the carrier of H, the multF of H #) H |^ a = H proof let b be Element of G; :: according to GROUP_2:def_6 ::_thesis: ( ( not b in H |^ a or b in H ) & ( not b in H or b in H |^ a ) ) thus ( b in H |^ a implies b in H ) ::_thesis: ( not b in H or b in H |^ a ) proof assume b in H |^ a ; ::_thesis: b in H then consider c being Element of G such that A7: ( b = c |^ a & c in H ) by Th58; ( b in con_class c & con_class c c= carr H ) by A6, A7, Th82; hence b in H by STRUCT_0:def_5; ::_thesis: verum end; assume b in H ; ::_thesis: b in H |^ a then A8: con_class b c= carr H by A6; b |^ (a ") in con_class b by Th82; then b |^ (a ") in H by A8, STRUCT_0:def_5; then (b |^ (a ")) |^ a in H |^ a by Th58; hence b in H |^ a by Th25; ::_thesis: verum end; hence H |^ a = multMagma(# the carrier of H, the multF of H #) ; ::_thesis: verum end; hence H is normal Subgroup of G ; ::_thesis: verum end; Lm5: for G being Group for N2 being normal Subgroup of G for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1) proof let G be Group; ::_thesis: for N2 being normal Subgroup of G for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1) let N2 be normal Subgroup of G; ::_thesis: for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1) let N1 be strict normal Subgroup of G; ::_thesis: (carr N1) * (carr N2) c= (carr N2) * (carr N1) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (carr N1) * (carr N2) or x in (carr N2) * (carr N1) ) assume x in (carr N1) * (carr N2) ; ::_thesis: x in (carr N2) * (carr N1) then consider a, b being Element of G such that A1: x = a * b and A2: a in carr N1 and A3: b in carr N2 ; a in N1 by A2, STRUCT_0:def_5; then a |^ b in N1 |^ b by Th58; then a |^ b in multMagma(# the carrier of N1, the multF of N1 #) by Def13; then A4: a |^ b in carr N1 by STRUCT_0:def_5; b * (a |^ b) = b * ((b ") * (a * b)) by GROUP_1:def_3 .= a * b by Th1 ; hence x in (carr N2) * (carr N1) by A1, A3, A4; ::_thesis: verum end; theorem Th125: :: GROUP_3:125 for G being Group for N1, N2 being strict normal Subgroup of G holds (carr N1) * (carr N2) = (carr N2) * (carr N1) proof let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G holds (carr N1) * (carr N2) = (carr N2) * (carr N1) let N1, N2 be strict normal Subgroup of G; ::_thesis: (carr N1) * (carr N2) = (carr N2) * (carr N1) ( (carr N1) * (carr N2) c= (carr N2) * (carr N1) & (carr N2) * (carr N1) c= (carr N1) * (carr N2) ) by Lm5; hence (carr N1) * (carr N2) = (carr N2) * (carr N1) by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: GROUP_3:126 for G being Group 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) proof let G be Group; ::_thesis: 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) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2) set A = (carr N1) * (carr N2); set B = carr N1; set C = carr N2; (carr N1) * (carr N2) = (carr N2) * (carr N1) by Th125; then consider H being strict Subgroup of G such that A1: the carrier of H = (carr N1) * (carr N2) by GROUP_2:78; now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_=_H_*_a let a be Element of G; ::_thesis: a * H = H * a thus a * H = (a * N1) * (carr N2) by A1, GROUP_2:29 .= (N1 * a) * (carr N2) by Th117 .= (carr N1) * (a * N2) by GROUP_2:30 .= (carr N1) * (N2 * a) by Th117 .= H * a by A1, GROUP_2:31 ; ::_thesis: verum end; then H is normal Subgroup of G by Th117; hence ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2) by A1; ::_thesis: verum end; theorem :: GROUP_3:127 for G being Group for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N proof let G be Group; ::_thesis: for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N let N be normal Subgroup of G; ::_thesis: Left_Cosets N = Right_Cosets N thus Left_Cosets N c= Right_Cosets N :: according to XBOOLE_0:def_10 ::_thesis: Right_Cosets N c= Left_Cosets N proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets N or x in Right_Cosets N ) assume x in Left_Cosets N ; ::_thesis: x in Right_Cosets N then consider a being Element of G such that A1: x = a * N by GROUP_2:def_15; x = N * a by A1, Th117; hence x in Right_Cosets N by GROUP_2:def_16; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets N or x in Left_Cosets N ) assume x in Right_Cosets N ; ::_thesis: x in Left_Cosets N then consider a being Element of G such that A2: x = N * a by GROUP_2:def_16; x = a * N by A2, Th117; hence x in Left_Cosets N by GROUP_2:def_15; ::_thesis: verum end; theorem :: GROUP_3:128 for G being Group for H being Subgroup of G st Left_Cosets H is finite & index H = 2 holds H is normal Subgroup of G proof let G be Group; ::_thesis: for H being Subgroup of G st Left_Cosets H is finite & index H = 2 holds H is normal Subgroup of G let H be Subgroup of G; ::_thesis: ( Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G ) assume that A1: Left_Cosets H is finite and A2: index H = 2 ; ::_thesis: H is normal Subgroup of G ex B being finite set st ( B = Left_Cosets H & index H = card B ) by A1, GROUP_2:146; then consider x, y being set such that A3: x <> y and A4: Left_Cosets H = {x,y} by A2, CARD_2:60; carr H in Left_Cosets H by GROUP_2:135; then ( {x,y} = {x,(carr H)} or {x,y} = {(carr H),y} ) by A4, TARSKI:def_2; then consider z3 being set such that A5: {x,y} = {(carr H),z3} ; A6: carr H misses z3 proof z3 in Left_Cosets H by A4, A5, TARSKI:def_2; then A7: ex a being Element of G st z3 = a * H by GROUP_2:def_15; A8: carr H = (1_ G) * H by GROUP_2:109; assume not carr H misses z3 ; ::_thesis: contradiction then carr H = z3 by A7, A8, GROUP_2:115; then A9: {x,y} = {(carr H)} by A5, ENUMSET1:29; then x = carr H by ZFMISC_1:4; hence contradiction by A3, A9, ZFMISC_1:4; ::_thesis: verum end; ( union (Left_Cosets H) = the carrier of G & union (Left_Cosets H) = (carr H) \/ z3 ) by A4, A5, GROUP_2:137, ZFMISC_1:75; then A10: ( union (Right_Cosets H) = the carrier of G & z3 = the carrier of G \ (carr H) ) by A6, GROUP_2:137, XBOOLE_1:88; ex C being finite set st ( C = Right_Cosets H & index H = card C ) by A1, GROUP_2:146; then consider z1, z2 being set such that A11: z1 <> z2 and A12: Right_Cosets H = {z1,z2} by A2, CARD_2:60; carr H in Right_Cosets H by GROUP_2:135; then ( {z1,z2} = {z1,(carr H)} or {z1,z2} = {(carr H),z2} ) by A12, TARSKI:def_2; then consider z4 being set such that A13: {z1,z2} = {(carr H),z4} ; A14: carr H misses z4 proof z4 in Right_Cosets H by A12, A13, TARSKI:def_2; then A15: ex a being Element of G st z4 = H * a by GROUP_2:def_16; A16: carr H = H * (1_ G) by GROUP_2:109; assume not carr H misses z4 ; ::_thesis: contradiction then carr H = z4 by A15, A16, GROUP_2:121; then A17: {z1,z2} = {(carr H)} by A13, ENUMSET1:29; then z1 = carr H by ZFMISC_1:4; hence contradiction by A11, A17, ZFMISC_1:4; ::_thesis: verum end; A18: union (Right_Cosets H) = (carr H) \/ z4 by A12, A13, ZFMISC_1:75; now__::_thesis:_for_c_being_Element_of_G_holds_c_*_H_=_H_*_c let c be Element of G; ::_thesis: c * H = H * c now__::_thesis:_c_*_H_=_H_*_c percases ( c * H = carr H or c * H <> carr H ) ; supposeA19: c * H = carr H ; ::_thesis: c * H = H * c then c in H by GROUP_2:113; hence c * H = H * c by A19, GROUP_2:119; ::_thesis: verum end; supposeA20: c * H <> carr H ; ::_thesis: c * H = H * c then not c in H by GROUP_2:113; then A21: H * c <> carr H by GROUP_2:119; c * H in Left_Cosets H by GROUP_2:def_15; then A22: c * H = z3 by A4, A5, A20, TARSKI:def_2; H * c in Right_Cosets H by GROUP_2:def_16; then H * c = z4 by A12, A13, A21, TARSKI:def_2; hence c * H = H * c by A10, A18, A14, A22, XBOOLE_1:88; ::_thesis: verum end; end; end; hence c * H = H * c ; ::_thesis: verum end; hence H is normal Subgroup of G by Th117; ::_thesis: verum end; definition let G be Group; let A be Subset of G; func Normalizer A -> strict Subgroup of G means :Def14: :: GROUP_3:def 14 the carrier of it = { h where h is Element of G : A |^ h = A } ; existence ex b1 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A } proof set X = { h where h is Element of G : A |^ h = A } ; { h where h is Element of G : A |^ h = A } c= the carrier of G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { h where h is Element of G : A |^ h = A } or x in the carrier of G ) assume x in { h where h is Element of G : A |^ h = A } ; ::_thesis: x in the carrier of G then ex h being Element of G st ( x = h & A |^ h = A ) ; hence x in the carrier of G ; ::_thesis: verum end; then reconsider X = { h where h is Element of G : A |^ h = A } as Subset of G ; A1: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_X_&_b_in_X_holds_ a_*_b_in_X let a, b be Element of G; ::_thesis: ( a in X & b in X implies a * b in X ) assume ( a in X & b in X ) ; ::_thesis: a * b in X then ( ex g being Element of G st ( a = g & A |^ g = A ) & ex h being Element of G st ( b = h & A |^ h = A ) ) ; then A |^ (a * b) = A by Th47; hence a * b in X ; ::_thesis: verum end; A2: now__::_thesis:_for_a_being_Element_of_G_st_a_in_X_holds_ a_"_in_X let a be Element of G; ::_thesis: ( a in X implies a " in X ) assume a in X ; ::_thesis: a " in X then ex b being Element of G st ( a = b & A |^ b = A ) ; then A = A |^ (a ") by Th54; hence a " in X ; ::_thesis: verum end; A |^ (1_ G) = A by Th52; then 1_ G in X ; hence ex b1 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A } by A1, A2, GROUP_2:52; ::_thesis: verum end; uniqueness for b1, b2 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A } & the carrier of b2 = { h where h is Element of G : A |^ h = A } holds b1 = b2 by GROUP_2:59; end; :: deftheorem Def14 defines Normalizer GROUP_3:def_14_:_ for G being Group for A being Subset of G for b3 being strict Subgroup of G holds ( b3 = Normalizer A iff the carrier of b3 = { h where h is Element of G : A |^ h = A } ); theorem Th129: :: GROUP_3:129 for x being set for G being Group for A being Subset of G holds ( x in Normalizer A iff ex h being Element of G st ( x = h & A |^ h = A ) ) proof let x be set ; ::_thesis: for G being Group for A being Subset of G holds ( x in Normalizer A iff ex h being Element of G st ( x = h & A |^ h = A ) ) let G be Group; ::_thesis: for A being Subset of G holds ( x in Normalizer A iff ex h being Element of G st ( x = h & A |^ h = A ) ) let A be Subset of G; ::_thesis: ( x in Normalizer A iff ex h being Element of G st ( x = h & A |^ h = A ) ) thus ( x in Normalizer A implies ex h being Element of G st ( x = h & A |^ h = A ) ) ::_thesis: ( ex h being Element of G st ( x = h & A |^ h = A ) implies x in Normalizer A ) proof assume x in Normalizer A ; ::_thesis: ex h being Element of G st ( x = h & A |^ h = A ) then x in the carrier of (Normalizer A) by STRUCT_0:def_5; then x in { h where h is Element of G : A |^ h = A } by Def14; hence ex h being Element of G st ( x = h & A |^ h = A ) ; ::_thesis: verum end; given h being Element of G such that A1: ( x = h & A |^ h = A ) ; ::_thesis: x in Normalizer A x in { b where b is Element of G : A |^ b = A } by A1; then x in the carrier of (Normalizer A) by Def14; hence x in Normalizer A by STRUCT_0:def_5; ::_thesis: verum end; theorem Th130: :: GROUP_3:130 for G being Group for A being Subset of G holds card (con_class A) = Index (Normalizer A) proof let G be Group; ::_thesis: for A being Subset of G holds card (con_class A) = Index (Normalizer A) let A be Subset of G; ::_thesis: card (con_class A) = Index (Normalizer A) defpred S1[ set , set ] means ex a being Element of G st ( \$1 = A |^ a & \$2 = (Normalizer A) * a ); A1: for x being set st x in con_class A holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in con_class A implies ex y being set st S1[x,y] ) assume x in con_class A ; ::_thesis: ex y being set st S1[x,y] then consider B being Subset of G such that A2: x = B and A3: A,B are_conjugated ; consider g being Element of G such that A4: B = A |^ g by A3, Th88; reconsider y = (Normalizer A) * g as set ; take y ; ::_thesis: S1[x,y] take g ; ::_thesis: ( x = A |^ g & y = (Normalizer A) * g ) thus ( x = A |^ g & y = (Normalizer A) * g ) by A2, A4; ::_thesis: verum end; consider f being Function such that A5: dom f = con_class A and A6: for x being set st x in con_class A holds S1[x,f . x] from CLASSES1:sch_1(A1); A7: for x, y1, y2 being set st x in con_class A & S1[x,y1] & S1[x,y2] holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( x in con_class A & S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume x in con_class A ; ::_thesis: ( not S1[x,y1] or not S1[x,y2] or y1 = y2 ) given a being Element of G such that A8: x = A |^ a and A9: y1 = (Normalizer A) * a ; ::_thesis: ( not S1[x,y2] or y1 = y2 ) given b being Element of G such that A10: x = A |^ b and A11: y2 = (Normalizer A) * b ; ::_thesis: y1 = y2 A = (A |^ b) |^ (a ") by A8, A10, Th54 .= A |^ (b * (a ")) by Th47 ; then b * (a ") in Normalizer A by Th129; hence y1 = y2 by A9, A11, GROUP_2:120; ::_thesis: verum end; A12: rng f = Right_Cosets (Normalizer A) proof thus rng f c= Right_Cosets (Normalizer A) :: according to XBOOLE_0:def_10 ::_thesis: Right_Cosets (Normalizer A) c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Right_Cosets (Normalizer A) ) assume x in rng f ; ::_thesis: x in Right_Cosets (Normalizer A) then consider y being set such that A13: ( y in dom f & f . y = x ) by FUNCT_1:def_3; ex a being Element of G st ( y = A |^ a & x = (Normalizer A) * a ) by A5, A6, A13; hence x in Right_Cosets (Normalizer A) by GROUP_2:def_16; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets (Normalizer A) or x in rng f ) assume x in Right_Cosets (Normalizer A) ; ::_thesis: x in rng f then consider a being Element of G such that A14: x = (Normalizer A) * a by GROUP_2:def_16; set y = A |^ a; A,A |^ a are_conjugated by Th88; then A15: A |^ a in con_class A ; then ex b being Element of G st ( A |^ a = A |^ b & f . (A |^ a) = (Normalizer A) * b ) by A6; then x = f . (A |^ a) by A7, A14, A15; hence x in rng f by A5, A15, FUNCT_1:def_3; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A16: x in dom f and A17: y in dom f and A18: f . x = f . y ; ::_thesis: x = y consider b being Element of G such that A19: y = A |^ b and A20: f . y = (Normalizer A) * b by A5, A6, A17; consider a being Element of G such that A21: x = A |^ a and A22: f . x = (Normalizer A) * a by A5, A6, A16; b * (a ") in Normalizer A by A18, A22, A20, GROUP_2:120; then ex h being Element of G st ( b * (a ") = h & A |^ h = A ) by Th129; then A = (A |^ b) |^ (a ") by Th47; hence x = y by A21, A19, Th54; ::_thesis: verum end; then con_class A, Right_Cosets (Normalizer A) are_equipotent by A5, A12, WELLORD2:def_4; hence card (con_class A) = card (Right_Cosets (Normalizer A)) by CARD_1:5 .= Index (Normalizer A) by GROUP_2:145 ; ::_thesis: verum end; theorem :: GROUP_3:131 for G being Group for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) holds ex C being finite set st ( C = con_class A & card C = index (Normalizer A) ) proof let G be Group; ::_thesis: for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) holds ex C being finite set st ( C = con_class A & card C = index (Normalizer A) ) let A be Subset of G; ::_thesis: ( ( 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) ) ) A1: card (con_class A) = Index (Normalizer A) by Th130 .= card (Left_Cosets (Normalizer A)) ; then A2: con_class A, Left_Cosets (Normalizer A) are_equipotent by CARD_1:5; assume A3: ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) ; ::_thesis: ex C being finite set st ( C = con_class A & card C = index (Normalizer A) ) then reconsider C = con_class A as finite set by A2, CARD_1:38; take C ; ::_thesis: ( C = con_class A & card C = index (Normalizer A) ) thus C = con_class A ; ::_thesis: card C = index (Normalizer A) Left_Cosets (Normalizer A) is finite by A3, A2, CARD_1:38; hence card C = index (Normalizer A) by A1, GROUP_2:def_18; ::_thesis: verum end; theorem Th132: :: GROUP_3:132 for G being Group for a being Element of G holds card (con_class a) = Index (Normalizer {a}) proof let G be Group; ::_thesis: for a being Element of G holds card (con_class a) = Index (Normalizer {a}) let a be Element of G; ::_thesis: card (con_class a) = Index (Normalizer {a}) deffunc H1( set ) -> set = {\$1}; consider f being Function such that A1: dom f = con_class a and A2: for x being set st x in con_class a holds f . x = H1(x) from FUNCT_1:sch_3(); A3: rng f = con_class {a} proof thus rng f c= con_class {a} :: according to XBOOLE_0:def_10 ::_thesis: con_class {a} c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in con_class {a} ) assume x in rng f ; ::_thesis: x in con_class {a} then consider y being set such that A4: y in dom f and A5: f . y = x by FUNCT_1:def_3; reconsider y = y as Element of G by A1, A4; f . y = {y} by A1, A2, A4; then x in { {d} where d is Element of G : d in con_class a } by A1, A4, A5; hence x in con_class {a} by Th100; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class {a} or x in rng f ) assume x in con_class {a} ; ::_thesis: x in rng f then x in { {b} where b is Element of G : b in con_class a } by Th100; then consider b being Element of G such that A6: x = {b} and A7: b in con_class a ; f . b = {b} by A2, A7; hence x in rng f by A1, A6, A7, FUNCT_1:def_3; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A8: ( x in dom f & y in dom f ) and A9: f . x = f . y ; ::_thesis: x = y ( f . x = {x} & f . y = {y} ) by A1, A2, A8; hence x = y by A9, ZFMISC_1:3; ::_thesis: verum end; then con_class a, con_class {a} are_equipotent by A1, A3, WELLORD2:def_4; hence card (con_class a) = card (con_class {a}) by CARD_1:5 .= Index (Normalizer {a}) by Th130 ; ::_thesis: verum end; theorem :: GROUP_3:133 for G being Group for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) holds ex C being finite set st ( C = con_class a & card C = index (Normalizer {a}) ) proof let G be Group; ::_thesis: for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) holds ex C being finite set st ( C = con_class a & card C = index (Normalizer {a}) ) let a be Element of G; ::_thesis: ( ( 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}) ) ) A1: card (con_class a) = Index (Normalizer {a}) by Th132 .= card (Left_Cosets (Normalizer {a})) ; then A2: con_class a, Left_Cosets (Normalizer {a}) are_equipotent by CARD_1:5; assume A3: ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) ; ::_thesis: ex C being finite set st ( C = con_class a & card C = index (Normalizer {a}) ) then reconsider C = con_class a as finite set by A2, CARD_1:38; take C ; ::_thesis: ( C = con_class a & card C = index (Normalizer {a}) ) thus C = con_class a ; ::_thesis: card C = index (Normalizer {a}) Left_Cosets (Normalizer {a}) is finite by A3, A2, CARD_1:38; hence card C = index (Normalizer {a}) by A1, GROUP_2:def_18; ::_thesis: verum end; definition let G be Group; let H be Subgroup of G; func Normalizer H -> strict Subgroup of G equals :: GROUP_3:def 15 Normalizer (carr H); correctness coherence Normalizer (carr H) is strict Subgroup of G; ; end; :: deftheorem defines Normalizer GROUP_3:def_15_:_ for G being Group for H being Subgroup of G holds Normalizer H = Normalizer (carr H); theorem Th134: :: GROUP_3:134 for x being set for G being Group for H being strict Subgroup of G holds ( x in Normalizer H iff ex h being Element of G st ( x = h & H |^ h = H ) ) proof let x be set ; ::_thesis: for G being Group for H being strict Subgroup of G holds ( x in Normalizer H iff ex h being Element of G st ( x = h & H |^ h = H ) ) let G be Group; ::_thesis: for H being strict Subgroup of G holds ( x in Normalizer H iff ex h being Element of G st ( x = h & H |^ h = H ) ) let H be strict Subgroup of G; ::_thesis: ( x in Normalizer H iff ex h being Element of G st ( x = h & H |^ h = H ) ) thus ( x in Normalizer H implies ex h being Element of G st ( x = h & H |^ h = H ) ) ::_thesis: ( ex h being Element of G st ( x = h & H |^ h = H ) implies x in Normalizer H ) proof assume x in Normalizer H ; ::_thesis: ex h being Element of G st ( x = h & H |^ h = H ) then consider a being Element of G such that A1: x = a and A2: (carr H) |^ a = carr H by Th129; H |^ a = H by A2, Def6; hence ex h being Element of G st ( x = h & H |^ h = H ) by A1; ::_thesis: verum end; given h being Element of G such that A3: x = h and A4: H |^ h = H ; ::_thesis: x in Normalizer H (carr H) |^ h = carr H by A4, Def6; hence x in Normalizer H by A3, Th129; ::_thesis: verum end; theorem Th135: :: GROUP_3:135 for G being Group for H being strict Subgroup of G holds card (con_class H) = Index (Normalizer H) proof let G be Group; ::_thesis: for H being strict Subgroup of G holds card (con_class H) = Index (Normalizer H) let H be strict Subgroup of G; ::_thesis: card (con_class H) = Index (Normalizer H) defpred S1[ set , set ] means ex H1 being strict Subgroup of G st ( \$1 = H1 & \$2 = carr H1 ); A1: for x being set st x in con_class H holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in con_class H implies ex y being set st S1[x,y] ) assume x in con_class H ; ::_thesis: ex y being set st S1[x,y] then reconsider H = x as strict Subgroup of G by Def1; reconsider y = carr H as set ; take y ; ::_thesis: S1[x,y] take H ; ::_thesis: ( x = H & y = carr H ) thus ( x = H & y = carr H ) ; ::_thesis: verum end; consider f being Function such that A2: dom f = con_class H and A3: for x being set st x in con_class H holds S1[x,f . x] from CLASSES1:sch_1(A1); A4: rng f = con_class (carr H) proof thus rng f c= con_class (carr H) :: according to XBOOLE_0:def_10 ::_thesis: con_class (carr H) c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in con_class (carr H) ) assume x in rng f ; ::_thesis: x in con_class (carr H) then consider y being set such that A5: y in dom f and A6: f . y = x by FUNCT_1:def_3; consider H1 being strict Subgroup of G such that A7: y = H1 and A8: x = carr H1 by A2, A3, A5, A6; H1,H are_conjugated by A2, A5, A7, Th107; then carr H1, carr H are_conjugated by Th113; hence x in con_class (carr H) by A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class (carr H) or x in rng f ) assume x in con_class (carr H) ; ::_thesis: x in rng f then consider B being Subset of G such that A9: B = x and A10: carr H,B are_conjugated ; consider H1 being strict Subgroup of G such that A11: the carrier of H1 = B by A10, Th93; B = carr H1 by A11; then H1,H are_conjugated by A10, Th113; then A12: H1 in con_class H by Th107; then ex H2 being strict Subgroup of G st ( H1 = H2 & f . H1 = carr H2 ) by A3; hence x in rng f by A2, A9, A11, A12, FUNCT_1:def_3; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A13: ( x in dom f & y in dom f ) and A14: f . x = f . y ; ::_thesis: x = y ( ex H1 being strict Subgroup of G st ( x = H1 & f . x = carr H1 ) & ex H2 being strict Subgroup of G st ( y = H2 & f . y = carr H2 ) ) by A2, A3, A13; hence x = y by A14, GROUP_2:59; ::_thesis: verum end; then con_class H, con_class (carr H) are_equipotent by A2, A4, WELLORD2:def_4; hence card (con_class H) = card (con_class (carr H)) by CARD_1:5 .= Index (Normalizer H) by Th130 ; ::_thesis: verum end; theorem :: GROUP_3:136 for G being Group for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) holds ex C being finite set st ( C = con_class H & card C = index (Normalizer H) ) proof let G be Group; ::_thesis: for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) holds ex C being finite set st ( C = con_class H & card C = index (Normalizer H) ) let H be strict Subgroup of G; ::_thesis: ( ( 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) ) ) A1: card (con_class H) = Index (Normalizer H) by Th135 .= card (Left_Cosets (Normalizer H)) ; then A2: con_class H, Left_Cosets (Normalizer H) are_equipotent by CARD_1:5; assume A3: ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) ; ::_thesis: ex C being finite set st ( C = con_class H & card C = index (Normalizer H) ) then reconsider C = con_class H as finite set by A2, CARD_1:38; take C ; ::_thesis: ( C = con_class H & card C = index (Normalizer H) ) thus C = con_class H ; ::_thesis: card C = index (Normalizer H) Left_Cosets (Normalizer H) is finite by A3, A2, CARD_1:38; hence card C = index (Normalizer H) by A1, GROUP_2:def_18; ::_thesis: verum end; theorem Th137: :: GROUP_3:137 for G being strict Group for H being strict Subgroup of G holds ( H is normal Subgroup of G iff Normalizer H = G ) proof let G be strict Group; ::_thesis: for H being strict Subgroup of G holds ( H is normal Subgroup of G iff Normalizer H = G ) let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff Normalizer H = G ) thus ( H is normal Subgroup of G implies Normalizer H = G ) ::_thesis: ( Normalizer H = G implies H is normal Subgroup of G ) proof assume A1: H is normal Subgroup of G ; ::_thesis: Normalizer H = G now__::_thesis:_for_a_being_Element_of_G_holds_a_in_Normalizer_H let a be Element of G; ::_thesis: a in Normalizer H H |^ a = H by A1, Def13; hence a in Normalizer H by Th134; ::_thesis: verum end; hence Normalizer H = G by GROUP_2:62; ::_thesis: verum end; assume A2: Normalizer H = G ; ::_thesis: H is normal Subgroup of G H is normal proof let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: H |^ a = multMagma(# the carrier of H, the multF of H #) a in Normalizer H by A2, STRUCT_0:def_5; then ex b being Element of G st ( b = a & H |^ b = H ) by Th134; hence H |^ a = multMagma(# the carrier of H, the multF of H #) ; ::_thesis: verum end; hence H is normal Subgroup of G ; ::_thesis: verum end; theorem :: GROUP_3:138 for G being strict Group holds Normalizer ((1). G) = G proof let G be strict Group; ::_thesis: Normalizer ((1). G) = G (1). G is normal Subgroup of G by Th114; hence Normalizer ((1). G) = G by Th137; ::_thesis: verum end; theorem :: GROUP_3:139 for G being strict Group holds Normalizer ((Omega). G) = G proof let G be strict Group; ::_thesis: Normalizer ((Omega). G) = G (Omega). G is normal Subgroup of G by Th114; hence Normalizer ((Omega). G) = G by Th137; ::_thesis: verum end;