:: GROUP_6 semantic presentation begin theorem Th1: :: GROUP_6:1 for A, B being non empty set for f being Function of A,B holds ( f is one-to-one iff for a, b being Element of A st f . a = f . b holds a = b ) proof let A, B be non empty set ; ::_thesis: for f being Function of A,B holds ( f is one-to-one iff for a, b being Element of A st f . a = f . b holds a = b ) let f be Function of A,B; ::_thesis: ( f is one-to-one iff for a, b being Element of A st f . a = f . b holds a = b ) thus ( f is one-to-one implies for a, b being Element of A st f . a = f . b holds a = b ) by FUNCT_2:19; ::_thesis: ( ( for a, b being Element of A st f . a = f . b holds a = b ) implies f is one-to-one ) assume for a, b being Element of A st f . a = f . b holds a = b ; ::_thesis: f is one-to-one then for a, b being set st a in A & b in A & f . a = f . b holds a = b ; hence f is one-to-one by FUNCT_2:19; ::_thesis: verum end; definition let G be Group; let A be Subgroup of G; :: original: Subgroup redefine mode Subgroup of A -> Subgroup of G; coherence for b1 being Subgroup of A holds b1 is Subgroup of G by GROUP_2:56; end; registration let G be Group; cluster (1). G -> normal ; coherence (1). G is normal by GROUP_3:114; cluster (Omega). G -> normal ; coherence (Omega). G is normal by GROUP_3:114; end; theorem Th2: :: GROUP_6:2 for G being Group for A being Subgroup of G for a being Element of G for X being Subgroup of A for x being Element of A st x = a holds ( x * X = a * X & X * x = X * a ) proof let G be Group; ::_thesis: for A being Subgroup of G for a being Element of G for X being Subgroup of A for x being Element of A st x = a holds ( x * X = a * X & X * x = X * a ) let A be Subgroup of G; ::_thesis: for a being Element of G for X being Subgroup of A for x being Element of A st x = a holds ( x * X = a * X & X * x = X * a ) let a be Element of G; ::_thesis: for X being Subgroup of A for x being Element of A st x = a holds ( x * X = a * X & X * x = X * a ) let X be Subgroup of A; ::_thesis: for x being Element of A st x = a holds ( x * X = a * X & X * x = X * a ) let x be Element of A; ::_thesis: ( x = a implies ( x * X = a * X & X * x = X * a ) ) set I = X; assume A1: x = a ; ::_thesis: ( x * X = a * X & X * x = X * a ) thus x * X c= a * X :: according to XBOOLE_0:def_10 ::_thesis: ( a * X c= x * X & X * x = X * a ) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x * X or y in a * X ) assume y in x * X ; ::_thesis: y in a * X then consider g being Element of A such that A2: ( y = x * g & g in X ) by GROUP_2:103; reconsider h = g as Element of G by GROUP_2:42; a * h = x * g by A1, GROUP_2:43; hence y in a * X by A2, GROUP_2:103; ::_thesis: verum end; thus a * X c= x * X ::_thesis: X * x = X * a proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a * X or y in x * X ) assume y in a * X ; ::_thesis: y in x * X then consider b being Element of G such that A3: y = a * b and A4: b in X by GROUP_2:103; reconsider c = b as Element of X by A4, STRUCT_0:def_5; reconsider c = c as Element of A by GROUP_2:42; a * b = x * c by A1, GROUP_2:43; hence y in x * X by A3, A4, GROUP_2:103; ::_thesis: verum end; thus X * x c= X * a :: according to XBOOLE_0:def_10 ::_thesis: X * a c= X * x proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X * x or y in X * a ) assume y in X * x ; ::_thesis: y in X * a then consider g being Element of A such that A5: ( y = g * x & g in X ) by GROUP_2:104; reconsider h = g as Element of G by GROUP_2:42; h * a = g * x by A1, GROUP_2:43; hence y in X * a by A5, GROUP_2:104; ::_thesis: verum end; thus X * a c= X * x ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X * a or y in X * x ) assume y in X * a ; ::_thesis: y in X * x then consider b being Element of G such that A6: y = b * a and A7: b in X by GROUP_2:104; reconsider c = b as Element of X by A7, STRUCT_0:def_5; reconsider c = c as Element of A by GROUP_2:42; b * a = c * x by A1, GROUP_2:43; hence y in X * x by A6, A7, GROUP_2:104; ::_thesis: verum end; end; theorem :: GROUP_6:3 for G being Group for A being Subgroup of G for X, Y being Subgroup of A holds X /\ Y = X /\ Y proof let G be Group; ::_thesis: for A being Subgroup of G for X, Y being Subgroup of A holds X /\ Y = X /\ Y let A be Subgroup of G; ::_thesis: for X, Y being Subgroup of A holds X /\ Y = X /\ Y let X, Y be Subgroup of A; ::_thesis: X /\ Y = X /\ Y reconsider Z = X /\ Y as Subgroup of G by GROUP_2:56; the carrier of (X /\ Y) = (carr X) /\ (carr Y) by GROUP_2:def_10; then X /\ Y = Z by GROUP_2:80; hence X /\ Y = X /\ Y ; ::_thesis: verum end; theorem Th4: :: GROUP_6:4 for G being Group for a, b being Element of G holds ( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") ) proof let G be Group; ::_thesis: for a, b being Element of G holds ( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") ) let a, b be Element of G; ::_thesis: ( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") ) thus (a * b) * (a ") = (((a ") ") * b) * (a ") .= b |^ (a ") by GROUP_3:def_2 ; ::_thesis: a * (b * (a ")) = b |^ (a ") hence a * (b * (a ")) = b |^ (a ") by GROUP_1:def_3; ::_thesis: verum end; theorem Th5: :: GROUP_6:5 for G being Group for A being Subgroup of G for a being Element of G holds ( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a ) proof let G be Group; ::_thesis: for A being Subgroup of G for a being Element of G holds ( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a ) let A be Subgroup of G; ::_thesis: for a being Element of G holds ( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a ) let a be Element of G; ::_thesis: ( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a ) thus (a * A) * A = a * (A * A) by GROUP_4:45 .= a * A by GROUP_2:76 ; ::_thesis: ( a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a ) hence a * (A * A) = a * A by GROUP_4:45; ::_thesis: ( (A * A) * a = A * a & A * (A * a) = A * a ) thus (A * A) * a = A * a by GROUP_2:76; ::_thesis: A * (A * a) = A * a hence A * (A * a) = A * a by GROUP_4:46; ::_thesis: verum end; theorem Th6: :: GROUP_6:6 for G being Group for A1 being Subset of G st A1 = { [.a,b.] where a, b is Element of G : verum } holds G ` = gr A1 proof let G be Group; ::_thesis: for A1 being Subset of G st A1 = { [.a,b.] where a, b is Element of G : verum } holds G ` = gr A1 let A1 be Subset of G; ::_thesis: ( A1 = { [.a,b.] where a, b is Element of G : verum } implies G ` = gr A1 ) assume A1: A1 = { [.a,b.] where a, b is Element of G : verum } ; ::_thesis: G ` = gr A1 A1 = commutators G proof thus A1 c= commutators G :: according to XBOOLE_0:def_10 ::_thesis: commutators G c= A1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in commutators G ) assume x in A1 ; ::_thesis: x in commutators G then ex a, b being Element of G st x = [.a,b.] by A1; hence x in commutators G by GROUP_5:58; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators G or x in A1 ) assume x in commutators G ; ::_thesis: x in A1 then ex a, b being Element of G st x = [.a,b.] by GROUP_5:58; hence x in A1 by A1; ::_thesis: verum end; hence G ` = gr A1 by GROUP_5:72; ::_thesis: verum end; theorem Th7: :: GROUP_6:7 for G being strict Group for B being strict Subgroup of G holds ( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B ) proof defpred S1[ set , set ] means verum; let G be strict Group; ::_thesis: for B being strict Subgroup of G holds ( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B ) let B be strict Subgroup of G; ::_thesis: ( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B ) thus ( G ` is Subgroup of B implies for a, b being Element of G holds [.a,b.] in B ) by GROUP_2:40, GROUP_5:74; ::_thesis: ( ( for a, b being Element of G holds [.a,b.] in B ) implies G ` is Subgroup of B ) deffunc H1( Element of G, Element of G) -> Element of the carrier of G = [.$1,$2.]; reconsider X = { H1(a,b) where a, b is Element of G : S1[a,b] } as Subset of G from DOMAIN_1:sch_9(); assume A1: for a, b being Element of G holds [.a,b.] in B ; ::_thesis: G ` is Subgroup of B X c= the carrier of B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of B ) assume x in X ; ::_thesis: x in the carrier of B then ex a, b being Element of G st x = [.a,b.] ; then x in B by A1; hence x in the carrier of B by STRUCT_0:def_5; ::_thesis: verum end; then gr X is Subgroup of B by GROUP_4:def_4; hence G ` is Subgroup of B by Th6; ::_thesis: verum end; theorem Th8: :: GROUP_6:8 for G being Group for B being Subgroup of G for N being normal Subgroup of G st N is Subgroup of B holds N is normal Subgroup of B proof let G be Group; ::_thesis: for B being Subgroup of G for N being normal Subgroup of G st N is Subgroup of B holds N is normal Subgroup of B let B be Subgroup of G; ::_thesis: for N being normal Subgroup of G st N is Subgroup of B holds N is normal Subgroup of B let N be normal Subgroup of G; ::_thesis: ( N is Subgroup of B implies N is normal Subgroup of B ) assume N is Subgroup of B ; ::_thesis: N is normal Subgroup of B then reconsider N9 = N as Subgroup of B ; now__::_thesis:_for_n_being_Element_of_B_holds_n_*_N9_c=_N9_*_n let n be Element of B; ::_thesis: n * N9 c= N9 * n thus n * N9 c= N9 * n ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n * N9 or x in N9 * n ) assume x in n * N9 ; ::_thesis: x in N9 * n then consider a being Element of B such that A1: x = n * a and A2: a in N9 by GROUP_2:103; reconsider a9 = a, n9 = n as Element of G by GROUP_2:42; x = n9 * a9 by A1, GROUP_2:43; then A3: x in n9 * N by A2, GROUP_2:103; n9 * N c= N * n9 by GROUP_3:118; then consider a1 being Element of G such that A4: x = a1 * n9 and A5: a1 in N by A3, GROUP_2:104; a1 in N9 by A5; then a1 in B by GROUP_2:40; then reconsider a19 = a1 as Element of B by STRUCT_0:def_5; x = a19 * n by A4, GROUP_2:43; hence x in N9 * n by A5, GROUP_2:104; ::_thesis: verum end; end; hence N is normal Subgroup of B by GROUP_3:118; ::_thesis: verum end; definition let G be Group; let B be Subgroup of G; let M be normal Subgroup of G; assume A1: multMagma(# the carrier of M, the multF of M #) is Subgroup of B ; func(B,M) `*` -> strict normal Subgroup of B equals :Def1: :: GROUP_6:def 1 multMagma(# the carrier of M, the multF of M #); coherence multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B proof reconsider x = multMagma(# the carrier of M, the multF of M #) as Subgroup of G by A1; now__::_thesis:_for_a_being_Element_of_G_holds_a_*_x_=_x_*_a let a be Element of G; ::_thesis: a * x = x * a thus a * x = a * M .= M * a by GROUP_3:117 .= x * a ; ::_thesis: verum end; then x is normal Subgroup of G by GROUP_3:117; hence multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B by A1, Th8; ::_thesis: verum end; correctness ; end; :: deftheorem Def1 defines `*` GROUP_6:def_1_:_ for G being Group for B being Subgroup of G for M being normal Subgroup of G st multMagma(# the carrier of M, the multF of M #) is Subgroup of B holds (B,M) `*` = multMagma(# the carrier of M, the multF of M #); theorem Th9: :: GROUP_6:9 for G being Group for B being Subgroup of G for N being normal Subgroup of G holds ( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B ) proof let G be Group; ::_thesis: for B being Subgroup of G for N being normal Subgroup of G holds ( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B ) let B be Subgroup of G; ::_thesis: for N being normal Subgroup of G holds ( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B ) let N be normal Subgroup of G; ::_thesis: ( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B ) thus B /\ N is normal Subgroup of B ::_thesis: N /\ B is normal Subgroup of B proof reconsider A = B /\ N as Subgroup of B by GROUP_2:88; now__::_thesis:_for_b_being_Element_of_B_holds_b_*_A_c=_A_*_b let b be Element of B; ::_thesis: b * A c= A * b thus b * A c= A * b ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in b * A or x in A * b ) assume x in b * A ; ::_thesis: x in A * b then consider a being Element of B such that A1: x = b * a and A2: a in A by GROUP_2:103; reconsider a9 = a, b9 = b as Element of G by GROUP_2:42; ( a in N & x = b9 * a9 ) by A1, A2, GROUP_2:43, GROUP_2:82; then A3: x in b9 * N by GROUP_2:103; reconsider x9 = x as Element of B by A1; A4: b9 " = b " by GROUP_2:48; b9 * N c= N * b9 by GROUP_3:118; then consider b1 being Element of G such that A5: x = b1 * b9 and A6: b1 in N by A3, GROUP_2:104; reconsider x99 = x as Element of G by A5; b1 = x99 * (b9 ") by A5, GROUP_1:14; then A7: b1 = x9 * (b ") by A4, GROUP_2:43; then reconsider b19 = b1 as Element of B ; b1 in B by A7, STRUCT_0:def_5; then A8: b19 in A by A6, GROUP_2:82; b19 * b = x by A5, GROUP_2:43; hence x in A * b by A8, GROUP_2:104; ::_thesis: verum end; end; hence B /\ N is normal Subgroup of B by GROUP_3:118; ::_thesis: verum end; hence N /\ B is normal Subgroup of B ; ::_thesis: verum end; definition let G be Group; let B be Subgroup of G; let N be normal Subgroup of G; :: original: /\ redefine funcB /\ N -> strict normal Subgroup of B; coherence B /\ N is strict normal Subgroup of B by Th9; end; definition let G be Group; let N be normal Subgroup of G; let B be Subgroup of G; :: original: /\ redefine funcN /\ B -> strict normal Subgroup of B; coherence N /\ B is strict normal Subgroup of B by Th9; end; definition let G be non empty 1-sorted ; redefine attr G is trivial means :Def2: :: GROUP_6:def 2 ex x being set st the carrier of G = {x}; compatibility ( G is trivial iff ex x being set st the carrier of G = {x} ) proof hereby ::_thesis: ( ex x being set st the carrier of G = {x} implies G is trivial ) set y = the Element of G; assume G is trivial ; ::_thesis: ex x being set st the carrier of G = {x} then for x being set holds ( x in the carrier of G iff x = the Element of G ) by STRUCT_0:def_10; then the carrier of G = { the Element of G} by TARSKI:def_1; hence ex x being set st the carrier of G = {x} ; ::_thesis: verum end; given x being set such that A1: the carrier of G = {x} ; ::_thesis: G is trivial now__::_thesis:_for_a,_b_being_Element_of_G_holds_a_=_b let a, b be Element of G; ::_thesis: a = b thus a = x by A1, TARSKI:def_1 .= b by A1, TARSKI:def_1 ; ::_thesis: verum end; hence G is trivial by STRUCT_0:def_10; ::_thesis: verum end; end; :: deftheorem Def2 defines trivial GROUP_6:def_2_:_ for G being non empty 1-sorted holds ( G is trivial iff ex x being set st the carrier of G = {x} ); theorem Th10: :: GROUP_6:10 for G being Group holds (1). G is trivial proof let G be Group; ::_thesis: (1). G is trivial the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7; hence (1). G is trivial by Def2; ::_thesis: verum end; registration let G be Group; cluster (1). G -> trivial ; coherence (1). G is trivial by Th10; end; registration cluster non empty trivial strict unital Group-like associative for multMagma ; existence ex b1 being Group st ( b1 is strict & b1 is trivial ) proof set G = the Group; take (1). the Group ; ::_thesis: ( (1). the Group is strict & (1). the Group is trivial ) thus ( (1). the Group is strict & (1). the Group is trivial ) ; ::_thesis: verum end; end; theorem Th11: :: GROUP_6:11 ( ( for G being trivial Group holds ( card G = 1 & G is finite ) ) & ( for G being finite Group st card G = 1 holds G is trivial ) ) proof thus for G being trivial Group holds ( card G = 1 & G is finite ) ::_thesis: for G being finite Group st card G = 1 holds G is trivial proof let G be trivial Group; ::_thesis: ( card G = 1 & G is finite ) ex x being set st the carrier of G = {x} by Def2; hence ( card G = 1 & G is finite ) by CARD_1:30; ::_thesis: verum end; let G be finite Group; ::_thesis: ( card G = 1 implies G is trivial ) assume card G = 1 ; ::_thesis: G is trivial hence ex x being set st the carrier of G = {x} by CARD_2:42; :: according to GROUP_6:def_2 ::_thesis: verum end; theorem Th12: :: GROUP_6:12 for G being trivial strict Group holds (1). G = G proof let G be trivial strict Group; ::_thesis: (1). G = G card G = 1 by Th11; then card G = card ((1). G) by GROUP_2:69; hence (1). G = G by GROUP_2:73; ::_thesis: verum end; notation let G be Group; let N be normal Subgroup of G; synonym Cosets N for Left_Cosets N; end; registration let G be Group; let N be normal Subgroup of G; cluster Cosets N -> non empty ; coherence not Cosets N is empty by GROUP_2:135; end; theorem Th13: :: GROUP_6:13 for G being Group for x being set for N being normal Subgroup of G st x in Cosets N holds ex a being Element of G st ( x = a * N & x = N * a ) proof let G be Group; ::_thesis: for x being set for N being normal Subgroup of G st x in Cosets N holds ex a being Element of G st ( x = a * N & x = N * a ) let x be set ; ::_thesis: for N being normal Subgroup of G st x in Cosets N holds ex a being Element of G st ( x = a * N & x = N * a ) let N be normal Subgroup of G; ::_thesis: ( x in Cosets N implies ex a being Element of G st ( x = a * N & x = N * a ) ) assume x in Cosets N ; ::_thesis: ex a being Element of G st ( x = a * N & x = N * a ) then consider a being Element of G such that A1: x = a * N by GROUP_2:def_15; x = N * a by A1, GROUP_3:117; hence ex a being Element of G st ( x = a * N & x = N * a ) by A1; ::_thesis: verum end; theorem Th14: :: GROUP_6:14 for G being Group for a being Element of G for N being normal Subgroup of G holds ( a * N in Cosets N & N * a in Cosets N ) proof let G be Group; ::_thesis: for a being Element of G for N being normal Subgroup of G holds ( a * N in Cosets N & N * a in Cosets N ) let a be Element of G; ::_thesis: for N being normal Subgroup of G holds ( a * N in Cosets N & N * a in Cosets N ) let N be normal Subgroup of G; ::_thesis: ( a * N in Cosets N & N * a in Cosets N ) N * a in Right_Cosets N by GROUP_2:def_16; hence ( a * N in Cosets N & N * a in Cosets N ) by GROUP_2:def_15, GROUP_3:127; ::_thesis: verum end; theorem Th15: :: GROUP_6:15 for G being Group for x being set for N being normal Subgroup of G st x in Cosets N holds x is Subset of G ; theorem Th16: :: GROUP_6:16 for G being Group for A1, A2 being Subset of G for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds A1 * A2 in Cosets N proof let G be Group; ::_thesis: for A1, A2 being Subset of G for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds A1 * A2 in Cosets N let A1, A2 be Subset of G; ::_thesis: for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds A1 * A2 in Cosets N let N be normal Subgroup of G; ::_thesis: ( A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N ) assume that A1: A1 in Cosets N and A2: A2 in Cosets N ; ::_thesis: A1 * A2 in Cosets N consider a being Element of G such that A3: A1 = a * N and A1 = N * a by A1, Th13; consider b being Element of G such that A4: A2 = b * N and A5: A2 = N * b by A2, Th13; A1 * A2 = a * (N * (b * N)) by A3, A4, GROUP_3:10 .= a * ((b * N) * N) by A4, A5, GROUP_3:13 .= a * (b * (N * N)) by GROUP_4:45 .= a * (b * N) by GROUP_2:76 .= (a * b) * N by GROUP_2:105 ; hence A1 * A2 in Cosets N by GROUP_2:def_15; ::_thesis: verum end; definition let G be Group; let N be normal Subgroup of G; func CosOp N -> BinOp of (Cosets N) means :Def3: :: GROUP_6:def 3 for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds it . (W1,W2) = A1 * A2; existence ex b1 being BinOp of (Cosets N) st for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds b1 . (W1,W2) = A1 * A2 proof defpred S1[ Element of Cosets N, Element of Cosets N, set ] means for A1, A2 being Subset of G st $1 = A1 & $2 = A2 holds $3 = A1 * A2; A1: for W1, W2 being Element of Cosets N ex V being Element of Cosets N st S1[W1,W2,V] proof let W1, W2 be Element of Cosets N; ::_thesis: ex V being Element of Cosets N st S1[W1,W2,V] reconsider A1 = W1, A2 = W2 as Subset of G by Th15; reconsider C = A1 * A2 as Element of Cosets N by Th16; take C ; ::_thesis: S1[W1,W2,C] thus S1[W1,W2,C] ; ::_thesis: verum end; thus ex B being BinOp of (Cosets N) st for W1, W2 being Element of Cosets N holds S1[W1,W2,B . (W1,W2)] from BINOP_1:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Cosets N) st ( for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds b1 . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds b2 . (W1,W2) = A1 * A2 ) holds b1 = b2 proof let o1, o2 be BinOp of (Cosets N); ::_thesis: ( ( for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds o1 . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds o2 . (W1,W2) = A1 * A2 ) implies o1 = o2 ) assume A2: for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds o1 . (W1,W2) = A1 * A2 ; ::_thesis: ( ex W1, W2 being Element of Cosets N ex A1, A2 being Subset of G st ( W1 = A1 & W2 = A2 & not o2 . (W1,W2) = A1 * A2 ) or o1 = o2 ) assume A3: for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds o2 . (W1,W2) = A1 * A2 ; ::_thesis: o1 = o2 now__::_thesis:_for_x,_y_being_set_st_x_in_Cosets_N_&_y_in_Cosets_N_holds_ o1_._(x,y)_=_o2_._(x,y) let x, y be set ; ::_thesis: ( x in Cosets N & y in Cosets N implies o1 . (x,y) = o2 . (x,y) ) assume A4: ( x in Cosets N & y in Cosets N ) ; ::_thesis: o1 . (x,y) = o2 . (x,y) then reconsider W = x, V = y as Element of Cosets N ; reconsider A1 = x, A2 = y as Subset of G by A4; o1 . (W,V) = A1 * A2 by A2; hence o1 . (x,y) = o2 . (x,y) by A3; ::_thesis: verum end; hence o1 = o2 by BINOP_1:1; ::_thesis: verum end; end; :: deftheorem Def3 defines CosOp GROUP_6:def_3_:_ for G being Group for N being normal Subgroup of G for b3 being BinOp of (Cosets N) holds ( b3 = CosOp N iff for W1, W2 being Element of Cosets N for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds b3 . (W1,W2) = A1 * A2 ); definition let G be Group; let N be normal Subgroup of G; funcG ./. N -> multMagma equals :: GROUP_6:def 4 multMagma(# (Cosets N),(CosOp N) #); correctness coherence multMagma(# (Cosets N),(CosOp N) #) is multMagma ; ; end; :: deftheorem defines ./. GROUP_6:def_4_:_ for G being Group for N being normal Subgroup of G holds G ./. N = multMagma(# (Cosets N),(CosOp N) #); registration let G be Group; let N be normal Subgroup of G; clusterG ./. N -> non empty strict ; coherence ( G ./. N is strict & not G ./. N is empty ) ; end; theorem :: GROUP_6:17 for G being Group for N being normal Subgroup of G holds the carrier of (G ./. N) = Cosets N ; theorem :: GROUP_6:18 for G being Group for N being normal Subgroup of G holds the multF of (G ./. N) = CosOp N ; definition let G be Group; let N be normal Subgroup of G; let S be Element of (G ./. N); func @ S -> Subset of G equals :: GROUP_6:def 5 S; coherence S is Subset of G by Th15; end; :: deftheorem defines @ GROUP_6:def_5_:_ for G being Group for N being normal Subgroup of G for S being Element of (G ./. N) holds @ S = S; theorem :: GROUP_6:19 for G being Group for N being normal Subgroup of G for T1, T2 being Element of (G ./. N) holds (@ T1) * (@ T2) = T1 * T2 by Def3; theorem :: GROUP_6:20 for G being Group for N being normal Subgroup of G for T1, T2 being Element of (G ./. N) holds @ (T1 * T2) = (@ T1) * (@ T2) by Def3; registration let G be Group; let N be normal Subgroup of G; clusterG ./. N -> Group-like associative ; coherence ( G ./. N is associative & G ./. N is Group-like ) proof thus for f, g, h being Element of (G ./. N) holds f * (g * h) = (f * g) * h :: according to GROUP_1:def_3 ::_thesis: G ./. N is Group-like proof let f, g, h be Element of (G ./. N); ::_thesis: f * (g * h) = (f * g) * h consider a being Element of G such that A1: f = a * N and f = N * a by Th13; consider c being Element of G such that A2: h = c * N and h = N * c by Th13; thus f * (g * h) = (@ f) * (@ (g * h)) by Def3 .= (a * N) * ((@ g) * (@ h)) by A1, Def3 .= ((@ f) * (@ g)) * (c * N) by A1, A2, GROUP_2:10 .= (@ (f * g)) * (@ h) by A2, Def3 .= (f * g) * h by Def3 ; ::_thesis: verum end; reconsider e = carr N as Element of (G ./. N) by GROUP_2:135; take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (G ./. N) holds ( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (G ./. N) st ( b1 * b2 = e & b2 * b1 = e ) ) let h be Element of (G ./. N); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (G ./. N) st ( h * b1 = e & b1 * h = e ) ) consider a being Element of G such that A3: h = a * N and A4: h = N * a by Th13; thus h * e = (a * N) * N by A3, Def3 .= a * (N * N) by GROUP_4:45 .= h by A3, GROUP_2:76 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (G ./. N) st ( h * b1 = e & b1 * h = e ) ) thus e * h = N * (N * a) by A4, Def3 .= (N * N) * a by GROUP_4:46 .= h by A4, GROUP_2:76 ; ::_thesis: ex b1 being Element of the carrier of (G ./. N) st ( h * b1 = e & b1 * h = e ) reconsider g = (a ") * N as Element of (G ./. N) by GROUP_2:def_15; take g ; ::_thesis: ( h * g = e & g * h = e ) thus h * g = (N * a) * ((a ") * N) by A4, Def3 .= ((N * a) * (a ")) * N by GROUP_3:9 .= (N * (a * (a "))) * N by GROUP_2:107 .= (N * (1_ G)) * N by GROUP_1:def_5 .= (carr N) * (carr N) by GROUP_2:109 .= e by GROUP_2:76 ; ::_thesis: g * h = e thus g * h = (@ g) * (@ h) by Def3 .= (((a ") * N) * a) * N by A3, GROUP_3:9 .= ((a ") * (N * a)) * N by GROUP_2:106 .= ((a ") * (a * N)) * N by GROUP_3:117 .= (((a ") * a) * N) * N by GROUP_2:105 .= ((1_ G) * N) * N by GROUP_1:def_5 .= (1_ G) * (N * N) by GROUP_4:45 .= (1_ G) * (carr N) by GROUP_2:76 .= e by GROUP_2:37 ; ::_thesis: verum end; end; theorem :: GROUP_6:21 for G being Group for N being normal Subgroup of G for S being Element of (G ./. N) ex a being Element of G st ( S = a * N & S = N * a ) by Th13; theorem :: GROUP_6:22 for G being Group for a being Element of G for N being normal Subgroup of G holds ( N * a is Element of (G ./. N) & a * N is Element of (G ./. N) & carr N is Element of (G ./. N) ) by Th14, GROUP_2:135; theorem Th23: :: GROUP_6:23 for G being Group for x being set for N being normal Subgroup of G holds ( x in G ./. N iff ex a being Element of G st ( x = a * N & x = N * a ) ) proof let G be Group; ::_thesis: for x being set for N being normal Subgroup of G holds ( x in G ./. N iff ex a being Element of G st ( x = a * N & x = N * a ) ) let x be set ; ::_thesis: for N being normal Subgroup of G holds ( x in G ./. N iff ex a being Element of G st ( x = a * N & x = N * a ) ) let N be normal Subgroup of G; ::_thesis: ( x in G ./. N iff ex a being Element of G st ( x = a * N & x = N * a ) ) thus ( x in G ./. N implies ex a being Element of G st ( x = a * N & x = N * a ) ) ::_thesis: ( ex a being Element of G st ( x = a * N & x = N * a ) implies x in G ./. N ) proof assume x in G ./. N ; ::_thesis: ex a being Element of G st ( x = a * N & x = N * a ) then x is Element of (G ./. N) by STRUCT_0:def_5; hence ex a being Element of G st ( x = a * N & x = N * a ) by Th13; ::_thesis: verum end; given a being Element of G such that A1: x = a * N and x = N * a ; ::_thesis: x in G ./. N x is Element of (G ./. N) by A1, Th14; hence x in G ./. N by STRUCT_0:def_5; ::_thesis: verum end; theorem Th24: :: GROUP_6:24 for G being Group for N being normal Subgroup of G holds 1_ (G ./. N) = carr N proof let G be Group; ::_thesis: for N being normal Subgroup of G holds 1_ (G ./. N) = carr N let N be normal Subgroup of G; ::_thesis: 1_ (G ./. N) = carr N reconsider e = carr N as Element of (G ./. N) by GROUP_2:135; now__::_thesis:_for_h_being_Element_of_(G_./._N)_holds_ (_h_*_e_=_h_&_e_*_h_=_h_) let h be Element of (G ./. N); ::_thesis: ( h * e = h & e * h = h ) consider a being Element of G such that A1: h = a * N and A2: h = N * a by Th13; thus h * e = (a * N) * N by A1, Def3 .= a * (N * N) by GROUP_4:45 .= h by A1, GROUP_2:76 ; ::_thesis: e * h = h thus e * h = N * (N * a) by A2, Def3 .= (N * N) * a by GROUP_4:46 .= h by A2, GROUP_2:76 ; ::_thesis: verum end; hence 1_ (G ./. N) = carr N by GROUP_1:4; ::_thesis: verum end; theorem Th25: :: GROUP_6:25 for G being Group for a being Element of G for N being normal Subgroup of G for S being Element of (G ./. N) st S = a * N holds S " = (a ") * N proof let G be Group; ::_thesis: for a being Element of G for N being normal Subgroup of G for S being Element of (G ./. N) st S = a * N holds S " = (a ") * N let a be Element of G; ::_thesis: for N being normal Subgroup of G for S being Element of (G ./. N) st S = a * N holds S " = (a ") * N let N be normal Subgroup of G; ::_thesis: for S being Element of (G ./. N) st S = a * N holds S " = (a ") * N let S be Element of (G ./. N); ::_thesis: ( S = a * N implies S " = (a ") * N ) reconsider g = (a ") * N as Element of (G ./. N) by Th14; assume A1: S = a * N ; ::_thesis: S " = (a ") * N A2: g * S = (@ g) * (@ S) by Def3 .= (((a ") * N) * a) * N by A1, GROUP_3:9 .= ((a ") * (N * a)) * N by GROUP_2:106 .= ((a ") * (a * N)) * N by GROUP_3:117 .= (((a ") * a) * N) * N by GROUP_2:105 .= ((1_ G) * N) * N by GROUP_1:def_5 .= (1_ G) * (N * N) by GROUP_4:45 .= (1_ G) * (carr N) by GROUP_2:76 .= carr N by GROUP_2:37 ; A3: 1_ (G ./. N) = carr N by Th24; S * g = (@ S) * (@ g) by Def3 .= (N * a) * ((a ") * N) by A1, GROUP_3:117 .= ((N * a) * (a ")) * N by GROUP_3:9 .= (N * (a * (a "))) * N by GROUP_2:107 .= (N * (1_ G)) * N by GROUP_1:def_5 .= (carr N) * (carr N) by GROUP_2:109 .= carr N by GROUP_2:76 ; hence S " = (a ") * N by A2, A3, GROUP_1:def_5; ::_thesis: verum end; theorem :: GROUP_6:26 for G being Group for N being normal Subgroup of G holds card (G ./. N) = Index N ; theorem :: GROUP_6:27 for G being Group for N being normal Subgroup of G st Left_Cosets N is finite holds card (G ./. N) = index N proof let G be Group; ::_thesis: for N being normal Subgroup of G st Left_Cosets N is finite holds card (G ./. N) = index N let N be normal Subgroup of G; ::_thesis: ( Left_Cosets N is finite implies card (G ./. N) = index N ) assume Left_Cosets N is finite ; ::_thesis: card (G ./. N) = index N then reconsider LC = Left_Cosets N as finite set ; thus card (G ./. N) = card LC .= index N by GROUP_2:def_18 ; ::_thesis: verum end; theorem Th28: :: GROUP_6:28 for G being Group for B being Subgroup of G for M being strict normal Subgroup of G st M is Subgroup of B holds B ./. ((B,M) `*`) is Subgroup of G ./. M proof let G be Group; ::_thesis: for B being Subgroup of G for M being strict normal Subgroup of G st M is Subgroup of B holds B ./. ((B,M) `*`) is Subgroup of G ./. M let B be Subgroup of G; ::_thesis: for M being strict normal Subgroup of G st M is Subgroup of B holds B ./. ((B,M) `*`) is Subgroup of G ./. M let M be strict normal Subgroup of G; ::_thesis: ( M is Subgroup of B implies B ./. ((B,M) `*`) is Subgroup of G ./. M ) set I = B ./. ((B,M) `*`); set J = (B,M) `*` ; set g = the multF of (B ./. ((B,M) `*`)); set f = the multF of (G ./. M); set X = [: the carrier of (B ./. ((B,M) `*`)), the carrier of (B ./. ((B,M) `*`)):]; assume A1: M is Subgroup of B ; ::_thesis: B ./. ((B,M) `*`) is Subgroup of G ./. M A2: the carrier of (B ./. ((B,M) `*`)) c= the carrier of (G ./. M) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (B ./. ((B,M) `*`)) or x in the carrier of (G ./. M) ) assume x in the carrier of (B ./. ((B,M) `*`)) ; ::_thesis: x in the carrier of (G ./. M) then consider a being Element of B such that A3: x = a * ((B,M) `*`) and x = ((B,M) `*`) * a by Th13; reconsider b = a as Element of G by GROUP_2:42; (B,M) `*` = M by A1, Def1; then a * ((B,M) `*`) = b * M by Th2; hence x in the carrier of (G ./. M) by A3, Th14; ::_thesis: verum end; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_the_multF_of_(B_./._((B,M)_`*`))_holds_ the_multF_of_(B_./._((B,M)_`*`))_._x_=_the_multF_of_(G_./._M)_._x let x be set ; ::_thesis: ( x in dom the multF of (B ./. ((B,M) `*`)) implies the multF of (B ./. ((B,M) `*`)) . x = the multF of (G ./. M) . x ) assume A5: x in dom the multF of (B ./. ((B,M) `*`)) ; ::_thesis: the multF of (B ./. ((B,M) `*`)) . x = the multF of (G ./. M) . x then consider y, z being set such that A6: [y,z] = x by RELAT_1:def_1; z in the carrier of (B ./. ((B,M) `*`)) by A5, A6, ZFMISC_1:87; then consider b being Element of B such that A7: z = b * ((B,M) `*`) and A8: z = ((B,M) `*`) * b by Th13; y in the carrier of (B ./. ((B,M) `*`)) by A5, A6, ZFMISC_1:87; then consider a being Element of B such that A9: y = a * ((B,M) `*`) and y = ((B,M) `*`) * a by Th13; reconsider W1 = y, W2 = z as Element of Cosets ((B,M) `*`) by A9, A7, Th14; A10: the multF of (B ./. ((B,M) `*`)) . x = the multF of (B ./. ((B,M) `*`)) . (W1,W2) by A6 .= (a * ((B,M) `*`)) * (((B,M) `*`) * b) by A9, A8, Def3 .= ((a * ((B,M) `*`)) * ((B,M) `*`)) * b by GROUP_3:11 .= (a * (((B,M) `*`) * ((B,M) `*`))) * b by GROUP_4:45 .= (a * ((B,M) `*`)) * b by GROUP_2:76 .= a * (((B,M) `*`) * b) by GROUP_2:106 .= a * (b * ((B,M) `*`)) by GROUP_3:117 .= (a * b) * ((B,M) `*`) by GROUP_2:105 ; reconsider a9 = a, b9 = b as Element of G by GROUP_2:42; A11: (B,M) `*` = M by A1, Def1; then A12: y = a9 * M by A9, Th2; z = b9 * M by A7, A11, Th2; then reconsider V1 = y, V2 = z as Element of Cosets M by A12, Th14; A13: a9 * b9 = a * b by GROUP_2:43; A14: z = M * b9 by A8, A11, Th2; the multF of (G ./. M) . x = the multF of (G ./. M) . (V1,V2) by A6 .= (a9 * M) * (M * b9) by A12, A14, Def3 .= ((a9 * M) * M) * b9 by GROUP_3:11 .= (a9 * (M * M)) * b9 by GROUP_4:45 .= (a9 * M) * b9 by GROUP_2:76 .= a9 * (M * b9) by GROUP_2:106 .= a9 * (b9 * M) by GROUP_3:117 .= (a9 * b9) * M by GROUP_2:105 ; hence the multF of (B ./. ((B,M) `*`)) . x = the multF of (G ./. M) . x by A10, A11, A13, Th2; ::_thesis: verum end; ( dom the multF of (B ./. ((B,M) `*`)) = [: the carrier of (B ./. ((B,M) `*`)), the carrier of (B ./. ((B,M) `*`)):] & dom the multF of (G ./. M) = [: the carrier of (G ./. M), the carrier of (G ./. M):] ) by FUNCT_2:def_1; then dom the multF of (B ./. ((B,M) `*`)) = (dom the multF of (G ./. M)) /\ [: the carrier of (B ./. ((B,M) `*`)), the carrier of (B ./. ((B,M) `*`)):] by A2, XBOOLE_1:28, ZFMISC_1:96; then the multF of (B ./. ((B,M) `*`)) = the multF of (G ./. M) || the carrier of (B ./. ((B,M) `*`)) by A4, FUNCT_1:46; hence B ./. ((B,M) `*`) is Subgroup of G ./. M by A2, GROUP_2:def_5; ::_thesis: verum end; theorem :: GROUP_6:29 for G being Group for N, M being strict normal Subgroup of G st M is Subgroup of N holds N ./. ((N,M) `*`) is normal Subgroup of G ./. M proof let G be Group; ::_thesis: for N, M being strict normal Subgroup of G st M is Subgroup of N holds N ./. ((N,M) `*`) is normal Subgroup of G ./. M let N, M be strict normal Subgroup of G; ::_thesis: ( M is Subgroup of N implies N ./. ((N,M) `*`) is normal Subgroup of G ./. M ) assume A1: M is Subgroup of N ; ::_thesis: N ./. ((N,M) `*`) is normal Subgroup of G ./. M then A2: (N,M) `*` = M by Def1; then reconsider I = M as normal Subgroup of N ; reconsider J = N ./. ((N,M) `*`) as Subgroup of G ./. M by A1, Th28; now__::_thesis:_for_S_being_Element_of_(G_./._M)_holds_S_*_J_c=_J_*_S let S be Element of (G ./. M); ::_thesis: S * J c= J * S thus S * J c= J * S ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S * J or x in J * S ) assume x in S * J ; ::_thesis: x in J * S then consider T being Element of (G ./. M) such that A3: x = S * T and A4: T in J by GROUP_2:103; consider c being Element of N such that T = c * I and A5: T = I * c by A2, A4, Th23; reconsider d = c as Element of G by GROUP_2:42; consider a being Element of G such that S = a * M and A6: S = M * a by Th13; set e = a * (d * (a ")); ( c in N & a * (d * (a ")) = d |^ (a ") ) by Th4, STRUCT_0:def_5; then a * (d * (a ")) in N by GROUP_5:3; then reconsider f = a * (d * (a ")) as Element of N by STRUCT_0:def_5; A7: M * (a * (d * (a "))) = I * f by Th2; reconsider V = I * f as Element of J by A2, Th14; A8: V in J by STRUCT_0:def_5; reconsider V = V as Element of (G ./. M) by GROUP_2:42; M * d = I * c by Th2; then x = (M * a) * (M * d) by A3, A6, A5, Def3 .= (M * a) * ((M * d) * (1_ G)) by GROUP_2:37 .= (M * a) * ((M * d) * ((a ") * a)) by GROUP_1:def_5 .= (M * a) * (M * (d * ((a ") * a))) by GROUP_2:107 .= ((M * a) * M) * (d * ((a ") * a)) by GROUP_3:11 .= (M * (a * M)) * (d * ((a ") * a)) by GROUP_3:13 .= (M * (M * a)) * (d * ((a ") * a)) by GROUP_3:117 .= M * ((M * a) * (d * ((a ") * a))) by GROUP_2:98 .= M * (M * (a * (d * ((a ") * a)))) by GROUP_2:107 .= M * (M * (a * ((d * (a ")) * a))) by GROUP_1:def_3 .= M * (M * ((a * (d * (a "))) * a)) by GROUP_1:def_3 .= M * ((M * (a * (d * (a ")))) * a) by GROUP_2:107 .= M * (((a * (d * (a "))) * M) * a) by GROUP_3:117 .= M * ((a * (d * (a "))) * (M * a)) by GROUP_2:106 .= (M * (a * (d * (a ")))) * (M * a) by GROUP_3:12 .= V * S by A6, A7, Def3 ; hence x in J * S by A8, GROUP_2:104; ::_thesis: verum end; end; hence N ./. ((N,M) `*`) is normal Subgroup of G ./. M by GROUP_3:118; ::_thesis: verum end; theorem :: GROUP_6:30 for G being strict Group for N being strict normal Subgroup of G holds ( G ./. N is commutative Group iff G ` is Subgroup of N ) proof let G be strict Group; ::_thesis: for N being strict normal Subgroup of G holds ( G ./. N is commutative Group iff G ` is Subgroup of N ) let N be strict normal Subgroup of G; ::_thesis: ( G ./. N is commutative Group iff G ` is Subgroup of N ) thus ( G ./. N is commutative Group implies G ` is Subgroup of N ) ::_thesis: ( G ` is Subgroup of N implies G ./. N is commutative Group ) proof assume A1: G ./. N is commutative Group ; ::_thesis: G ` is Subgroup of N now__::_thesis:_for_a,_b_being_Element_of_G_holds_[.a,b.]_in_N let a, b be Element of G; ::_thesis: [.a,b.] in N reconsider S = a * N, T = b * N as Element of (G ./. N) by Th14; A2: ( [.S,T.] = 1_ (G ./. N) & 1_ (G ./. N) = carr N ) by A1, Th24, GROUP_5:37; ( S " = (a ") * N & T " = (b ") * N ) by Th25; then A3: (S ") * (T ") = ((a ") * N) * ((b ") * N) by Def3; ( S * T = (a * N) * (b * N) & [.S,T.] = ((S ") * (T ")) * (S * T) ) by Def3, GROUP_5:16; then [.S,T.] = (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by A3, Def3; then carr N = (((a ") * N) * ((b ") * N)) * (a * (N * (b * N))) by A2, GROUP_3:10 .= (((a ") * N) * ((b ") * N)) * (a * ((N * b) * N)) by GROUP_3:13 .= (((a ") * N) * ((b ") * N)) * (a * ((b * N) * N)) by GROUP_3:117 .= (((a ") * N) * ((b ") * N)) * (a * (b * N)) by Th5 .= (((a ") * N) * ((b ") * N)) * ((a * b) * N) by GROUP_2:105 .= ((a ") * (N * ((b ") * N))) * ((a * b) * N) by GROUP_3:10 .= ((a ") * ((N * (b ")) * N)) * ((a * b) * N) by GROUP_3:13 .= ((a ") * (((b ") * N) * N)) * ((a * b) * N) by GROUP_3:117 .= ((a ") * ((b ") * N)) * ((a * b) * N) by Th5 .= (((a ") * (b ")) * N) * ((a * b) * N) by GROUP_2:105 .= ((a ") * (b ")) * (N * ((a * b) * N)) by GROUP_3:10 .= ((a ") * (b ")) * ((N * (a * b)) * N) by GROUP_3:13 .= ((a ") * (b ")) * (((a * b) * N) * N) by GROUP_3:117 .= ((a ") * (b ")) * ((a * b) * N) by Th5 .= (((a ") * (b ")) * (a * b)) * N by GROUP_2:105 .= [.a,b.] * N by GROUP_5:16 ; hence [.a,b.] in N by GROUP_2:113; ::_thesis: verum end; hence G ` is Subgroup of N by Th7; ::_thesis: verum end; assume A4: G ` is Subgroup of N ; ::_thesis: G ./. N is commutative Group now__::_thesis:_for_S,_T_being_Element_of_(G_./._N)_holds_[.S,T.]_=_1__(G_./._N) let S, T be Element of (G ./. N); ::_thesis: [.S,T.] = 1_ (G ./. N) A5: [.S,T.] = ((S ") * (T ")) * (S * T) by GROUP_5:16; consider b being Element of G such that A6: T = b * N and T = N * b by Th13; A7: T " = (b ") * N by A6, Th25; consider a being Element of G such that A8: S = a * N and S = N * a by Th13; S " = (a ") * N by A8, Th25; then A9: (S ") * (T ") = ((a ") * N) * ((b ") * N) by A7, Def3; [.a,b.] in N by A4, Th7; then A10: carr N = [.a,b.] * N by GROUP_2:113 .= (((a ") * (b ")) * (a * b)) * N by GROUP_5:16 .= ((a ") * (b ")) * ((a * b) * N) by GROUP_2:105 .= ((a ") * (b ")) * (((a * b) * N) * N) by Th5 .= ((a ") * (b ")) * ((N * (a * b)) * N) by GROUP_3:117 .= ((a ") * (b ")) * (N * ((a * b) * N)) by GROUP_3:13 .= (((a ") * (b ")) * N) * ((a * b) * N) by GROUP_3:10 .= ((a ") * ((b ") * N)) * ((a * b) * N) by GROUP_2:105 .= ((a ") * (((b ") * N) * N)) * ((a * b) * N) by Th5 .= ((a ") * ((N * (b ")) * N)) * ((a * b) * N) by GROUP_3:117 .= ((a ") * (N * ((b ") * N))) * ((a * b) * N) by GROUP_3:13 .= (((a ") * N) * ((b ") * N)) * ((a * b) * N) by GROUP_3:10 .= (((a ") * N) * ((b ") * N)) * (a * (b * N)) by GROUP_2:105 .= (((a ") * N) * ((b ") * N)) * (a * ((b * N) * N)) by Th5 .= (((a ") * N) * ((b ") * N)) * (a * ((N * b) * N)) by GROUP_3:117 .= (((a ") * N) * ((b ") * N)) * (a * (N * (b * N))) by GROUP_3:13 .= (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by GROUP_3:10 ; S * T = (a * N) * (b * N) by A8, A6, Def3; then [.S,T.] = (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by A9, A5, Def3; hence [.S,T.] = 1_ (G ./. N) by A10, Th24; ::_thesis: verum end; hence G ./. N is commutative Group by GROUP_5:37; ::_thesis: verum end; Lm1: for G, H being Group for a, b being Element of G for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds f . (a * b) = (f . a) * (f . b) proof let G, H be Group; ::_thesis: for a, b being Element of G for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds f . (a * b) = (f . a) * (f . b) let a, b be Element of G; ::_thesis: for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds f . (a * b) = (f . a) * (f . b) let f be Function of the carrier of G, the carrier of H; ::_thesis: ( ( for a being Element of G holds f . a = 1_ H ) implies f . (a * b) = (f . a) * (f . b) ) assume A1: for a being Element of G holds f . a = 1_ H ; ::_thesis: f . (a * b) = (f . a) * (f . b) hence f . (a * b) = 1_ H .= (1_ H) * (1_ H) by GROUP_1:def_4 .= (f . a) * (1_ H) by A1 .= (f . a) * (f . b) by A1 ; ::_thesis: verum end; definition let G, H be non empty multMagma ; let f be Function of G,H; attrf is multiplicative means :Def6: :: GROUP_6:def 6 for a, b being Element of G holds f . (a * b) = (f . a) * (f . b); end; :: deftheorem Def6 defines multiplicative GROUP_6:def_6_:_ for G, H being non empty multMagma for f being Function of G,H holds ( f is multiplicative iff for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) ); registration let G, H be Group; cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty V22( the carrier of G) quasi_total multiplicative for Element of bool [: the carrier of G, the carrier of H:]; existence ex b1 being Function of G,H st b1 is multiplicative proof take f = the carrier of G --> (1_ H); ::_thesis: f is multiplicative for a being Element of G holds f . a = 1_ H by FUNCOP_1:7; hence for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) by Lm1; :: according to GROUP_6:def_6 ::_thesis: verum end; end; definition let G, H be Group; mode Homomorphism of G,H is multiplicative Function of G,H; end; theorem Th31: :: GROUP_6:31 for G, H being Group for g being Homomorphism of G,H holds g . (1_ G) = 1_ H proof let G, H be Group; ::_thesis: for g being Homomorphism of G,H holds g . (1_ G) = 1_ H let g be Homomorphism of G,H; ::_thesis: g . (1_ G) = 1_ H g . (1_ G) = g . ((1_ G) * (1_ G)) by GROUP_1:def_4 .= (g . (1_ G)) * (g . (1_ G)) by Def6 ; hence g . (1_ G) = 1_ H by GROUP_1:7; ::_thesis: verum end; registration let G, H be Group; cluster Function-like quasi_total multiplicative -> unity-preserving for Element of bool [: the carrier of G, the carrier of H:]; coherence for b1 being Homomorphism of G,H holds b1 is unity-preserving proof let g be Homomorphism of G,H; ::_thesis: g is unity-preserving thus g . (1_ G) = 1_ H by Th31; :: according to GROUP_1:def_13 ::_thesis: verum end; end; theorem Th32: :: GROUP_6:32 for G, H being Group for a being Element of G for g being Homomorphism of G,H holds g . (a ") = (g . a) " proof let G, H be Group; ::_thesis: for a being Element of G for g being Homomorphism of G,H holds g . (a ") = (g . a) " let a be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . (a ") = (g . a) " let g be Homomorphism of G,H; ::_thesis: g . (a ") = (g . a) " (g . (a ")) * (g . a) = g . ((a ") * a) by Def6 .= g . (1_ G) by GROUP_1:def_5 .= 1_ H by Th31 ; hence g . (a ") = (g . a) " by GROUP_1:12; ::_thesis: verum end; theorem Th33: :: GROUP_6:33 for G, H being Group for a, b being Element of G for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b) proof let G, H be Group; ::_thesis: for a, b being Element of G for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b) let a, b be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b) let g be Homomorphism of G,H; ::_thesis: g . (a |^ b) = (g . a) |^ (g . b) thus g . (a |^ b) = g . (((b ") * a) * b) by GROUP_3:def_2 .= (g . ((b ") * a)) * (g . b) by Def6 .= ((g . (b ")) * (g . a)) * (g . b) by Def6 .= (((g . b) ") * (g . a)) * (g . b) by Th32 .= (g . a) |^ (g . b) by GROUP_3:def_2 ; ::_thesis: verum end; theorem Th34: :: GROUP_6:34 for G, H being Group for a, b being Element of G for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).] proof let G, H be Group; ::_thesis: for a, b being Element of G for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).] let a, b be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).] let g be Homomorphism of G,H; ::_thesis: g . [.a,b.] = [.(g . a),(g . b).] thus g . [.a,b.] = g . ((((a ") * (b ")) * a) * b) by GROUP_5:16 .= (g . (((a ") * (b ")) * a)) * (g . b) by Def6 .= ((g . ((a ") * (b "))) * (g . a)) * (g . b) by Def6 .= (((g . (a ")) * (g . (b "))) * (g . a)) * (g . b) by Def6 .= ((((g . a) ") * (g . (b "))) * (g . a)) * (g . b) by Th32 .= ((((g . a) ") * ((g . b) ")) * (g . a)) * (g . b) by Th32 .= [.(g . a),(g . b).] by GROUP_5:16 ; ::_thesis: verum end; theorem :: GROUP_6:35 for G, H being Group for a1, a2, a3 being Element of G for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).] proof let G, H be Group; ::_thesis: for a1, a2, a3 being Element of G for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).] let a1, a2, a3 be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).] let g be Homomorphism of G,H; ::_thesis: g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).] thus g . [.a1,a2,a3.] = g . [.[.a1,a2.],a3.] by GROUP_5:def_3 .= [.(g . [.a1,a2.]),(g . a3).] by Th34 .= [.[.(g . a1),(g . a2).],(g . a3).] by Th34 .= [.(g . a1),(g . a2),(g . a3).] by GROUP_5:def_3 ; ::_thesis: verum end; theorem Th36: :: GROUP_6:36 for n being Element of NAT for G, H being Group for a being Element of G for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n proof let n be Element of NAT ; ::_thesis: for G, H being Group for a being Element of G for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n let G, H be Group; ::_thesis: for a being Element of G for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n let a be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n let g be Homomorphism of G,H; ::_thesis: g . (a |^ n) = (g . a) |^ n defpred S1[ Element of NAT ] means g . (a |^ $1) = (g . a) |^ $1; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] thus g . (a |^ (n + 1)) = g . ((a |^ n) * a) by GROUP_1:34 .= ((g . a) |^ n) * (g . a) by A2, Def6 .= (g . a) |^ (n + 1) by GROUP_1:34 ; ::_thesis: verum end; g . (a |^ 0) = g . (1_ G) by GROUP_1:25 .= 1_ H by Th31 .= (g . a) |^ 0 by GROUP_1:25 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence g . (a |^ n) = (g . a) |^ n ; ::_thesis: verum end; theorem :: GROUP_6:37 for i being Integer for G, H being Group for a being Element of G for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i proof let i be Integer; ::_thesis: for G, H being Group for a being Element of G for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i let G, H be Group; ::_thesis: for a being Element of G for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i let a be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i let g be Homomorphism of G,H; ::_thesis: g . (a |^ i) = (g . a) |^ i percases ( i >= 0 or i < 0 ) ; supposeA1: i >= 0 ; ::_thesis: g . (a |^ i) = (g . a) |^ i hence g . (a |^ i) = g . (a |^ (abs i)) by ABSVALUE:def_1 .= (g . a) |^ (abs i) by Th36 .= (g . a) |^ i by A1, ABSVALUE:def_1 ; ::_thesis: verum end; supposeA2: i < 0 ; ::_thesis: g . (a |^ i) = (g . a) |^ i hence g . (a |^ i) = g . ((a |^ (abs i)) ") by GROUP_1:30 .= (g . (a |^ (abs i))) " by Th32 .= ((g . a) |^ (abs i)) " by Th36 .= (g . a) |^ i by A2, GROUP_1:30 ; ::_thesis: verum end; end; end; theorem Th38: :: GROUP_6:38 for G being Group holds id the carrier of G is multiplicative proof let G be Group; ::_thesis: id the carrier of G is multiplicative set f = id the carrier of G; let a be Element of G; :: according to GROUP_6:def_6 ::_thesis: for b being Element of G holds (id the carrier of G) . (a * b) = ((id the carrier of G) . a) * ((id the carrier of G) . b) let b be Element of G; ::_thesis: (id the carrier of G) . (a * b) = ((id the carrier of G) . a) * ((id the carrier of G) . b) thus (id the carrier of G) . (a * b) = a * b by FUNCT_1:18 .= ((id the carrier of G) . a) * b by FUNCT_1:18 .= ((id the carrier of G) . a) * ((id the carrier of G) . b) by FUNCT_1:18 ; ::_thesis: verum end; theorem Th39: :: GROUP_6:39 for G, H, I being Group for h being Homomorphism of G,H for h1 being Homomorphism of H,I holds h1 * h is multiplicative proof let G, H, I be Group; ::_thesis: for h being Homomorphism of G,H for h1 being Homomorphism of H,I holds h1 * h is multiplicative let h be Homomorphism of G,H; ::_thesis: for h1 being Homomorphism of H,I holds h1 * h is multiplicative let h1 be Homomorphism of H,I; ::_thesis: h1 * h is multiplicative set f = h1 * h; let a be Element of G; :: according to GROUP_6:def_6 ::_thesis: for b being Element of G holds (h1 * h) . (a * b) = ((h1 * h) . a) * ((h1 * h) . b) let b be Element of G; ::_thesis: (h1 * h) . (a * b) = ((h1 * h) . a) * ((h1 * h) . b) thus (h1 * h) . (a * b) = h1 . (h . (a * b)) by FUNCT_2:15 .= h1 . ((h . a) * (h . b)) by Def6 .= (h1 . (h . a)) * (h1 . (h . b)) by Def6 .= ((h1 * h) . a) * (h1 . (h . b)) by FUNCT_2:15 .= ((h1 * h) . a) * ((h1 * h) . b) by FUNCT_2:15 ; ::_thesis: verum end; registration let G, H, I be Group; let h be Homomorphism of G,H; let h1 be Homomorphism of H,I; clusterh * h1 -> multiplicative for Function of G,I; coherence for b1 being Function of G,I st b1 = h1 * h holds b1 is multiplicative by Th39; end; definition let G, H be Group; func 1: (G,H) -> Function of G,H means :Def7: :: GROUP_6:def 7 for a being Element of G holds it . a = 1_ H; existence ex b1 being Function of G,H st for a being Element of G holds b1 . a = 1_ H proof take the carrier of G --> (1_ H) ; ::_thesis: for a being Element of G holds ( the carrier of G --> (1_ H)) . a = 1_ H thus for a being Element of G holds ( the carrier of G --> (1_ H)) . a = 1_ H by FUNCOP_1:7; ::_thesis: verum end; uniqueness for b1, b2 being Function of G,H st ( for a being Element of G holds b1 . a = 1_ H ) & ( for a being Element of G holds b2 . a = 1_ H ) holds b1 = b2 proof let g, h be Function of G,H; ::_thesis: ( ( for a being Element of G holds g . a = 1_ H ) & ( for a being Element of G holds h . a = 1_ H ) implies g = h ) assume that A1: for a being Element of G holds g . a = 1_ H and A2: for a being Element of G holds h . a = 1_ H ; ::_thesis: g = h for a being Element of G holds g . a = h . a proof let a be Element of G; ::_thesis: g . a = h . a g . a = 1_ H by A1; hence g . a = h . a by A2; ::_thesis: verum end; hence g = h by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def7 defines 1: GROUP_6:def_7_:_ for G, H being Group for b3 being Function of G,H holds ( b3 = 1: (G,H) iff for a being Element of G holds b3 . a = 1_ H ); registration let G, H be Group; cluster 1: (G,H) -> multiplicative ; coherence 1: (G,H) is multiplicative proof set f = 1: (G,H); let a be Element of G; :: according to GROUP_6:def_6 ::_thesis: for b being Element of G holds (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b) let b be Element of G; ::_thesis: (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b) for a being Element of G holds (1: (G,H)) . a = 1_ H by Def7; hence (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b) by Lm1; ::_thesis: verum end; end; theorem :: GROUP_6:40 for G, H, I being Group for h being Homomorphism of G,H for h1 being Homomorphism of H,I holds ( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) ) proof let G, H, I be Group; ::_thesis: for h being Homomorphism of G,H for h1 being Homomorphism of H,I holds ( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) ) let h be Homomorphism of G,H; ::_thesis: for h1 being Homomorphism of H,I holds ( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) ) let h1 be Homomorphism of H,I; ::_thesis: ( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) ) A1: now__::_thesis:_for_a_being_Element_of_G_holds_((1:_(H,I))_*_h)_._a_=_1__I let a be Element of G; ::_thesis: ((1: (H,I)) * h) . a = 1_ I thus ((1: (H,I)) * h) . a = (1: (H,I)) . (h . a) by FUNCT_2:15 .= 1_ I by Def7 ; ::_thesis: verum end; now__::_thesis:_for_a_being_Element_of_G_holds_(h1_*_(1:_(G,H)))_._a_=_1__I let a be Element of G; ::_thesis: (h1 * (1: (G,H))) . a = 1_ I thus (h1 * (1: (G,H))) . a = h1 . ((1: (G,H)) . a) by FUNCT_2:15 .= h1 . (1_ H) by Def7 .= 1_ I by Th31 ; ::_thesis: verum end; hence ( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) ) by A1, Def7; ::_thesis: verum end; definition let G be Group; let N be normal Subgroup of G; func nat_hom N -> Function of G,(G ./. N) means :Def8: :: GROUP_6:def 8 for a being Element of G holds it . a = a * N; existence ex b1 being Function of G,(G ./. N) st for a being Element of G holds b1 . a = a * N proof defpred S1[ set , set ] means ex a being Element of G st ( $1 = a & $2 = a * N ); A1: for x being set st x in the carrier of G holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier of G implies ex y being set st S1[x,y] ) assume x in the carrier of G ; ::_thesis: ex y being set st S1[x,y] then reconsider a = x as Element of G ; reconsider y = a * N as set ; take y ; ::_thesis: S1[x,y] take a ; ::_thesis: ( x = a & y = a * N ) thus ( x = a & y = a * N ) ; ::_thesis: verum end; consider f being Function such that A2: dom f = the carrier of G and A3: for x being set st x in the carrier of G holds S1[x,f . x] from CLASSES1:sch_1(A1); rng f c= the carrier of (G ./. N) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in the carrier of (G ./. N) ) assume x in rng f ; ::_thesis: x in the carrier of (G ./. N) then consider y being set such that A4: y in dom f and A5: f . y = x by FUNCT_1:def_3; consider a being Element of G such that y = a and A6: f . y = a * N by A2, A3, A4; a * N = N * a by GROUP_3:117; then x in G ./. N by A5, A6, Th23; hence x in the carrier of (G ./. N) by STRUCT_0:def_5; ::_thesis: verum end; then reconsider f = f as Function of G,(G ./. N) by A2, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: for a being Element of G holds f . a = a * N let a be Element of G; ::_thesis: f . a = a * N ex b being Element of G st ( a = b & f . a = b * N ) by A3; hence f . a = a * N ; ::_thesis: verum end; uniqueness for b1, b2 being Function of G,(G ./. N) st ( for a being Element of G holds b1 . a = a * N ) & ( for a being Element of G holds b2 . a = a * N ) holds b1 = b2 proof let n1, n2 be Function of G,(G ./. N); ::_thesis: ( ( for a being Element of G holds n1 . a = a * N ) & ( for a being Element of G holds n2 . a = a * N ) implies n1 = n2 ) assume that A7: for a being Element of G holds n1 . a = a * N and A8: for a being Element of G holds n2 . a = a * N ; ::_thesis: n1 = n2 now__::_thesis:_for_a_being_Element_of_G_holds_n1_._a_=_n2_._a let a be Element of G; ::_thesis: n1 . a = n2 . a n1 . a = a * N by A7; hence n1 . a = n2 . a by A8; ::_thesis: verum end; hence n1 = n2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def8 defines nat_hom GROUP_6:def_8_:_ for G being Group for N being normal Subgroup of G for b3 being Function of G,(G ./. N) holds ( b3 = nat_hom N iff for a being Element of G holds b3 . a = a * N ); registration let G be Group; let N be normal Subgroup of G; cluster nat_hom N -> multiplicative ; coherence nat_hom N is multiplicative proof set f = nat_hom N; let a be Element of G; :: according to GROUP_6:def_6 ::_thesis: for b being Element of G holds (nat_hom N) . (a * b) = ((nat_hom N) . a) * ((nat_hom N) . b) let b be Element of G; ::_thesis: (nat_hom N) . (a * b) = ((nat_hom N) . a) * ((nat_hom N) . b) A1: (nat_hom N) . a = a * N by Def8; A2: (nat_hom N) . b = b * N by Def8; A3: (nat_hom N) . (a * b) = (a * b) * N by Def8; thus ((nat_hom N) . a) * ((nat_hom N) . b) = (@ ((nat_hom N) . a)) * (@ ((nat_hom N) . b)) by Def3 .= ((a * N) * b) * N by A1, A2, GROUP_3:9 .= (a * (N * b)) * N by GROUP_2:106 .= (a * (b * N)) * N by GROUP_3:117 .= a * ((b * N) * N) by GROUP_2:96 .= a * (b * N) by Th5 .= (nat_hom N) . (a * b) by A3, GROUP_2:105 ; ::_thesis: verum end; end; definition let G, H be Group; let g be Homomorphism of G,H; func Ker g -> strict Subgroup of G means :Def9: :: GROUP_6:def 9 the carrier of it = { a where a is Element of G : g . a = 1_ H } ; existence ex b1 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H } proof defpred S1[ set ] means g . $1 = 1_ H; reconsider A = { a where a is Element of G : S1[a] } as Subset of G from DOMAIN_1:sch_7(); A1: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_A_&_b_in_A_holds_ a_*_b_in_A let a, b be Element of G; ::_thesis: ( a in A & b in A implies a * b in A ) assume ( a in A & b in A ) ; ::_thesis: a * b in A then A2: ( ex a1 being Element of G st ( a1 = a & g . a1 = 1_ H ) & ex b1 being Element of G st ( b1 = b & g . b1 = 1_ H ) ) ; g . (a * b) = (g . a) * (g . b) by Def6 .= 1_ H by A2, GROUP_1:def_4 ; hence a * b in A ; ::_thesis: verum end; A3: now__::_thesis:_for_a_being_Element_of_G_st_a_in_A_holds_ a_"_in_A let a be Element of G; ::_thesis: ( a in A implies a " in A ) assume a in A ; ::_thesis: a " in A then ex a1 being Element of G st ( a1 = a & g . a1 = 1_ H ) ; then g . (a ") = (1_ H) " by Th32 .= 1_ H by GROUP_1:8 ; hence a " in A ; ::_thesis: verum end; g . (1_ G) = 1_ H by Th31; then 1_ G in A ; then consider B being strict Subgroup of G such that A4: the carrier of B = A by A1, A3, GROUP_2:52; reconsider B = B as strict Subgroup of G ; take B ; ::_thesis: the carrier of B = { a where a is Element of G : g . a = 1_ H } thus the carrier of B = { a where a is Element of G : g . a = 1_ H } by A4; ::_thesis: verum end; uniqueness for b1, b2 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H } & the carrier of b2 = { a where a is Element of G : g . a = 1_ H } holds b1 = b2 by GROUP_2:59; end; :: deftheorem Def9 defines Ker GROUP_6:def_9_:_ for G, H being Group for g being Homomorphism of G,H for b4 being strict Subgroup of G holds ( b4 = Ker g iff the carrier of b4 = { a where a is Element of G : g . a = 1_ H } ); registration let G, H be Group; let g be Homomorphism of G,H; cluster Ker g -> strict normal ; coherence Ker g is normal proof defpred S1[ set ] means g . G = 1_ H; reconsider A = { a where a is Element of G : S1[a] } as Subset of G from DOMAIN_1:sch_7(); A1: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_A_&_b_in_A_holds_ a_*_b_in_A let a, b be Element of G; ::_thesis: ( a in A & b in A implies a * b in A ) assume ( a in A & b in A ) ; ::_thesis: a * b in A then A2: ( ex a1 being Element of G st ( a1 = a & g . a1 = 1_ H ) & ex b1 being Element of G st ( b1 = b & g . b1 = 1_ H ) ) ; g . (a * b) = (g . a) * (g . b) by Def6 .= 1_ H by A2, GROUP_1:def_4 ; hence a * b in A ; ::_thesis: verum end; A3: now__::_thesis:_for_a_being_Element_of_G_st_a_in_A_holds_ a_"_in_A let a be Element of G; ::_thesis: ( a in A implies a " in A ) assume a in A ; ::_thesis: a " in A then ex a1 being Element of G st ( a1 = a & g . a1 = 1_ H ) ; then g . (a ") = (1_ H) " by Th32 .= 1_ H by GROUP_1:8 ; hence a " in A ; ::_thesis: verum end; g . (1_ G) = 1_ H by Th31; then 1_ G in A ; then consider B being strict Subgroup of G such that A4: the carrier of B = A by A1, A3, GROUP_2:52; now__::_thesis:_for_a_being_Element_of_G_holds_B_|^_a_is_Subgroup_of_B let a be Element of G; ::_thesis: B |^ a is Subgroup of B now__::_thesis:_for_b_being_Element_of_G_st_b_in_B_|^_a_holds_ b_in_B let b be Element of G; ::_thesis: ( b in B |^ a implies b in B ) assume b in B |^ a ; ::_thesis: b in B then consider c being Element of G such that A5: b = c |^ a and A6: c in B by GROUP_3:58; c in A by A4, A6, STRUCT_0:def_5; then ex a1 being Element of G st ( c = a1 & g . a1 = 1_ H ) ; then g . b = (1_ H) |^ (g . a) by A5, Th33 .= 1_ H by GROUP_3:17 ; then b in A ; hence b in B by A4, STRUCT_0:def_5; ::_thesis: verum end; hence B |^ a is Subgroup of B by GROUP_2:58; ::_thesis: verum end; then B is normal Subgroup of G by GROUP_3:122; hence Ker g is normal by A4, Def9; ::_thesis: verum end; end; theorem Th41: :: GROUP_6:41 for G, H being Group for a being Element of G for h being Homomorphism of G,H holds ( a in Ker h iff h . a = 1_ H ) proof let G, H be Group; ::_thesis: for a being Element of G for h being Homomorphism of G,H holds ( a in Ker h iff h . a = 1_ H ) let a be Element of G; ::_thesis: for h being Homomorphism of G,H holds ( a in Ker h iff h . a = 1_ H ) let h be Homomorphism of G,H; ::_thesis: ( a in Ker h iff h . a = 1_ H ) thus ( a in Ker h implies h . a = 1_ H ) ::_thesis: ( h . a = 1_ H implies a in Ker h ) proof assume a in Ker h ; ::_thesis: h . a = 1_ H then a in the carrier of (Ker h) by STRUCT_0:def_5; then a in { b where b is Element of G : h . b = 1_ H } by Def9; then ex b being Element of G st ( a = b & h . b = 1_ H ) ; hence h . a = 1_ H ; ::_thesis: verum end; assume h . a = 1_ H ; ::_thesis: a in Ker h then a in { b where b is Element of G : h . b = 1_ H } ; then a in the carrier of (Ker h) by Def9; hence a in Ker h by STRUCT_0:def_5; ::_thesis: verum end; theorem :: GROUP_6:42 for G, H being strict Group holds Ker (1: (G,H)) = G proof let G, H be strict Group; ::_thesis: Ker (1: (G,H)) = G now__::_thesis:_for_a_being_Element_of_G_holds_a_in_Ker_(1:_(G,H)) let a be Element of G; ::_thesis: a in Ker (1: (G,H)) (1: (G,H)) . a = 1_ H by Def7; hence a in Ker (1: (G,H)) by Th41; ::_thesis: verum end; hence Ker (1: (G,H)) = G by GROUP_2:62; ::_thesis: verum end; theorem Th43: :: GROUP_6:43 for G being Group for N being strict normal Subgroup of G holds Ker (nat_hom N) = N proof let G be Group; ::_thesis: for N being strict normal Subgroup of G holds Ker (nat_hom N) = N let N be strict normal Subgroup of G; ::_thesis: Ker (nat_hom N) = N let a be Element of G; :: according to GROUP_2:def_6 ::_thesis: ( ( not a in Ker (nat_hom N) or a in N ) & ( not a in N or a in Ker (nat_hom N) ) ) thus ( a in Ker (nat_hom N) implies a in N ) ::_thesis: ( not a in N or a in Ker (nat_hom N) ) proof assume a in Ker (nat_hom N) ; ::_thesis: a in N then A1: (nat_hom N) . a = 1_ (G ./. N) by Th41; ( (nat_hom N) . a = a * N & 1_ (G ./. N) = carr N ) by Def8, Th24; hence a in N by A1, GROUP_2:113; ::_thesis: verum end; assume a in N ; ::_thesis: a in Ker (nat_hom N) then A2: a * N = carr N by GROUP_2:113; ( (nat_hom N) . a = a * N & 1_ (G ./. N) = carr N ) by Def8, Th24; hence a in Ker (nat_hom N) by A2, Th41; ::_thesis: verum end; definition let G, H be Group; let g be Homomorphism of G,H; func Image g -> strict Subgroup of H means :Def10: :: GROUP_6:def 10 the carrier of it = g .: the carrier of G; existence ex b1 being strict Subgroup of H st the carrier of b1 = g .: the carrier of G proof the carrier of G c= the carrier of G ; then reconsider X = the carrier of G as Subset of G ; set S = g .: X; A1: now__::_thesis:_for_c,_d_being_Element_of_H_st_c_in_g_.:_X_&_d_in_g_.:_X_holds_ c_*_d_in_g_.:_X let c, d be Element of H; ::_thesis: ( c in g .: X & d in g .: X implies c * d in g .: X ) assume that A2: c in g .: X and A3: d in g .: X ; ::_thesis: c * d in g .: X consider b being Element of G such that b in X and A4: d = g . b by A3, FUNCT_2:65; consider a being Element of G such that a in X and A5: c = g . a by A2, FUNCT_2:65; c * d = g . (a * b) by A5, A4, Def6; hence c * d in g .: X by FUNCT_2:35; ::_thesis: verum end; A6: now__::_thesis:_for_c_being_Element_of_H_st_c_in_g_.:_X_holds_ c_"_in_g_.:_X let c be Element of H; ::_thesis: ( c in g .: X implies c " in g .: X ) assume c in g .: X ; ::_thesis: c " in g .: X then consider a being Element of G such that a in X and A7: c = g . a by FUNCT_2:65; g . (a ") = c " by A7, Th32; hence c " in g .: X by FUNCT_2:35; ::_thesis: verum end; dom g = the carrier of G by FUNCT_2:def_1; then consider D being strict Subgroup of H such that A8: the carrier of D = g .: X by A1, A6, GROUP_2:52; take D ; ::_thesis: the carrier of D = g .: the carrier of G thus the carrier of D = g .: the carrier of G by A8; ::_thesis: verum end; uniqueness for b1, b2 being strict Subgroup of H st the carrier of b1 = g .: the carrier of G & the carrier of b2 = g .: the carrier of G holds b1 = b2 by GROUP_2:59; end; :: deftheorem Def10 defines Image GROUP_6:def_10_:_ for G, H being Group for g being Homomorphism of G,H for b4 being strict Subgroup of H holds ( b4 = Image g iff the carrier of b4 = g .: the carrier of G ); theorem Th44: :: GROUP_6:44 for G, H being Group for g being Homomorphism of G,H holds rng g = the carrier of (Image g) proof let G, H be Group; ::_thesis: for g being Homomorphism of G,H holds rng g = the carrier of (Image g) let g be Homomorphism of G,H; ::_thesis: rng g = the carrier of (Image g) the carrier of (Image g) = g .: the carrier of G by Def10 .= g .: (dom g) by FUNCT_2:def_1 .= rng g by RELAT_1:113 ; hence rng g = the carrier of (Image g) ; ::_thesis: verum end; theorem Th45: :: GROUP_6:45 for H, G being Group for x being set for g being Homomorphism of G,H holds ( x in Image g iff ex a being Element of G st x = g . a ) proof let H, G be Group; ::_thesis: for x being set for g being Homomorphism of G,H holds ( x in Image g iff ex a being Element of G st x = g . a ) let x be set ; ::_thesis: for g being Homomorphism of G,H holds ( x in Image g iff ex a being Element of G st x = g . a ) let g be Homomorphism of G,H; ::_thesis: ( x in Image g iff ex a being Element of G st x = g . a ) thus ( x in Image g implies ex a being Element of G st x = g . a ) ::_thesis: ( ex a being Element of G st x = g . a implies x in Image g ) proof assume x in Image g ; ::_thesis: ex a being Element of G st x = g . a then x in the carrier of (Image g) by STRUCT_0:def_5; then x in g .: the carrier of G by Def10; then consider y being set such that y in dom g and A1: y in the carrier of G and A2: g . y = x by FUNCT_1:def_6; reconsider y = y as Element of G by A1; take y ; ::_thesis: x = g . y thus x = g . y by A2; ::_thesis: verum end; given a being Element of G such that A3: x = g . a ; ::_thesis: x in Image g the carrier of G = dom g by FUNCT_2:def_1; then x in g .: the carrier of G by A3, FUNCT_1:def_6; then x in the carrier of (Image g) by Def10; hence x in Image g by STRUCT_0:def_5; ::_thesis: verum end; theorem :: GROUP_6:46 for G, H being Group for g being Homomorphism of G,H holds Image g = gr (rng g) proof let G, H be Group; ::_thesis: for g being Homomorphism of G,H holds Image g = gr (rng g) let g be Homomorphism of G,H; ::_thesis: Image g = gr (rng g) ( rng g = the carrier of (Image g) & the carrier of (Image g) = carr (Image g) ) by Th44; hence Image g = gr (rng g) by GROUP_4:31; ::_thesis: verum end; theorem :: GROUP_6:47 for G, H being Group holds Image (1: (G,H)) = (1). H proof let G, H be Group; ::_thesis: Image (1: (G,H)) = (1). H set g = 1: (G,H); A1: the carrier of (Image (1: (G,H))) c= {(1_ H)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Image (1: (G,H))) or x in {(1_ H)} ) assume x in the carrier of (Image (1: (G,H))) ; ::_thesis: x in {(1_ H)} then x in (1: (G,H)) .: the carrier of G by Def10; then consider y being set such that y in dom (1: (G,H)) and A2: y in the carrier of G and A3: (1: (G,H)) . y = x by FUNCT_1:def_6; reconsider y = y as Element of G by A2; (1: (G,H)) . y = 1_ H by Def7; hence x in {(1_ H)} by A3, TARSKI:def_1; ::_thesis: verum end; 1_ H in Image (1: (G,H)) by GROUP_2:46; then 1_ H in the carrier of (Image (1: (G,H))) by STRUCT_0:def_5; then {(1_ H)} c= the carrier of (Image (1: (G,H))) by ZFMISC_1:31; then the carrier of (Image (1: (G,H))) = {(1_ H)} by A1, XBOOLE_0:def_10; hence Image (1: (G,H)) = (1). H by GROUP_2:def_7; ::_thesis: verum end; theorem Th48: :: GROUP_6:48 for G being Group for N being normal Subgroup of G holds Image (nat_hom N) = G ./. N proof let G be Group; ::_thesis: for N being normal Subgroup of G holds Image (nat_hom N) = G ./. N let N be normal Subgroup of G; ::_thesis: Image (nat_hom N) = G ./. N now__::_thesis:_for_S_being_Element_of_(G_./._N)_holds_S_in_Image_(nat_hom_N) let S be Element of (G ./. N); ::_thesis: S in Image (nat_hom N) consider a being Element of G such that A1: S = a * N and S = N * a by Th13; (nat_hom N) . a = a * N by Def8; hence S in Image (nat_hom N) by A1, Th45; ::_thesis: verum end; hence Image (nat_hom N) = G ./. N by GROUP_2:62; ::_thesis: verum end; theorem Th49: :: GROUP_6:49 for H, G being Group for h being Homomorphism of G,H holds h is Homomorphism of G,(Image h) proof let H, G be Group; ::_thesis: for h being Homomorphism of G,H holds h is Homomorphism of G,(Image h) let h be Homomorphism of G,H; ::_thesis: h is Homomorphism of G,(Image h) ( rng h = the carrier of (Image h) & dom h = the carrier of G ) by Th44, FUNCT_2:def_1; then reconsider f9 = h as Function of G,(Image h) by RELSET_1:4; now__::_thesis:_for_a,_b_being_Element_of_G_holds_(f9_._a)_*_(f9_._b)_=_f9_._(a_*_b) let a, b be Element of G; ::_thesis: (f9 . a) * (f9 . b) = f9 . (a * b) thus (f9 . a) * (f9 . b) = (h . a) * (h . b) by GROUP_2:43 .= f9 . (a * b) by Def6 ; ::_thesis: verum end; hence h is Homomorphism of G,(Image h) by Def6; ::_thesis: verum end; theorem Th50: :: GROUP_6:50 for H, G being Group for g being Homomorphism of G,H st G is finite holds Image g is finite proof let H, G be Group; ::_thesis: for g being Homomorphism of G,H st G is finite holds Image g is finite let g be Homomorphism of G,H; ::_thesis: ( G is finite implies Image g is finite ) assume G is finite ; ::_thesis: Image g is finite then g .: the carrier of G is finite ; hence Image g is finite by Def10; ::_thesis: verum end; registration let G be finite Group; let H be Group; let g be Homomorphism of G,H; cluster Image g -> finite strict ; coherence Image g is finite by Th50; end; Lm2: for A being commutative Group for a, b being Element of A holds a * b = b * a ; theorem :: GROUP_6:51 for H, G being Group for g being Homomorphism of G,H st G is commutative Group holds Image g is commutative proof let H, G be Group; ::_thesis: for g being Homomorphism of G,H st G is commutative Group holds Image g is commutative let g be Homomorphism of G,H; ::_thesis: ( G is commutative Group implies Image g is commutative ) assume A1: G is commutative Group ; ::_thesis: Image g is commutative let h1, h2 be Element of (Image g); :: according to GROUP_1:def_12 ::_thesis: h1 * h2 = h2 * h1 reconsider c = h1, d = h2 as Element of H by GROUP_2:42; h1 in Image g by STRUCT_0:def_5; then consider a being Element of G such that A2: h1 = g . a by Th45; h2 in Image g by STRUCT_0:def_5; then consider b being Element of G such that A3: h2 = g . b by Th45; thus h1 * h2 = c * d by GROUP_2:43 .= g . (a * b) by A2, A3, Def6 .= g . (b * a) by A1, Lm2 .= d * c by A2, A3, Def6 .= h2 * h1 by GROUP_2:43 ; ::_thesis: verum end; theorem Th52: :: GROUP_6:52 for H, G being Group for g being Homomorphism of G,H holds card (Image g) c= card G proof let H, G be Group; ::_thesis: for g being Homomorphism of G,H holds card (Image g) c= card G let g be Homomorphism of G,H; ::_thesis: card (Image g) c= card G card (g .: the carrier of G) c= card the carrier of G by CARD_1:67; hence card (Image g) c= card G by Def10; ::_thesis: verum end; theorem :: GROUP_6:53 for G being finite Group for H being Group for g being Homomorphism of G,H holds card (Image g) <= card G proof let G be finite Group; ::_thesis: for H being Group for g being Homomorphism of G,H holds card (Image g) <= card G let H be Group; ::_thesis: for g being Homomorphism of G,H holds card (Image g) <= card G let g be Homomorphism of G,H; ::_thesis: card (Image g) <= card G card (Image g) c= card G by Th52; hence card (Image g) <= card G by NAT_1:39; ::_thesis: verum end; theorem :: GROUP_6:54 for G, H being Group for c being Element of H for h being Homomorphism of G,H st h is one-to-one & c in Image h holds h . ((h ") . c) = c proof let G, H be Group; ::_thesis: for c being Element of H for h being Homomorphism of G,H st h is one-to-one & c in Image h holds h . ((h ") . c) = c let c be Element of H; ::_thesis: for h being Homomorphism of G,H st h is one-to-one & c in Image h holds h . ((h ") . c) = c let h be Homomorphism of G,H; ::_thesis: ( h is one-to-one & c in Image h implies h . ((h ") . c) = c ) reconsider h9 = h as Function of G,(Image h) by Th49; assume that A1: h is one-to-one and A2: c in Image h ; ::_thesis: h . ((h ") . c) = c A3: rng h9 = the carrier of (Image h) by Th44; c in the carrier of (Image h) by A2, STRUCT_0:def_5; hence h . ((h ") . c) = c by A1, A3, FUNCT_1:35; ::_thesis: verum end; theorem Th55: :: GROUP_6:55 for H, G being Group for h being Homomorphism of G,H st h is one-to-one holds h " is Homomorphism of (Image h),G proof let H, G be Group; ::_thesis: for h being Homomorphism of G,H st h is one-to-one holds h " is Homomorphism of (Image h),G let h be Homomorphism of G,H; ::_thesis: ( h is one-to-one implies h " is Homomorphism of (Image h),G ) assume A1: h is one-to-one ; ::_thesis: h " is Homomorphism of (Image h),G reconsider Imh = Image h as Group ; ( h is Function of G,Imh & rng h = the carrier of Imh ) by Th44, Th49; then reconsider h9 = h " as Function of Imh,G by A1, FUNCT_2:25; now__::_thesis:_for_a,_b_being_Element_of_Imh_holds_h9_._(a_*_b)_=_(h9_._a)_*_(h9_._b) let a, b be Element of Imh; ::_thesis: h9 . (a * b) = (h9 . a) * (h9 . b) reconsider a9 = a, b9 = b as Element of H by GROUP_2:42; a9 in Imh by STRUCT_0:def_5; then consider a1 being Element of G such that A2: h . a1 = a9 by Th45; b9 in Imh by STRUCT_0:def_5; then consider b1 being Element of G such that A3: h . b1 = b9 by Th45; thus h9 . (a * b) = h9 . ((h . a1) * (h . b1)) by A2, A3, GROUP_2:43 .= h9 . (h . (a1 * b1)) by Def6 .= a1 * b1 by A1, FUNCT_2:26 .= (h9 . a) * b1 by A1, A2, FUNCT_2:26 .= (h9 . a) * (h9 . b) by A1, A3, FUNCT_2:26 ; ::_thesis: verum end; hence h " is Homomorphism of (Image h),G by Def6; ::_thesis: verum end; theorem Th56: :: GROUP_6:56 for H, G being Group for h being Homomorphism of G,H holds ( h is one-to-one iff Ker h = (1). G ) proof let H, G be Group; ::_thesis: for h being Homomorphism of G,H holds ( h is one-to-one iff Ker h = (1). G ) let h be Homomorphism of G,H; ::_thesis: ( h is one-to-one iff Ker h = (1). G ) thus ( h is one-to-one implies Ker h = (1). G ) ::_thesis: ( Ker h = (1). G implies h is one-to-one ) proof assume A1: h is one-to-one ; ::_thesis: Ker h = (1). G now__::_thesis:_for_x_being_set_holds_ (_x_in_the_carrier_of_(Ker_h)_iff_x_=_1__G_) let x be set ; ::_thesis: ( x in the carrier of (Ker h) iff x = 1_ G ) thus ( x in the carrier of (Ker h) iff x = 1_ G ) ::_thesis: verum proof thus ( x in the carrier of (Ker h) implies x = 1_ G ) ::_thesis: ( x = 1_ G implies x in the carrier of (Ker h) ) proof assume A2: x in the carrier of (Ker h) ; ::_thesis: x = 1_ G then x in Ker h by STRUCT_0:def_5; then x in G by GROUP_2:40; then reconsider a = x as Element of G by STRUCT_0:def_5; a in Ker h by A2, STRUCT_0:def_5; then h . a = 1_ H by Th41 .= h . (1_ G) by Th31 ; hence x = 1_ G by A1, Th1; ::_thesis: verum end; assume A3: x = 1_ G ; ::_thesis: x in the carrier of (Ker h) then reconsider a = x as Element of G ; h . a = 1_ H by A3, Th31; then a in Ker h by Th41; hence x in the carrier of (Ker h) by STRUCT_0:def_5; ::_thesis: verum end; end; then the carrier of (Ker h) = {(1_ G)} by TARSKI:def_1; hence Ker h = (1). G by GROUP_2:def_7; ::_thesis: verum end; assume Ker h = (1). G ; ::_thesis: h is one-to-one then A4: the carrier of (Ker h) = {(1_ G)} by GROUP_2:def_7; now__::_thesis:_for_a,_b_being_Element_of_G_st_a_<>_b_holds_ not_h_._a_=_h_._b let a, b be Element of G; ::_thesis: ( a <> b implies not h . a = h . b ) assume that A5: a <> b and A6: h . a = h . b ; ::_thesis: contradiction (h . a) * (h . (a ")) = h . (a * (a ")) by Def6 .= h . (1_ G) by GROUP_1:def_5 .= 1_ H by Th31 ; then 1_ H = h . (b * (a ")) by A6, Def6; then b * (a ") in Ker h by Th41; then A7: b * (a ") in the carrier of (Ker h) by STRUCT_0:def_5; a = (1_ G) * a by GROUP_1:def_4 .= (b * (a ")) * a by A4, A7, TARSKI:def_1 .= b * ((a ") * a) by GROUP_1:def_3 .= b * (1_ G) by GROUP_1:def_5 .= b by GROUP_1:def_4 ; hence contradiction by A5; ::_thesis: verum end; then for a, b being Element of G st h . a = h . b holds a = b ; hence h is one-to-one by Th1; ::_thesis: verum end; theorem Th57: :: GROUP_6:57 for G being Group for H being strict Group for h being Homomorphism of G,H holds ( h is onto iff Image h = H ) proof let G be Group; ::_thesis: for H being strict Group for h being Homomorphism of G,H holds ( h is onto iff Image h = H ) let H be strict Group; ::_thesis: for h being Homomorphism of G,H holds ( h is onto iff Image h = H ) let h be Homomorphism of G,H; ::_thesis: ( h is onto iff Image h = H ) thus ( h is onto implies Image h = H ) ::_thesis: ( Image h = H implies h is onto ) proof assume rng h = the carrier of H ; :: according to FUNCT_2:def_3 ::_thesis: Image h = H then the carrier of (Image h) = the carrier of H by Th44; hence Image h = H by GROUP_2:61; ::_thesis: verum end; assume A1: Image h = H ; ::_thesis: h is onto the carrier of H c= rng h proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H or x in rng h ) assume x in the carrier of H ; ::_thesis: x in rng h then x in h .: the carrier of G by A1, Def10; then ex y being set st ( y in dom h & y in the carrier of G & h . y = x ) by FUNCT_1:def_6; hence x in rng h by FUNCT_1:def_3; ::_thesis: verum end; then rng h = the carrier of H by XBOOLE_0:def_10; hence h is onto by FUNCT_2:def_3; ::_thesis: verum end; theorem Th58: :: GROUP_6:58 for G, H being non empty set for h being Function of G,H st h is onto holds for c being Element of H ex a being Element of G st h . a = c proof let G, H be non empty set ; ::_thesis: for h being Function of G,H st h is onto holds for c being Element of H ex a being Element of G st h . a = c let h be Function of G,H; ::_thesis: ( h is onto implies for c being Element of H ex a being Element of G st h . a = c ) assume A1: rng h = H ; :: according to FUNCT_2:def_3 ::_thesis: for c being Element of H ex a being Element of G st h . a = c let c be Element of H; ::_thesis: ex a being Element of G st h . a = c ex a being set st ( a in G & h . a = c ) by A1, FUNCT_2:11; hence ex a being Element of G st h . a = c ; ::_thesis: verum end; theorem Th59: :: GROUP_6:59 for G being Group for N being normal Subgroup of G holds nat_hom N is onto proof let G be Group; ::_thesis: for N being normal Subgroup of G holds nat_hom N is onto let N be normal Subgroup of G; ::_thesis: nat_hom N is onto Image (nat_hom N) = G ./. N by Th48; hence nat_hom N is onto by Th57; ::_thesis: verum end; theorem Th60: :: GROUP_6:60 for G, H being set for h being Function of G,H holds ( h is bijective iff ( rng h = H & h is one-to-one ) ) proof let G, H be set ; ::_thesis: for h being Function of G,H holds ( h is bijective iff ( rng h = H & h is one-to-one ) ) let h be Function of G,H; ::_thesis: ( h is bijective iff ( rng h = H & h is one-to-one ) ) thus ( h is bijective implies ( rng h = H & h is one-to-one ) ) by FUNCT_2:def_3; ::_thesis: ( rng h = H & h is one-to-one implies h is bijective ) assume ( rng h = H & h is one-to-one ) ; ::_thesis: h is bijective hence ( h is one-to-one & h is onto ) by FUNCT_2:def_3; :: according to FUNCT_2:def_4 ::_thesis: verum end; theorem :: GROUP_6:61 for G being set for H being non empty set for h being Function of G,H st h is bijective holds ( dom h = G & rng h = H ) by FUNCT_2:def_1, FUNCT_2:def_3; theorem Th62: :: GROUP_6:62 for G being Group for H being strict Group for h being Homomorphism of G,H st h is bijective holds h " is Homomorphism of H,G proof let G be Group; ::_thesis: for H being strict Group for h being Homomorphism of G,H st h is bijective holds h " is Homomorphism of H,G let H be strict Group; ::_thesis: for h being Homomorphism of G,H st h is bijective holds h " is Homomorphism of H,G let h be Homomorphism of G,H; ::_thesis: ( h is bijective implies h " is Homomorphism of H,G ) assume A1: ( h is one-to-one & h is onto ) ; :: according to FUNCT_2:def_4 ::_thesis: h " is Homomorphism of H,G then H = Image h by Th57; hence h " is Homomorphism of H,G by A1, Th55; ::_thesis: verum end; theorem Th63: :: GROUP_6:63 for G being set for H being non empty set for h being Function of G,H for g1 being Function of H,G st h is bijective & g1 = h " holds g1 is bijective proof let G be set ; ::_thesis: for H being non empty set for h being Function of G,H for g1 being Function of H,G st h is bijective & g1 = h " holds g1 is bijective let H be non empty set ; ::_thesis: for h being Function of G,H for g1 being Function of H,G st h is bijective & g1 = h " holds g1 is bijective let h be Function of G,H; ::_thesis: for g1 being Function of H,G st h is bijective & g1 = h " holds g1 is bijective let g1 be Function of H,G; ::_thesis: ( h is bijective & g1 = h " implies g1 is bijective ) assume A1: ( h is bijective & g1 = h " ) ; ::_thesis: g1 is bijective then ( dom h = G & rng g1 = dom h ) by FUNCT_1:33, FUNCT_2:def_1; hence g1 is bijective by A1, Th60; ::_thesis: verum end; theorem Th64: :: GROUP_6:64 for G being set for H, I being non empty set for h being Function of G,H for h1 being Function of H,I st h is bijective & h1 is bijective holds h1 * h is bijective proof let G be set ; ::_thesis: for H, I being non empty set for h being Function of G,H for h1 being Function of H,I st h is bijective & h1 is bijective holds h1 * h is bijective let H, I be non empty set ; ::_thesis: for h being Function of G,H for h1 being Function of H,I st h is bijective & h1 is bijective holds h1 * h is bijective let h be Function of G,H; ::_thesis: for h1 being Function of H,I st h is bijective & h1 is bijective holds h1 * h is bijective let h1 be Function of H,I; ::_thesis: ( h is bijective & h1 is bijective implies h1 * h is bijective ) assume that A1: h is bijective and A2: h1 is bijective ; ::_thesis: h1 * h is bijective ( dom h1 = H & rng h = H ) by A1, Th60, FUNCT_2:def_1; then rng (h1 * h) = rng h1 by RELAT_1:28 .= I by A2, Th60 ; hence h1 * h is bijective by A1, A2, Th60; ::_thesis: verum end; theorem Th65: :: GROUP_6:65 for G being Group holds nat_hom ((1). G) is bijective proof let G be Group; ::_thesis: nat_hom ((1). G) is bijective set g = nat_hom ((1). G); Ker (nat_hom ((1). G)) = (1). G by Th43; then A1: nat_hom ((1). G) is one-to-one by Th56; nat_hom ((1). G) is onto by Th59; hence nat_hom ((1). G) is bijective by A1; ::_thesis: verum end; definition let G, H be Group; predG,H are_isomorphic means :Def11: :: GROUP_6:def 11 ex h being Homomorphism of G,H st h is bijective ; reflexivity for G being Group ex h being Homomorphism of G,G st h is bijective proof let G be Group; ::_thesis: ex h being Homomorphism of G,G st h is bijective reconsider i = id the carrier of G as Homomorphism of G,G by Th38; i is bijective ; hence ex h being Homomorphism of G,G st h is bijective ; ::_thesis: verum end; end; :: deftheorem Def11 defines are_isomorphic GROUP_6:def_11_:_ for G, H being Group holds ( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective ); theorem Th66: :: GROUP_6:66 for G, H being strict Group st G,H are_isomorphic holds H,G are_isomorphic proof let G, H be strict Group; ::_thesis: ( G,H are_isomorphic implies H,G are_isomorphic ) assume G,H are_isomorphic ; ::_thesis: H,G are_isomorphic then consider h being Homomorphism of G,H such that A1: h is bijective by Def11; reconsider g = h " as Homomorphism of H,G by A1, Th62; take g ; :: according to GROUP_6:def_11 ::_thesis: g is bijective thus g is bijective by A1, Th63; ::_thesis: verum end; definition let G, H be strict Group; :: original: are_isomorphic redefine predG,H are_isomorphic ; symmetry for G, H being strict Group st (b1,b2) holds (b2,b1) by Th66; end; theorem :: GROUP_6:67 for G, H, I being Group st G,H are_isomorphic & H,I are_isomorphic holds G,I are_isomorphic proof let G, H, I be Group; ::_thesis: ( G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic ) assume that A1: G,H are_isomorphic and A2: H,I are_isomorphic ; ::_thesis: G,I are_isomorphic consider g being Homomorphism of G,H such that A3: g is bijective by A1, Def11; consider h1 being Homomorphism of H,I such that A4: h1 is bijective by A2, Def11; h1 * g is bijective by A3, A4, Th64; hence G,I are_isomorphic by Def11; ::_thesis: verum end; theorem :: GROUP_6:68 for H, G being Group for h being Homomorphism of G,H st h is one-to-one holds G, Image h are_isomorphic proof let H, G be Group; ::_thesis: for h being Homomorphism of G,H st h is one-to-one holds G, Image h are_isomorphic let h be Homomorphism of G,H; ::_thesis: ( h is one-to-one implies G, Image h are_isomorphic ) reconsider ih = h as Homomorphism of G,(Image h) by Th49; assume A1: h is one-to-one ; ::_thesis: G, Image h are_isomorphic take ih ; :: according to GROUP_6:def_11 ::_thesis: ih is bijective the carrier of (Image h) = rng ih by Th44; then ih is onto by FUNCT_2:def_3; hence ih is bijective by A1; ::_thesis: verum end; theorem Th69: :: GROUP_6:69 for G, H being strict Group st G is trivial & H is trivial holds G,H are_isomorphic proof let G, H be strict Group; ::_thesis: ( G is trivial & H is trivial implies G,H are_isomorphic ) assume that A1: G is trivial and A2: H is trivial ; ::_thesis: G,H are_isomorphic take 1: (G,H) ; :: according to GROUP_6:def_11 ::_thesis: 1: (G,H) is bijective A3: H = (1). H by A2, Th12; set h = 1: (G,H); A4: G = (1). G by A1, Th12; now__::_thesis:_for_a,_b_being_Element_of_G_st_(1:_(G,H))_._a_=_(1:_(G,H))_._b_holds_ a_=_b let a, b be Element of G; ::_thesis: ( (1: (G,H)) . a = (1: (G,H)) . b implies a = b ) assume (1: (G,H)) . a = (1: (G,H)) . b ; ::_thesis: a = b a in the carrier of ((1). G) by A4; then a in {(1_ G)} by GROUP_2:def_7; then A5: a = 1_ G by TARSKI:def_1; b in the carrier of ((1). G) by A4; then b in {(1_ G)} by GROUP_2:def_7; hence a = b by A5, TARSKI:def_1; ::_thesis: verum end; then A6: 1: (G,H) is one-to-one by Th1; the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7; then rng (1: (G,H)) = {((1: (G,H)) . (1_ G))} by A4, FUNCT_2:48 .= {(1_ H)} by Def7 .= the carrier of ((1). H) by GROUP_2:def_7 ; then 1: (G,H) is onto by A3, FUNCT_2:def_3; hence 1: (G,H) is bijective by A6; ::_thesis: verum end; theorem :: GROUP_6:70 for G, H being Group holds (1). G, (1). H are_isomorphic by Th69; theorem :: GROUP_6:71 for G being strict Group holds G,G ./. ((1). G) are_isomorphic proof let G be strict Group; ::_thesis: G,G ./. ((1). G) are_isomorphic nat_hom ((1). G) is bijective by Th65; hence G,G ./. ((1). G) are_isomorphic by Def11; ::_thesis: verum end; theorem :: GROUP_6:72 for G being Group holds G ./. ((Omega). G) is trivial proof let G be Group; ::_thesis: G ./. ((Omega). G) is trivial the carrier of (G ./. ((Omega). G)) = { the carrier of G} by GROUP_2:142; hence G ./. ((Omega). G) is trivial by Def2; ::_thesis: verum end; theorem Th73: :: GROUP_6:73 for G, H being strict Group st G,H are_isomorphic holds card G = card H proof let G, H be strict Group; ::_thesis: ( G,H are_isomorphic implies card G = card H ) assume A1: G,H are_isomorphic ; ::_thesis: card G = card H then consider h being Homomorphism of G,H such that A2: h is bijective by Def11; consider g1 being Homomorphism of H,G such that A3: g1 is bijective by A1, Def11; Image g1 = G by A3, Th57; then A4: card G c= card H by Th52; Image h = H by A2, Th57; then card H c= card G by Th52; hence card G = card H by A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th74: :: GROUP_6:74 for G, H being Group st G,H are_isomorphic & G is finite holds H is finite proof let G, H be Group; ::_thesis: ( G,H are_isomorphic & G is finite implies H is finite ) assume that A1: G,H are_isomorphic and A2: G is finite ; ::_thesis: H is finite consider h being Homomorphism of G,H such that A3: h is bijective by A1, Def11; rng h = the carrier of H by A3, FUNCT_2:def_3; hence H is finite by A2; ::_thesis: verum end; theorem :: GROUP_6:75 for G, H being strict Group st G,H are_isomorphic & G is finite holds card G = card H by Th73; theorem :: GROUP_6:76 for G being trivial strict Group for H being strict Group st G,H are_isomorphic holds H is trivial proof let G be trivial strict Group; ::_thesis: for H being strict Group st G,H are_isomorphic holds H is trivial let H be strict Group; ::_thesis: ( G,H are_isomorphic implies H is trivial ) assume A1: G,H are_isomorphic ; ::_thesis: H is trivial then reconsider H = H as finite Group by Th74; card G = 1 by Th11; then card H = 1 by A1, Th73; hence H is trivial by Th11; ::_thesis: verum end; theorem :: GROUP_6:77 for G being Group for H being strict Group st G,H are_isomorphic & G is commutative holds H is commutative proof let G be Group; ::_thesis: for H being strict Group st G,H are_isomorphic & G is commutative holds H is commutative let H be strict Group; ::_thesis: ( G,H are_isomorphic & G is commutative implies H is commutative ) assume that A1: G,H are_isomorphic and A2: G is commutative ; ::_thesis: H is commutative consider h being Homomorphism of G,H such that A3: h is bijective by A1, Def11; now__::_thesis:_for_c,_d_being_Element_of_H_holds_c_*_d_=_d_*_c let c, d be Element of H; ::_thesis: c * d = d * c consider a being Element of G such that A4: h . a = c by A3, Th58; consider b being Element of G such that A5: h . b = d by A3, Th58; thus c * d = h . (a * b) by A4, A5, Def6 .= h . (b * a) by A2, Lm2 .= d * c by A4, A5, Def6 ; ::_thesis: verum end; hence H is commutative by GROUP_1:def_12; ::_thesis: verum end; Lm3: for H, G being Group for g being Homomorphism of G,H holds ( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st ( h is bijective & g = h * (nat_hom (Ker g)) ) ) proof let H, G be Group; ::_thesis: for g being Homomorphism of G,H holds ( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st ( h is bijective & g = h * (nat_hom (Ker g)) ) ) let g be Homomorphism of G,H; ::_thesis: ( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st ( h is bijective & g = h * (nat_hom (Ker g)) ) ) set I = G ./. (Ker g); set J = Image g; defpred S1[ set , set ] means for a being Element of G st $1 = a * (Ker g) holds $2 = g . a; A1: dom (nat_hom (Ker g)) = the carrier of G by FUNCT_2:def_1; A2: for S being Element of (G ./. (Ker g)) ex T being Element of (Image g) st S1[S,T] proof let S be Element of (G ./. (Ker g)); ::_thesis: ex T being Element of (Image g) st S1[S,T] consider a being Element of G such that A3: S = a * (Ker g) and S = (Ker g) * a by Th13; g . a in Image g by Th45; then reconsider T = g . a as Element of (Image g) by STRUCT_0:def_5; take T ; ::_thesis: S1[S,T] let b be Element of G; ::_thesis: ( S = b * (Ker g) implies T = g . b ) assume S = b * (Ker g) ; ::_thesis: T = g . b then (a ") * b in Ker g by A3, GROUP_2:114; then 1_ H = g . ((a ") * b) by Th41 .= (g . (a ")) * (g . b) by Def6 .= ((g . a) ") * (g . b) by Th32 ; then g . b = ((g . a) ") " by GROUP_1:12; hence T = g . b ; ::_thesis: verum end; consider f being Function of (G ./. (Ker g)),(Image g) such that A4: for S being Element of (G ./. (Ker g)) holds S1[S,f . S] from FUNCT_2:sch_3(A2); now__::_thesis:_for_S,_T_being_Element_of_(G_./._(Ker_g))_holds_f_._(S_*_T)_=_(f_._S)_*_(f_._T) let S, T be Element of (G ./. (Ker g)); ::_thesis: f . (S * T) = (f . S) * (f . T) consider a being Element of G such that A5: S = a * (Ker g) and S = (Ker g) * a by Th13; consider b being Element of G such that A6: T = b * (Ker g) and A7: T = (Ker g) * b by Th13; A8: f . T = g . b by A4, A6; f . S = g . a by A4, A5; then A9: (f . S) * (f . T) = (g . a) * (g . b) by A8, GROUP_2:43 .= g . (a * b) by Def6 ; S * T = (a * (Ker g)) * ((Ker g) * b) by A5, A7, Def3 .= ((a * (Ker g)) * (Ker g)) * b by GROUP_3:11 .= (a * (Ker g)) * b by Th5 .= a * ((Ker g) * b) by GROUP_2:106 .= a * (b * (Ker g)) by GROUP_3:117 .= (a * b) * (Ker g) by GROUP_2:105 ; hence f . (S * T) = (f . S) * (f . T) by A4, A9; ::_thesis: verum end; then reconsider f = f as Homomorphism of (G ./. (Ker g)),(Image g) by Def6; A10: f is one-to-one proof let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not y1 in dom f or not b1 in dom f or not f . y1 = f . b1 or y1 = b1 ) let y2 be set ; ::_thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 ) assume ( y1 in dom f & y2 in dom f ) ; ::_thesis: ( not f . y1 = f . y2 or y1 = y2 ) then reconsider S = y1, T = y2 as Element of (G ./. (Ker g)) ; assume A11: f . y1 = f . y2 ; ::_thesis: y1 = y2 consider a being Element of G such that A12: S = a * (Ker g) and S = (Ker g) * a by Th13; consider b being Element of G such that A13: T = b * (Ker g) and T = (Ker g) * b by Th13; A14: f . T = g . b by A4, A13; f . S = g . a by A4, A12; then ((g . b) ") * (g . a) = 1_ H by A11, A14, GROUP_1:def_5; then 1_ H = (g . (b ")) * (g . a) by Th32 .= g . ((b ") * a) by Def6 ; then (b ") * a in Ker g by Th41; hence y1 = y2 by A12, A13, GROUP_2:114; ::_thesis: verum end; A15: dom g = the carrier of G by FUNCT_2:def_1; A16: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_g_implies_(_x_in_dom_(nat_hom_(Ker_g))_&_(nat_hom_(Ker_g))_._x_in_dom_f_)_)_&_(_x_in_dom_(nat_hom_(Ker_g))_&_(nat_hom_(Ker_g))_._x_in_dom_f_implies_x_in_dom_g_)_) let x be set ; ::_thesis: ( ( x in dom g implies ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) ) & ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f implies x in dom g ) ) thus ( x in dom g implies ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) ) ::_thesis: ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f implies x in dom g ) proof assume A17: x in dom g ; ::_thesis: ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) hence x in dom (nat_hom (Ker g)) by A1; ::_thesis: (nat_hom (Ker g)) . x in dom f A18: dom f = the carrier of (G ./. (Ker g)) by FUNCT_2:def_1; (nat_hom (Ker g)) . x in rng (nat_hom (Ker g)) by A1, A17, FUNCT_1:def_3; hence (nat_hom (Ker g)) . x in dom f by A18; ::_thesis: verum end; assume that A19: x in dom (nat_hom (Ker g)) and (nat_hom (Ker g)) . x in dom f ; ::_thesis: x in dom g thus x in dom g by A15, A19; ::_thesis: verum end; the carrier of (Image g) c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Image g) or x in rng f ) assume x in the carrier of (Image g) ; ::_thesis: x in rng f then x in Image g by STRUCT_0:def_5; then consider a being Element of G such that A20: x = g . a by Th45; reconsider S = a * (Ker g) as Element of (G ./. (Ker g)) by Th14; ( f . S = g . a & the carrier of (G ./. (Ker g)) = dom f ) by A4, FUNCT_2:def_1; hence x in rng f by A20, FUNCT_1:def_3; ::_thesis: verum end; then A21: rng f = the carrier of (Image g) by XBOOLE_0:def_10; then f is bijective by A10, Th60; hence G ./. (Ker g), Image g are_isomorphic by Def11; ::_thesis: ex h being Homomorphism of (G ./. (Ker g)),(Image g) st ( h is bijective & g = h * (nat_hom (Ker g)) ) take f ; ::_thesis: ( f is bijective & g = f * (nat_hom (Ker g)) ) thus f is bijective by A21, A10, Th60; ::_thesis: g = f * (nat_hom (Ker g)) now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_ g_._x_=_f_._((nat_hom_(Ker_g))_._x) let x be set ; ::_thesis: ( x in dom g implies g . x = f . ((nat_hom (Ker g)) . x) ) assume x in dom g ; ::_thesis: g . x = f . ((nat_hom (Ker g)) . x) then reconsider a = x as Element of G ; (nat_hom (Ker g)) . a = a * (Ker g) by Def8; hence g . x = f . ((nat_hom (Ker g)) . x) by A4; ::_thesis: verum end; hence g = f * (nat_hom (Ker g)) by A16, FUNCT_1:10; ::_thesis: verum end; theorem :: GROUP_6:78 for H, G being Group for g being Homomorphism of G,H holds G ./. (Ker g), Image g are_isomorphic by Lm3; theorem :: GROUP_6:79 for H, G being Group for g being Homomorphism of G,H ex h being Homomorphism of (G ./. (Ker g)),(Image g) st ( h is bijective & g = h * (nat_hom (Ker g)) ) by Lm3; theorem :: GROUP_6:80 for G being Group for N being normal Subgroup of G for M being strict normal Subgroup of G for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds (G ./. M) ./. J,G ./. N are_isomorphic proof let G be Group; ::_thesis: for N being normal Subgroup of G for M being strict normal Subgroup of G for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds (G ./. M) ./. J,G ./. N are_isomorphic let N be normal Subgroup of G; ::_thesis: for M being strict normal Subgroup of G for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds (G ./. M) ./. J,G ./. N are_isomorphic let M be strict normal Subgroup of G; ::_thesis: for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds (G ./. M) ./. J,G ./. N are_isomorphic let J be strict normal Subgroup of G ./. M; ::_thesis: ( J = N ./. ((N,M) `*`) & M is Subgroup of N implies (G ./. M) ./. J,G ./. N are_isomorphic ) assume that A1: J = N ./. ((N,M) `*`) and A2: M is Subgroup of N ; ::_thesis: (G ./. M) ./. J,G ./. N are_isomorphic defpred S1[ set , set ] means for a being Element of G st $1 = a * M holds $2 = a * N; A3: for x being Element of (G ./. M) ex y being Element of (G ./. N) st S1[x,y] proof let x be Element of (G ./. M); ::_thesis: ex y being Element of (G ./. N) st S1[x,y] consider a being Element of G such that A4: x = a * M and x = M * a by Th13; reconsider y = a * N as Element of (G ./. N) by Th14; take y ; ::_thesis: S1[x,y] let b be Element of G; ::_thesis: ( x = b * M implies y = b * N ) assume x = b * M ; ::_thesis: y = b * N then (a ") * b in M by A4, GROUP_2:114; then (a ") * b in N by A2, GROUP_2:40; hence y = b * N by GROUP_2:114; ::_thesis: verum end; consider f being Function of (G ./. M),(G ./. N) such that A5: for x being Element of (G ./. M) holds S1[x,f . x] from FUNCT_2:sch_3(A3); now__::_thesis:_for_x,_y_being_Element_of_(G_./._M)_holds_f_._(x_*_y)_=_(f_._x)_*_(f_._y) let x, y be Element of (G ./. M); ::_thesis: f . (x * y) = (f . x) * (f . y) consider a being Element of G such that A6: x = a * M and x = M * a by Th13; consider b being Element of G such that A7: y = b * M and y = M * b by Th13; A8: x * y = (@ x) * (@ y) by Def3 .= ((a * M) * b) * M by A6, A7, GROUP_3:9 .= (a * (M * b)) * M by GROUP_2:106 .= (a * (b * M)) * M by GROUP_3:117 .= a * ((b * M) * M) by GROUP_2:96 .= a * (b * M) by Th5 .= (a * b) * M by GROUP_2:105 ; A9: f . y = b * N by A5, A7; A10: f . x = a * N by A5, A6; (f . x) * (f . y) = (@ (f . x)) * (@ (f . y)) by Def3 .= ((a * N) * b) * N by A10, A9, GROUP_3:9 .= (a * (N * b)) * N by GROUP_2:106 .= (a * (b * N)) * N by GROUP_3:117 .= a * ((b * N) * N) by GROUP_2:96 .= a * (b * N) by Th5 .= (a * b) * N by GROUP_2:105 ; hence f . (x * y) = (f . x) * (f . y) by A5, A8; ::_thesis: verum end; then reconsider f = f as Homomorphism of (G ./. M),(G ./. N) by Def6; A11: Ker f = J proof let S be Element of (G ./. M); :: according to GROUP_2:def_6 ::_thesis: ( ( not S in Ker f or S in J ) & ( not S in J or S in Ker f ) ) thus ( S in Ker f implies S in J ) ::_thesis: ( not S in J or S in Ker f ) proof assume S in Ker f ; ::_thesis: S in J then A12: f . S = 1_ (G ./. N) by Th41 .= carr N by Th24 ; consider a being Element of G such that A13: S = a * M and A14: S = M * a by Th13; f . S = a * N by A5, A13; then a in N by A12, GROUP_2:113; then reconsider q = a as Element of N by STRUCT_0:def_5; (N,M) `*` = M by A2, Def1; then ( S = q * ((N,M) `*`) & S = ((N,M) `*`) * q ) by A13, A14, Th2; hence S in J by A1, Th23; ::_thesis: verum end; assume S in J ; ::_thesis: S in Ker f then consider a being Element of N such that A15: S = a * ((N,M) `*`) and S = ((N,M) `*`) * a by A1, Th23; reconsider a9 = a as Element of G by GROUP_2:42; (N,M) `*` = M by A2, Def1; then S = a9 * M by A15, Th2; then A16: f . S = a9 * N by A5; a in N by STRUCT_0:def_5; then f . S = carr N by A16, GROUP_2:113 .= 1_ (G ./. N) by Th24 ; hence S in Ker f by Th41; ::_thesis: verum end; the carrier of (G ./. N) c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (G ./. N) or x in rng f ) assume x in the carrier of (G ./. N) ; ::_thesis: x in rng f then x in G ./. N by STRUCT_0:def_5; then consider a being Element of G such that A17: x = a * N and x = N * a by Th23; reconsider S = a * M as Element of (G ./. M) by Th14; ( f . S = a * N & dom f = the carrier of (G ./. M) ) by A5, FUNCT_2:def_1; hence x in rng f by A17, FUNCT_1:def_3; ::_thesis: verum end; then rng f = the carrier of (G ./. N) by XBOOLE_0:def_10; then f is onto by FUNCT_2:def_3; then Image f = G ./. N by Th57; hence (G ./. M) ./. J,G ./. N are_isomorphic by A11, Lm3; ::_thesis: verum end; theorem :: GROUP_6:81 for G being Group for B being Subgroup of G for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic proof let G be Group; ::_thesis: for B being Subgroup of G for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic let B be Subgroup of G; ::_thesis: for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic let N be strict normal Subgroup of G; ::_thesis: (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic set f = nat_hom N; set g = (nat_hom N) | the carrier of B; set I = (B "\/" N) ./. (((B "\/" N),N) `*`); set J = ((B "\/" N),N) `*` ; A1: the carrier of B c= the carrier of G by GROUP_2:def_5; A2: ( dom ((nat_hom N) | the carrier of B) = (dom (nat_hom N)) /\ the carrier of B & dom (nat_hom N) = the carrier of G ) by FUNCT_2:def_1, RELAT_1:61; then A3: dom ((nat_hom N) | the carrier of B) = the carrier of B by A1, XBOOLE_1:28; A4: N is Subgroup of B "\/" N by GROUP_4:60; then A5: N = ((B "\/" N),N) `*` by Def1; A6: B is Subgroup of B "\/" N by GROUP_4:60; rng ((nat_hom N) | the carrier of B) c= the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((nat_hom N) | the carrier of B) or y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) ) assume y in rng ((nat_hom N) | the carrier of B) ; ::_thesis: y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) then consider x being set such that A7: x in dom ((nat_hom N) | the carrier of B) and A8: ((nat_hom N) | the carrier of B) . x = y by FUNCT_1:def_3; reconsider x = x as Element of B by A2, A1, A7, XBOOLE_1:28; reconsider x9 = x as Element of G by GROUP_2:42; reconsider x99 = x as Element of (B "\/" N) by A6, GROUP_2:42; A9: ( x99 * (((B "\/" N),N) `*`) = x9 * N & N * x9 = (((B "\/" N),N) `*`) * x99 ) by A5, Th2; A10: ((nat_hom N) | the carrier of B) . x = (nat_hom N) . x9 by A7, FUNCT_1:47 .= x9 * N by Def8 ; then ((nat_hom N) | the carrier of B) . x = N * x9 by GROUP_3:117; then y in (B "\/" N) ./. (((B "\/" N),N) `*`) by A8, A10, A9, Th23; hence y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) by STRUCT_0:def_5; ::_thesis: verum end; then reconsider g = (nat_hom N) | the carrier of B as Function of B,((B "\/" N) ./. (((B "\/" N),N) `*`)) by A3, FUNCT_2:def_1, RELSET_1:4; A11: (B "\/" N) ./. (((B "\/" N),N) `*`) is Subgroup of G ./. N by A4, Th28; now__::_thesis:_for_a,_b_being_Element_of_B_holds_g_._(a_*_b)_=_(g_._a)_*_(g_._b) let a, b be Element of B; ::_thesis: g . (a * b) = (g . a) * (g . b) reconsider a9 = a, b9 = b as Element of G by GROUP_2:42; A12: ( (nat_hom N) . a9 = g . a & (nat_hom N) . b9 = g . b ) by FUNCT_1:49; a * b = a9 * b9 by GROUP_2:43; hence g . (a * b) = (nat_hom N) . (a9 * b9) by FUNCT_1:49 .= ((nat_hom N) . a9) * ((nat_hom N) . b9) by Def6 .= (g . a) * (g . b) by A11, A12, GROUP_2:43 ; ::_thesis: verum end; then reconsider g = g as Homomorphism of B,((B "\/" N) ./. (((B "\/" N),N) `*`)) by Def6; A13: Ker g = B /\ N proof let b be Element of B; :: according to GROUP_2:def_6 ::_thesis: ( ( not b in Ker g or b in B /\ N ) & ( not b in B /\ N or b in Ker g ) ) reconsider c = b as Element of G by GROUP_2:42; A14: g . b = (nat_hom N) . c by FUNCT_1:49 .= c * N by Def8 ; thus ( b in Ker g implies b in B /\ N ) ::_thesis: ( not b in B /\ N or b in Ker g ) proof assume b in Ker g ; ::_thesis: b in B /\ N then g . b = 1_ ((B "\/" N) ./. (((B "\/" N),N) `*`)) by Th41 .= carr (((B "\/" N),N) `*`) by Th24 .= carr N by A4, Def1 ; then ( b in B & b in N ) by A14, GROUP_2:113, STRUCT_0:def_5; hence b in B /\ N by GROUP_2:82; ::_thesis: verum end; assume b in B /\ N ; ::_thesis: b in Ker g then b in N by GROUP_2:82; then c * N = carr (((B "\/" N),N) `*`) by A5, GROUP_2:113 .= 1_ ((B "\/" N) ./. (((B "\/" N),N) `*`)) by Th24 ; hence b in Ker g by A14, Th41; ::_thesis: verum end; the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) c= rng g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) or x in rng g ) assume x in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) ; ::_thesis: x in rng g then x in (B "\/" N) ./. (((B "\/" N),N) `*`) by STRUCT_0:def_5; then consider b being Element of (B "\/" N) such that A15: x = b * (((B "\/" N),N) `*`) and x = (((B "\/" N),N) `*`) * b by Th23; ( B * N = N * B & b in B "\/" N ) by GROUP_5:8, STRUCT_0:def_5; then consider a1, a2 being Element of G such that A16: b = a1 * a2 and A17: a1 in B and A18: a2 in N by GROUP_5:5; A19: a1 in the carrier of B by A17, STRUCT_0:def_5; x = (a1 * a2) * N by A5, A15, A16, Th2 .= a1 * (a2 * N) by GROUP_2:105 .= a1 * N by A18, GROUP_2:113 .= (nat_hom N) . a1 by Def8 .= g . a1 by A19, FUNCT_1:49 ; hence x in rng g by A3, A19, FUNCT_1:def_3; ::_thesis: verum end; then the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) = rng g by XBOOLE_0:def_10; then g is onto by FUNCT_2:def_3; then Image g = (B "\/" N) ./. (((B "\/" N),N) `*`) by Th57; hence (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic by A13, Lm3; ::_thesis: verum end;