Copyright (c) 1991 Association of Mizar Users
environ vocabulary FUNCT_1, REALSET1, GROUP_2, GROUP_3, RLSUB_1, INT_1, BOOLE, RELAT_1, GROUP_1, RCOMP_1, SUBSET_1, GROUP_4, GROUP_5, VECTSP_1, NATTRA_1, FINSET_1, CARD_1, BINOP_1, QC_LANG1, ABSVALUE, WELLORD1, LATTICES, GROUP_6; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, CARD_1, FINSET_1, BINOP_1, REALSET1, INT_1, RLVECT_1, VECTSP_1, GROUP_1, GROUP_2, GROUP_3, NAT_1, GROUP_4, GROUP_5; constructors DOMAIN_1, BINOP_1, REALSET1, NAT_1, GROUP_4, GROUP_5, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0; clusters FUNCT_1, FINSET_1, GROUP_1, GROUP_2, GROUP_3, STRUCT_0, RELSET_1, INT_1, FUNCT_2, MEMBERED, ZFMISC_1, PARTFUN1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE; definitions XBOOLE_0, FUNCT_1, GROUP_1, GROUP_2, TARSKI, VECTSP_1, STRUCT_0; theorems BINOP_1, CARD_1, CARD_2, FINSET_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_5, TARSKI, ZFMISC_1, RLVECT_1, REALSET1, VECTSP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1; schemes BINOP_1, COMPLSP1, FUNCT_1, FUNCT_2, DOMAIN_1, NAT_1; begin theorem Th1: for A,B being non empty set, 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; let f be Function of 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:25; assume for a,b being Element of A st f.a = f.b holds a = b; then for a,b being set st a in A & b in A & f.a = f.b holds a = b; hence thesis by FUNCT_2:25; end; definition let G be Group, A be Subgroup of G; redefine mode Subgroup of A -> Subgroup of G; coherence proof let H be Subgroup of A; thus thesis by GROUP_2:65; end; end; definition let G be Group; cluster (1).G -> normal; coherence by GROUP_3:137; cluster (Omega).G -> normal; coherence by GROUP_3:137; end; reserve n for Nat; reserve i for Integer; reserve G,H,I for Group; reserve A,B for Subgroup of G; reserve N for normal Subgroup of G; reserve a,a1,a2,a3,b,b1 for Element of G; reserve c,d for Element of H; reserve f for Function of the carrier of G, the carrier of H; reserve x,y,y1,y2,z for set; reserve A1,A2 for Subset of G; theorem Th2: for X being Subgroup of A, x being Element of A st x = a holds x * X = a * (X qua Subgroup of G) & X * x = (X qua Subgroup of G) * a proof let X be Subgroup of A, x be Element of A; assume A1: x = a; set I = X qua Subgroup of G; thus x * X c= a * I proof let y; assume y in x * X; then consider g being Element of A such that A2: y = x * g & g in X by GROUP_2:125; reconsider h = g as Element of G by GROUP_2:51; a * h = x * g by A1,GROUP_2:52; hence thesis by A2,GROUP_2:125; end; thus a * I c= x * X proof let y; assume y in a * I; then consider b such that A3: y = a * b & b in X by GROUP_2:125; reconsider c = b as Element of X by A3,RLVECT_1:def 1; reconsider c as Element of A by GROUP_2:51; a * b = x * c by A1,GROUP_2:52; hence thesis by A3,GROUP_2:125; end; thus X * x c= I * a proof let y; assume y in X * x; then consider g being Element of A such that A4: y = g * x & g in X by GROUP_2:126; reconsider h = g as Element of G by GROUP_2:51; h * a = g * x by A1,GROUP_2:52; hence thesis by A4,GROUP_2:126; end; thus I * a c= X * x proof let y; assume y in I * a; then consider b such that A5: y = b * a & b in X by GROUP_2:126; reconsider c = b as Element of X by A5,RLVECT_1:def 1; reconsider c as Element of A by GROUP_2:51; b * a = c * x by A1,GROUP_2:52; hence thesis by A5,GROUP_2:126; end; end; theorem for X,Y being Subgroup of A holds (X qua Subgroup of G) /\ (Y qua Subgroup of G) = X /\ Y proof let X,Y be Subgroup of A; A1: the carrier of X /\ Y = (carr X) /\ (carr Y) & the carrier of (X qua Subgroup of G) /\ (Y qua Subgroup of G) = (carr (X qua Subgroup of G)) /\ (carr (Y qua Subgroup of G)) & carr X = the carrier of X & the carrier of Y = carr Y & carr (X qua Subgroup of G) = the carrier of X & the carrier of Y = carr (Y qua Subgroup of G) by GROUP_2:def 9,def 10; reconsider Z = X /\ Y as Subgroup of G by GROUP_2:65; (X qua Subgroup of G) /\ (Y qua Subgroup of G) = Z by A1,GROUP_2:97; hence thesis; end; theorem Th4: a * b * a" = b |^ a" & a * (b * a") = b |^ a" proof thus a * b * a" = a"" * b * a" by GROUP_1:19 .= b |^ a" by GROUP_3:def 2; hence thesis by VECTSP_1:def 16; end; canceled; theorem Th6: a * A * A = a * A & a * (A * A) = a * A & A * A * a = A * a & A * (A * a) = A *a proof thus a * A * A = a * (A * A) by GROUP_4:60 .= a * carr A by GROUP_4:58 .= a * A by GROUP_2:def 13; hence a * (A * A) = a * A by GROUP_4:60; thus A * A * a = carr A * a by GROUP_4:58 .= A * a by GROUP_2:def 14; hence thesis by GROUP_4:61; end; theorem Th7: for G being Group, A1 being Subset of G holds A1 = {[.a,b.] where a is Element of G, b is Element of G : not contradiction} implies G` = gr A1 proof let G be Group, A1 be Subset of G; assume A1: A1 = {[.a,b.] where a is Element of G, b is Element of G : not contradiction}; A1 = commutators G proof thus A1 c= commutators G proof let x; assume x in A1; then ex a,b being Element of G st x = [.a,b.] by A1; hence thesis by GROUP_5:65; end; let x; assume x in commutators G; then ex a,b being Element of G st x = [.a,b.] by GROUP_5:65; hence thesis by A1; end; hence thesis by GROUP_5:82; end; theorem Th8: for G being strict Group, 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 let G be strict Group, B be strict Subgroup of G; thus G` is Subgroup of B implies for a,b being Element of G holds [.a,b.] in B proof assume A1: G` is Subgroup of B; let a,b be Element of G; [.a,b.] in G` by GROUP_5:84; hence thesis by A1,GROUP_2:49; end; assume A2: for a,b being Element of G holds [.a,b.] in B; defpred P[set,set] means not contradiction; deffunc F(Element of G,Element of G) = [.$1,$2.]; reconsider X = {F(a,b) where a is Element of G, b is Element of G : P[a,b]} as Subset of G from SubsetFD2; X c= the carrier of B proof let x; assume x in X; then ex a,b being Element of G st x = [.a,b.]; then x in B by A2; hence thesis by RLVECT_1:def 1; end; then gr X is Subgroup of B by GROUP_4:def 5; hence thesis by Th7; end; theorem Th9: for N being normal Subgroup of G holds N is Subgroup of B implies N is normal Subgroup of B proof let N be normal Subgroup of G; assume N is Subgroup of B; then reconsider N' = N as Subgroup of B; now let n be Element of B; thus n * N' c= N' * n proof let x; assume x in n * N'; then consider a being Element of B such that A1: x = n * a and A2: a in N' by GROUP_2:125; reconsider a' = a, n' = n as Element of G by GROUP_2:51; x = n' * a' by A1,GROUP_2:52; then x in n' * N & n' * N c= N * n' by A2,GROUP_2:125,GROUP_3:141; then consider a1 such that A3: x = a1 * n' and A4: a1 in N by GROUP_2:126; a1 in N' by A4; then a1 in B by GROUP_2:49; then reconsider a1' = a1 as Element of B by RLVECT_1:def 1; x = a1' * n by A3,GROUP_2:52; hence thesis by A4,GROUP_2:126; end; end; hence thesis by GROUP_3:141; end; definition let G,B; let M be normal Subgroup of G; assume A1: the HGrStr of M is Subgroup of B; func (B,M)`*` -> strict normal Subgroup of B equals :Def1: the HGrStr of M; coherence proof reconsider x = the HGrStr of M as Subgroup of G by A1; now let a; A2: carr x = the carrier of M by GROUP_2:def 9 .= carr M by GROUP_2:def 9; thus a * x = a * carr x by GROUP_2:def 13 .= a * M by A2,GROUP_2:def 13 .= M * a by GROUP_3:140 .= carr(M) * a by GROUP_2:def 14 .= x * a by A2,GROUP_2:def 14; end; then x is normal Subgroup of G by GROUP_3:140; hence thesis by A1,Th9; end; correctness; end; theorem Th10: B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B proof thus B /\ N is normal Subgroup of B proof reconsider A = B /\ N as Subgroup of B by GROUP_2:106; now let b be Element of B; thus b * A c= A * b proof let x; assume x in b * A; then consider a being Element of B such that A1: x = b * a and A2: a in A by GROUP_2:125; A3: a in N by A2,GROUP_2:99; reconsider a' = a, b' = b as Element of G by GROUP_2:51; x = b' * a' by A1,GROUP_2:52; then x in b' * N & b' * N c= N * b' by A3,GROUP_2:125,GROUP_3:141; then consider b1 such that A4: x = b1 * b' and A5: b1 in N by GROUP_2:126; reconsider x' = x as Element of B by A1; reconsider x'' = x as Element of G by A4; b1 = x'' * b'" & b'" = b" by A4,GROUP_1:22,GROUP_2:57; then A6:b1 = x' * b" by GROUP_2:52; then A7: b1 in B by RLVECT_1:def 1; reconsider b1' = b1 as Element of B by A6; b1' * b = x & b1' in A by A4,A5,A7,GROUP_2:52,99; hence thesis by GROUP_2:126; end; end; hence thesis by GROUP_3:141; end; hence thesis; end; definition let G,B; let N be normal Subgroup of G; redefine func B /\ N -> strict normal Subgroup of B; coherence by Th10; end; definition let G; let N be normal Subgroup of G; let B; redefine func N /\ B -> strict normal Subgroup of B; coherence by Th10; end; definition let G be non empty 1-sorted; redefine attr G is trivial means :Def2: ex x st the carrier of G = {x}; compatibility proof hereby assume A1: G is trivial; consider y being Element of G; for x holds x in the carrier of G iff x = y by A1,REALSET1:def 20; then the carrier of G = {y} by TARSKI:def 1; hence ex x st the carrier of G = {x}; end; given x such that A2: the carrier of G = {x}; now let a,b be Element of G; thus a = x by A2,TARSKI:def 1 .= b by A2,TARSKI:def 1; end; hence thesis by REALSET1:def 20; end; end; definition cluster trivial Group; existence proof consider G; take (1).G; the carrier of (1).G = {1.G} by GROUP_2:def 7; hence thesis by Def2; end; end; theorem Th11: (1).G is trivial proof the carrier of (1).G = {1.G} by GROUP_2:def 7; hence thesis by Def2; end; theorem Th12: G is trivial iff ord G = 1 & G is finite proof thus G is trivial implies ord G = 1 & G is finite proof given x such that A1: the carrier of G = {x}; G is finite by A1,GROUP_1:def 13; then ex B being finite set st B = the carrier of G & ord G = card B by GROUP_1:def 14; hence thesis by A1,CARD_1:79,GROUP_1:def 13; end; assume A2: ord G = 1 & G is finite; then consider c being finite set such that A3: c = the carrier of G & ord G = card c by GROUP_1:def 14; thus ex x st the carrier of G = {x} by A2,A3,CARD_2:60; end; theorem Th13: for G being strict Group holds G is trivial implies (1).G = G proof let G be strict Group; assume G is trivial; then A1: ord G = 1 & G is finite by Th12; then ord G = ord (1).G by GROUP_2:81; hence G = (1).G by A1,GROUP_2:85; end; definition let G,N; func Cosets N -> set equals :Def3: Left_Cosets N; coherence; end; definition let G,N; cluster Cosets N -> non empty; coherence proof Cosets N = Left_Cosets N by Def3; hence thesis by GROUP_2:165; end; end; theorem Th14: for N being normal Subgroup of G holds Cosets N = Left_Cosets N & Cosets N = Right_Cosets N proof let N be normal Subgroup of G; thus Cosets N = Left_Cosets N by Def3; hence thesis by GROUP_3:150; end; theorem Th15: for N being normal Subgroup of G holds x in Cosets N implies ex a st x = a * N & x = N * a proof let N be normal Subgroup of G; assume x in Cosets N; then x in Left_Cosets N by Def3; then consider a such that A1: x = a * N by GROUP_2:def 15; x = N * a by A1,GROUP_3:140; hence thesis by A1; end; theorem Th16: for N being normal Subgroup of G holds a * N in Cosets N & N * a in Cosets N proof let N be normal Subgroup of G; A1: a * N in Left_Cosets N by GROUP_2:def 15; N * a in Right_Cosets N by GROUP_2:def 16; hence thesis by A1,Th14; end; theorem Th17: for N being normal Subgroup of G holds x in Cosets N implies x is Subset of G proof let N be normal Subgroup of G; assume x in Cosets N; then ex a st x = a * N & x = N * a by Th15; hence thesis; end; theorem Th18: for N being normal Subgroup of G holds A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N proof let N be normal Subgroup of G; assume A1: A1 in Cosets N & A2 in Cosets N; then consider a such that A2: A1 = a * N & A1 = N * a by Th15; consider b such that A3: A2 = b * N & A2 = N * b by A1,Th15; A1 * A2 = a * (N * (b * N)) by A2,A3,GROUP_3:11 .= a * (b * N * N) by A3,GROUP_3:15 .= a * (b * (N * N)) by GROUP_4:60 .= a * (b * carr N) by GROUP_4:58 .= a * (b * N) by GROUP_2:def 13 .= a * b * N by GROUP_2:127; then A1 * A2 in Left_Cosets N by GROUP_2:def 15; hence thesis by Th14; end; definition let G; let N be normal Subgroup of G; func CosOp N -> BinOp of Cosets N means :Def4: for W1,W2 being Element of Cosets N for A1,A2 st W1 = A1 & W2 = A2 holds it.(W1,W2) = A1 * A2; existence proof defpred P[Element of Cosets N,Element of Cosets N,set] means for A1,A2 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 P[W1,W2,V] proof let W1,W2 be Element of Cosets N; reconsider A1 = W1, A2 = W2 as Subset of G by Th17; reconsider C = A1 * A2 as Element of Cosets N by Th18; take C; thus thesis; end; thus ex B being BinOp of Cosets N st for W1,W2 being Element of Cosets N holds P[W1,W2,B.(W1,W2)] from BinOpEx(A1); end; uniqueness proof let o1,o2 be BinOp of Cosets N; assume A2: for W1,W2 being Element of Cosets N for A1,A2 st W1 = A1 & W2 = A2 holds o1.(W1,W2) = A1 * A2; assume A3: for W1,W2 being Element of Cosets N for A1,A2 st W1 = A1 & W2 = A2 holds o2.(W1,W2) = A1 * A2; now let x,y be set; assume A4: x in Cosets N & y in Cosets N; then reconsider W = x, V = y as Element of Cosets N; reconsider A1 = x, A2 = y as Subset of G by A4,Th17; o1.(W,V) = A1 * A2 & o2.(W,V) = A1 * A2 by A2,A3; then o1.(x,y) = o2.(x,y) & o1. [x,y] = o1.(x,y) & o2. [x,y] = o2.(x,y) by BINOP_1:def 1; hence o1. [x,y] = o2. [x,y]; end; hence thesis by FUNCT_2:118; end; end; definition let G; let N be normal Subgroup of G; func G./.N -> HGrStr equals :Def5: HGrStr (# Cosets N, CosOp N #); correctness; end; definition let G; let N be normal Subgroup of G; cluster G./.N -> strict non empty; coherence proof G./.N = HGrStr (# Cosets N, CosOp N #) by Def5; hence G./.N is strict & the carrier of G./.N is non empty; end; end; canceled 3; theorem Th22: for N being normal Subgroup of G holds the carrier of G./.N = Cosets N proof let N be normal Subgroup of G; G./.N = HGrStr (# Cosets N, CosOp N #) by Def5; hence thesis; end; theorem Th23: for N being normal Subgroup of G holds the mult of G./.N = CosOp N proof let N be normal Subgroup of G; G./.N = HGrStr (# Cosets N, CosOp N #) by Def5; hence thesis; end; reserve N for normal Subgroup of G; reserve S,T1,T2 for Element of G./.N; definition let G,N,S; func @S -> Subset of G equals :Def6: S; coherence proof S is Element of Cosets N by Th22; hence thesis by Th17; end; end; theorem Th24: for N being normal Subgroup of G, T1,T2 being Element of G./.N holds @T1 * @T2 = T1 * T2 proof let N be normal Subgroup of G, T1,T2 be Element of G./.N; reconsider S1 = T1 as Element of Cosets N by Th22; reconsider S2 = T2 as Element of Cosets N by Th22; S1 = @T1 & S2 = @T2 by Def6; hence @T1 * @T2 = (CosOp N).(T1,T2) by Def4 .= (the mult of G./.N).(T1,T2) by Th23 .= T1 * T2 by VECTSP_1:def 10; end; theorem Th25: @(T1 * T2) = @T1 * @T2 proof thus @(T1 * T2) = T1 * T2 by Def6 .= @T1 * @T2 by Th24; end; definition let G; let N be normal Subgroup of G; cluster G./.N -> associative Group-like; coherence proof A1: the carrier of G./.N = Cosets N by Th22; G./.N is associative Group-like proof thus for f,g,h being Element of G./.N holds f * (g * h) = f * g * h proof let f,g,h be Element of G./.N; consider a such that A2: f = a * N & f = N * a by A1,Th15; consider c being Element of G such that A3: h = c * N & h = N * c by A1,Th15; A4: @f = f & @g = g & @h = h by Def6; thus f * (g * h) = @f * @(g * h) by Th24 .= (a * N) * (@g * @h) by A2,A4,Th25 .= @f * @g * (c * N) by A2,A3,A4,GROUP_2:14 .= @(f * g) * @h by A3,A4,Th25 .= f * g * h by Th24; end; A5: carr N in Left_Cosets N & Cosets N = Left_Cosets N by Th14,GROUP_2:165; then reconsider e = carr N as Element of G./.N by Th22; take e; let h be Element of G./.N; consider a such that A6: h = a * N & h = N * a by A1,Th15; A7: @h = h & @e = e by Def6; thus h * e = @h * @e by Th24 .= (a * N) * N by A6,A7,GROUP_2:def 11 .= a * (N * N) by GROUP_4:60 .= a * carr N by GROUP_4:58 .= h by A6,GROUP_2:def 13; thus e * h = @e * @h by Th24 .= N * (N * a) by A6,A7,GROUP_2:def 12 .= N * N * a by GROUP_4:61 .= carr N * a by GROUP_4:58 .= h by A6,GROUP_2:def 14; reconsider g = a" * N as Element of G./.N by A1,A5,GROUP_2: def 15; A8: @g = g by Def6; take g; thus h * g = N * a * (a" * N) by A6,A7,A8,Th24 .= N * a * a" * N by GROUP_3:10 .= N * (a * a") * N by GROUP_2:129 .= N * 1.G * N by GROUP_1:def 5 .= carr N * N by GROUP_2:132 .= carr N * carr N by GROUP_2:def 11 .= e by GROUP_2:91; thus g * h = @g * @h by Th24 .= a" * N * a * N by A6,A7,A8,GROUP_3:10 .= a" * (N * a) * N by GROUP_2:128 .= a" * (a * N) * N by GROUP_3:140 .= a" * a * N * N by GROUP_2:127 .= 1.G * N * N by GROUP_1:def 5 .= 1.G * (N * N) by GROUP_4:60 .= 1.G * carr N by GROUP_4:58 .= e by GROUP_2:43; end; hence thesis; end; end; theorem Th26: for N being normal Subgroup of G, S being Element of G./.N ex a st S = a * N & S = N * a proof let N be normal Subgroup of G, S be Element of G./.N; S in the carrier of G./.N & the carrier of G./.N = Cosets N by Th22; hence thesis by Th15; end; theorem Th27: N * a is Element of G./.N & a * N is Element of G./.N & carr N is Element of G./.N proof N * a in Cosets N & a * N in Cosets N & Cosets N = the carrier of G./.N & carr N in Left_Cosets N & Cosets N = Left_Cosets N by Th14,Th16,Th22,GROUP_2:165; hence thesis; end; theorem Th28: for N being normal Subgroup of G holds x in G./.N iff ex a st x = a * N & x = N * a proof let N be normal Subgroup of G; thus x in G./.N implies ex a st x = a * N & x = N * a proof assume x in G./.N; then x is Element of G./.N by RLVECT_1:def 1; hence thesis by Th26; end; given a such that A1: x = a * N & x = N * a; x is Element of G./.N by A1,Th27; hence thesis by RLVECT_1:def 1; end; theorem Th29: for N being normal Subgroup of G holds 1.(G./.N) = carr N proof let N be normal Subgroup of G; reconsider e = carr N as Element of G./.N by Th27; A1: the carrier of G./.N = Cosets N by Th22; now let h be Element of G./.N; consider a such that A2: h = a * N & h = N * a by A1,Th15; A3: @h = h & @e = e by Def6; thus h * e = @h * @e by Th24 .= (a * N) * N by A2,A3,GROUP_2:def 11 .= a * (N * N) by GROUP_4:60 .= a * carr N by GROUP_4:58 .= h by A2,GROUP_2:def 13; thus e * h = @e * @h by Th24 .= N * (N * a) by A2,A3,GROUP_2:def 12 .= N * N * a by GROUP_4:61 .= carr N * a by GROUP_4:58 .= h by A2,GROUP_2:def 14; end; hence thesis by GROUP_1:10; end; theorem Th30: for N being normal Subgroup of G, S being Element of G./.N holds S = a * N implies S" = a" * N proof let N be normal Subgroup of G, S be Element of G./.N; assume A1: S = a * N; reconsider g = a" * N as Element of G./.N by Th27; A2: @g = g by Def6; A3: @S = S by Def6; A4: S * g = @S * @g by Th24 .= N * a * (a" * N) by A1,A2,A3,GROUP_3:140 .= N * a * a" * N by GROUP_3:10 .= N * (a * a") * N by GROUP_2:129 .= N * 1.G * N by GROUP_1:def 5 .= carr N * N by GROUP_2:132 .= carr N * carr N by GROUP_2:def 11 .= carr N by GROUP_2:91; A5: g * S = @g * @S by Th24 .= a" * N * a * N by A1,A2,A3,GROUP_3:10 .= a" * (N * a) * N by GROUP_2:128 .= a" * (a * N) * N by GROUP_3:140 .= a" * a * N * N by GROUP_2:127 .= 1.G * N * N by GROUP_1:def 5 .= 1.G * (N * N) by GROUP_4:60 .= 1.G * carr N by GROUP_4:58 .= carr N by GROUP_2:43; 1.(G./.N) = carr N by Th29; hence thesis by A4,A5,GROUP_1:def 5; end; theorem Th31: for N being normal Subgroup of G holds Left_Cosets N is finite implies G./.N is finite proof let N be normal Subgroup of G; assume Left_Cosets N is finite; then Cosets N is finite by Th14; then the carrier of G./.N is finite by Th22; hence thesis by GROUP_1:def 13; end; theorem for N being normal Subgroup of G holds Ord(G./.N) = Index N proof let N be normal Subgroup of G; thus Ord(G./.N) = Card(the carrier of G./.N) by GROUP_1:def 12 .= Card Cosets N by Th22 .= Card Left_Cosets N by Th14 .= Index N by GROUP_2:175; end; theorem for N being normal Subgroup of G holds Left_Cosets N is finite implies ord(G./.N) = index N proof let N be normal Subgroup of G; assume A1: Left_Cosets N is finite; then reconsider LC = Left_Cosets N as finite set; A2: Cosets N = LC by Th14; A3: G./.N is finite by A1,Th31; then reconsider GN = the carrier of G./.N as finite set by GROUP_1:def 13; thus ord(G./.N) = card GN by A3,GROUP_1:def 14 .= card LC by A2,Th22 .= index N by GROUP_2:def 18; end; theorem Th34: for M being strict normal Subgroup of G holds M is Subgroup of B implies B./.(B,M)`*` is Subgroup of G./.M proof let M be strict normal Subgroup of G; assume A1: M is Subgroup of B; set I = B./.(B,M)`*`; set J = (B,M)`*`; A2: the carrier of I c= the carrier of G./.M proof let x; assume A3: x in the carrier of I; the carrier of I = Cosets((B,M)`*`) by Th22; then consider a being Element of B such that A4: x = a * J & x = J * a by A3,Th15; reconsider b = a as Element of G by GROUP_2:51; J = M by A1,Def1; then a * J = b * M & J * a = M * b by Th2; then x in Cosets M & the carrier of G./.M = Cosets M by A4,Th16,Th22 ; hence thesis; end; set g = the mult of I; set f = the mult of G./.M; set X = [: the carrier of I,the carrier of I :]; A5: dom g = X & dom f = [: the carrier of G./.M,the carrier of G./.M :] & X c= [: the carrier of G./.M,the carrier of G./.M :] by A2,FUNCT_2:def 1,ZFMISC_1:119; then A6: dom g = dom f /\ X by XBOOLE_1:28; now let x; assume A7: x in dom g; then consider y,z such that A8: [y,z] = x by A5,ZFMISC_1:102; A9: y in the carrier of I & z in the carrier of I by A5,A7,A8,ZFMISC_1:106; A10: the carrier of I = Cosets((B,M)`*`) by Th22; then consider a being Element of B such that A11: y = a * J & y = J * a by A9,Th15; consider b being Element of B such that A12: z = b * J & z = J * b by A9,A10,Th15; reconsider W1 = y, W2 = z as Element of Cosets J by A11,A12,Th16; A13: the mult of I = CosOp J & the mult of G./.M = CosOp M by Th23; A14: g.x = g.(W1,W2) by A8,BINOP_1:def 1 .= (a * J) * (J * b) by A11,A12,A13,Def4 .= a * J * J * b by GROUP_3:12 .= a * (J * J) * b by GROUP_4:60 .= a * carr J * b by GROUP_4:58 .= a * J * b by GROUP_2:def 13 .= a * (J * b) by GROUP_2:128 .= a * (b * J) by GROUP_3:140 .= a * b * J by GROUP_2:127; reconsider a' = a, b' = b as Element of G by GROUP_2:51; A15: J = M by A1,Def1; then A16: y = a' * M & y = M * a' & z = b' * M & z = M * b' by A11, A12,Th2; then reconsider V1 = y, V2 = z as Element of Cosets M by Th16; A17: f.x = f.(V1,V2) by A8,BINOP_1:def 1 .= (a' * M) * (M * b') by A13,A16,Def4 .= a' * M * M * b' by GROUP_3:12 .= a' * (M * M) * b' by GROUP_4:60 .= a' * carr M * b' by GROUP_4:58 .= a' * M * b' by GROUP_2:def 13 .= a' * (M * b') by GROUP_2:128 .= a' * (b' * M) by GROUP_3:140 .= a' * b' * M by GROUP_2:127; a' * b' = a * b by GROUP_2:52; hence g.x = f.x by A14,A15,A17,Th2; end; then g = f | X by A6,FUNCT_1:68; hence thesis by A2,GROUP_2:def 5; end; theorem for N,M being strict normal Subgroup of G holds M is Subgroup of N implies N./.(N,M)`*` is normal Subgroup of G./.M proof let N,M be strict normal Subgroup of G; assume A1: M is Subgroup of N; then A2: (N,M)`*` = M by Def1; reconsider J = N./.(N,M)`*` as Subgroup of G./.M by A1,Th34; reconsider I = M as normal Subgroup of N by A2; now let S be Element of G./.M; thus S * J c= J * S proof let x; assume x in S * J; then consider T being Element of G./.M such that A3: x = S * T and A4: T in J by GROUP_2:125; consider a such that A5: S = a * M & S = M * a by Th26; consider c being Element of N such that A6: T = c * I & T = I * c by A2,A4,Th28; reconsider d = c as Element of G by GROUP_2:51; set e = a * (d * a"); A7: c in N by RLVECT_1:def 1; e = d |^ a" by Th4; then e in N by A7,GROUP_5:3; then reconsider f = e as Element of N by RLVECT_1:def 1; reconsider V = I * f as Element of J by A2,Th27; A8: V in J by RLVECT_1:def 1; reconsider V as Element of G./.M by GROUP_2:51; A9: @S = S & @T = T & c * I = d * M & M * d = I * c & M * e = I * f & @V = V by Def6,Th2; then x = M * a * (M * d) by A3,A5,A6,Th24 .= M * a * (M * d * 1.G) by GROUP_2:43 .= M * a * (M * d * (a" * a)) by GROUP_1:def 5 .= M * a * (M * (d * (a" * a))) by GROUP_2:129 .= M * a * M * (d * (a" * a)) by GROUP_3:12 .= M * (a * M) * (d * (a" * a)) by GROUP_3:15 .= M * (M * a) * (d * (a" * a)) by GROUP_3:140 .= M * ((M * a) * (d * (a" * a))) by GROUP_3:14 .= M * (M * (a * (d * (a" * a)))) by GROUP_2:129 .= M * (M * (a * (d * a" * a))) by VECTSP_1:def 16 .= M * (M * (a * (d * a") * a)) by VECTSP_1:def 16 .= M * (M * e * a) by GROUP_2:129 .= M * (e * M * a) by GROUP_3:140 .= M * (e * (M * a)) by GROUP_2:128 .= M * e * (M * a) by GROUP_3:13 .= V * S by A5,A9,Th24; hence x in J * S by A8,GROUP_2:126; end; end; hence thesis by GROUP_3:141; end; theorem for G being strict Group, N be strict normal Subgroup of G holds G./.N is commutative Group iff G` is Subgroup of N proof let G be strict Group, N be strict normal Subgroup of G; thus G./.N is commutative Group implies G` is Subgroup of N proof assume A1: G./.N is commutative Group; now let a,b be Element of G; reconsider S = a * N,T = b * N as Element of G./.N by Th27; S" = @(S") & T" = @(T") & S" = a" * N & T" = b" * N by Def6,Th30; then A2: S" * T" = (a" * N) * (b" * N) by Th24; S = @S & T = @T by Def6; then A3: S * T = (a * N) * (b * N) by Th24; A4: @(S" * T") = (S" * T") & @(S * T) = (S * T) by Def6; [.S,T.] = (S" * T") * (S * T) by GROUP_5:19; then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) & [.S,T.] = 1.(G./.N) & 1.(G./.N) = carr N by A1,A2,A3,A4,Th24,Th29 ,GROUP_5:40; then carr N = (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:11 .= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:15 .= (a" * N) * (b" * N) * (a * (b * N * N)) by GROUP_3:140 .= (a" * N) * (b" * N) * (a * (b * N)) by Th6 .= (a" * N) * (b" * N) * (a * b * N) by GROUP_2:127 .= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:11 .= a" * (N * b" * N) * (a * b * N) by GROUP_3:15 .= a" * (b" * N * N) * (a * b * N) by GROUP_3:140 .= a" * (b" * N) * (a * b * N) by Th6 .= (a" * b" * N) * (a * b * N) by GROUP_2:127 .= (a" * b") * (N * (a * b * N)) by GROUP_3:11 .= (a" * b") * (N * (a * b) * N) by GROUP_3:15 .= (a" * b") * ((a * b) * N * N) by GROUP_3:140 .= (a" * b") * ((a * b) * N) by Th6 .= (a" * b") * (a * b) * N by GROUP_2:127 .= [.a,b.] * N by GROUP_5:19; hence [.a,b.] in N by GROUP_2:136; end; hence thesis by Th8; end; assume A5: G` is Subgroup of N; now let S,T be Element of G./.N; consider a being Element of G such that A6: S = a * N & S = N * a by Th26; consider b being Element of G such that A7: T = b * N & T = N * b by Th26; [.a,b.] in N by A5,Th8; then A8: carr N = [.a,b.] * N by GROUP_2:136 .= (a" * b") * (a * b) * N by GROUP_5:19 .= (a" * b") * ((a * b) * N) by GROUP_2:127 .= (a" * b") * ((a * b) * N * N) by Th6 .= (a" * b") * (N * (a * b) * N) by GROUP_3:140 .= (a" * b") * (N * (a * b * N)) by GROUP_3:15 .= (a" * b" * N) * (a * b * N) by GROUP_3:11 .= a" * (b" * N) * (a * b * N) by GROUP_2:127 .= a" * (b" * N * N) * (a * b * N) by Th6 .= a" * (N * b" * N) * (a * b * N) by GROUP_3:140 .= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:15 .= (a" * N) * (b" * N) * (a * b * N) by GROUP_3:11 .= (a" * N) * (b" * N) * (a * (b * N)) by GROUP_2:127 .= (a" * N) * (b" * N) * (a * (b * N * N)) by Th6 .= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:140 .= (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:15 .= (a" * N) * (b" * N) * (a * N * (b * N)) by GROUP_3:11; S" = @(S") & T" = @(T") & S" = a" * N & T" = b" * N by A6,A7,Def6, Th30 ; then A9: S" * T" = (a" * N) * (b" * N) by Th24; S = @S & T = @T by Def6; then A10: S * T = (a * N) * (b * N) by A6,A7,Th24; A11: @(S" * T") = (S" * T") & @(S * T) = (S * T) by Def6; [.S,T.] = (S" * T") * (S * T) by GROUP_5:19; then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) & 1.(G./.N) = carr N by A9,A10,A11,Th24,Th29; hence [.S,T.] = 1.(G./.N) by A8; end; hence thesis by GROUP_5:40; end; Lm1: (for a holds f.a = 1.H) implies f.(a * b) = f.a * f.b proof assume A1: for a holds f.a = 1.H; 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; end; definition let G,H; mode Homomorphism of G,H -> Function of the carrier of G, the carrier of H means :Def7: it.(a * b) = it.a * it.b; existence proof deffunc F(Element of G) = 1.H; consider f such that A1: for a holds f.a = F(a) from LambdaD; take f; thus thesis by A1,Lm1; end; end; reserve g,h for Homomorphism of G,H; reserve g1 for Homomorphism of H,G; reserve h1 for Homomorphism of H,I; canceled 3; theorem Th40: g.(1.G) = 1.H proof g.(1.G) = g.(1.G * 1.G) by GROUP_1:def 4 .= g.(1.G) * g.(1.G) by Def7; hence thesis by GROUP_1:15; end; theorem Th41: g.(a") = (g.a)" proof g.(a") * g.a = g.(a" * a) by Def7 .= g.(1.G) by GROUP_1:def 5 .= 1.H by Th40; hence thesis by GROUP_1:20; end; theorem Th42: g.(a |^ b) = (g.a) |^ (g.b) proof thus g.(a |^ b) = g.(b" * a * b) by GROUP_3:def 2 .= g.(b" * a) * g.b by Def7 .= g.(b") * g.a * g.b by Def7 .= (g.b)" * g.a * g.b by Th41 .= (g.a) |^ (g.b) by GROUP_3:def 2; end; theorem Th43: g. [.a,b.] = [.g.a,g.b.] proof thus g. [.a,b.] = g.(a" * b" * a * b) by GROUP_5:19 .= g.(a" * b" * a) * g.b by Def7 .= g.(a" * b") * g.a * g.b by Def7 .= g.(a") * g.(b") * g.a * g.b by Def7 .= (g.a)" * g.(b") * g.a * g.b by Th41 .= (g.a)" * (g.b)" * g.a * g.b by Th41 .= [.g.a,g.b.] by GROUP_5:19; end; theorem g. [.a1,a2,a3.] = [.g.a1,g.a2,g.a3.] proof thus g. [.a1,a2,a3.] = g. [.[.a1,a2.],a3.] by GROUP_5:def 3 .= [.g. [.a1,a2.],g.a3.] by Th43 .= [.[.g.a1,g.a2.],g.a3.] by Th43 .= [.g.a1,g.a2,g.a3.] by GROUP_5:def 3; end; theorem Th45: g.(a |^ n) = (g.a) |^ n proof defpred Q[Nat] means g.(a |^ $1) = (g.a) |^ $1; A1: Q[0] proof thus g.(a |^ 0) = g.(1.G) by GROUP_1:43 .= 1.H by Th40 .= (g.a) |^ 0 by GROUP_1:43; end; A2: for n st Q[n] holds Q[n + 1] proof let n; assume A3: Q[n]; thus g.(a |^ (n + 1)) = g.(a |^ n * a) by GROUP_1:49 .= (g.a) |^ n * g.a by A3,Def7 .= (g.a) |^ (n + 1) by GROUP_1:49; end; for n holds Q[n] from Ind(A1,A2); hence thesis; end; theorem g.(a |^ i) = (g.a) |^ i proof now per cases; suppose A1: i >= 0; hence g.(a |^ i) = g.(a |^ abs( i )) by GROUP_1:55 .= (g.a) |^ abs( i ) by Th45 .= (g.a) |^ i by A1,GROUP_1:55; suppose A2: i < 0; hence g.(a |^ i) = g.(a |^ abs( i ))" by GROUP_1:56 .= (g.(a |^ abs( i )))" by Th41 .= ((g.a) |^ abs( i ))" by Th45 .= (g.a) |^ i by A2,GROUP_1:56; end; hence thesis; end; theorem Th47: id the carrier of G is Homomorphism of G,G proof reconsider f = id the carrier of G as Function of the carrier of G, the carrier of G; now let a,b; thus f.(a * b) = a * b by FUNCT_1:35 .= f.a * b by FUNCT_1:35 .= f.a * f.b by FUNCT_1:35; end; hence thesis by Def7; end; theorem Th48: h1 * h is Homomorphism of G,I proof reconsider f = h1 * h as Function of the carrier of G, the carrier of I; now let a,b; thus f.(a * b) = h1.(h.(a * b)) by FUNCT_2:21 .= h1.(h.a * h.b) by Def7 .= (h1.(h.a)) * (h1.(h.b)) by Def7 .= f.a * (h1.(h.b)) by FUNCT_2:21 .= f.a * f.b by FUNCT_2:21; end; hence thesis by Def7; end; definition let G,H,I,h,h1; redefine func h1 * h -> Homomorphism of G,I; coherence by Th48; end; definition let G,H,g; redefine func rng g -> Subset of H; coherence by RELSET_1:12; end; definition let G,H; func 1:(G,H) -> Homomorphism of G,H means :Def8: for a holds it.a = 1.H; existence proof deffunc F(Element of G) = 1.H; consider f such that A1: for a holds f.a = F(a) from LambdaD; f.(a * b) = f.a * f.b by A1,Lm1; then reconsider g = f as Homomorphism of G,H by Def7; take g; thus thesis by A1; end; uniqueness proof let g,h be Homomorphism of G,H such that A2: for a holds g.a = 1.H and A3: for a holds h.a = 1.H; for a holds g.a = h.a proof let a; g.a = 1.H & h.a = 1.H by A2,A3; hence thesis; end; hence thesis by FUNCT_2:113; end; end; theorem h1 * 1:(G,H) = 1:(G,I) & 1:(H,I) * h = 1:(G,I) proof A1: now let a; thus (h1 * 1:(G,H)).a = h1.(1:(G,H).a) by FUNCT_2:21 .= h1.(1.H) by Def8 .= 1.I by Th40; end; now let a; thus (1:(H,I) * h).a = 1:(H,I).(h.a) by FUNCT_2:21 .= 1.I by Def8; end; hence thesis by A1,Def8; end; definition let G; let N be normal Subgroup of G; func nat_hom N -> Homomorphism of G,G./.N means :Def9: for a holds it.a = a * N; existence proof defpred P[set,set] means ex a st $1 = a & $2 = a * N; A1: for x,y1,y2 st x in the carrier of G & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x st x in the carrier of G ex y st P[x,y] proof let x; assume x in the carrier of G; then reconsider a = x as Element of G; reconsider y = a * N as set; take y; take a; thus thesis; end; consider f being Function such that A3: dom f = the carrier of G and A4: for x st x in the carrier of G holds P[x,f.x] from FuncEx(A1,A2); rng f c= the carrier of G./.N proof let x; assume x in rng f; then consider y such that A5: y in dom f and A6: f.y = x by FUNCT_1:def 5; consider a such that A7: y = a & f.y = a * N by A3,A4,A5; a * N = N * a by GROUP_3:140; then x in G./.N by A6,A7,Th28; hence thesis by RLVECT_1:def 1; end; then reconsider f as Function of the carrier of G, the carrier of G./.N by A3,FUNCT_2:def 1,RELSET_1:11 ; now let a,b; consider a1 such that A8: a = a1 & f.a = a1 * N by A4; consider b1 such that A9: b = b1 & f.b = b1 * N by A4; A10: ex c being Element of G st c = a * b & f.(a * b) = c * N by A4; A11: @(f.a) = f.a & @(f.b) = f.b by Def6; thus f.a * f.b = @(f.a) * @(f.b) by Th24 .= (a1 * N) * b1 * N by A8,A9,A11,GROUP_3:10 .= a1 * (N * b1) * N by GROUP_2:128 .= a1 * (b1 * N) * N by GROUP_3:140 .= a1 * ((b1 * N) * N) by GROUP_3:9 .= a1 * (b1 * N) by Th6 .= f.(a * b) by A8,A9,A10,GROUP_2:127; end; then reconsider f as Homomorphism of G,G./.N by Def7; take f; let a; ex b st a = b & f.a = b * N by A4; hence thesis; end; uniqueness proof let n1,n2 be Homomorphism of G,G./.N such that A12: for a holds n1.a = a * N and A13: for a holds n2.a = a * N; now let a; n1.a = a * N & n2.a = a * N by A12,A13; hence n1.a = n2.a; end; hence thesis by FUNCT_2:113; end; end; definition let G,H,g; func Ker g -> strict Subgroup of G means :Def10: the carrier of it = {a : g.a = 1.H}; existence proof defpred P[set] means g.$1 = 1.H; reconsider A = {a : P[a]} as Subset of G from SubsetD; g.(1.G) = 1.H by Th40; then A1: 1.G in A; A2: now let a,b; assume that A3: a in A and A4: b in A; A5: ex a1 st a1 = a & g.a1 = 1.H by A3; A6: ex b1 st b1 = b & g.b1 = 1.H by A4; g.(a * b) = g.a * g.b by Def7 .= 1.H by A5,A6,GROUP_1:def 4; hence a * b in A; end; now let a; assume a in A; then ex a1 st a1 = a & g.a1 = 1.H; then g.(a") = (1.H)" by Th41 .= 1.H by GROUP_1:16; hence a" in A; end; then consider B being strict Subgroup of G such that A7: the carrier of B = A by A1,A2,GROUP_2:61; reconsider B as strict Subgroup of G; take B; thus thesis by A7; end; uniqueness by GROUP_2:68; end; definition let G,H,g; cluster Ker g -> normal; coherence proof defpred P[set] means g.$1 = 1.H; reconsider A = {a : P[a]} as Subset of G from SubsetD; g.(1.G) = 1.H by Th40; then A1: 1.G in A; A2: now let a,b; assume that A3: a in A and A4: b in A; A5: ex a1 st a1 = a & g.a1 = 1.H by A3; A6: ex b1 st b1 = b & g.b1 = 1.H by A4; g.(a * b) = g.a * g.b by Def7 .= 1.H by A5,A6,GROUP_1:def 4; hence a * b in A; end; now let a; assume a in A; then ex a1 st a1 = a & g.a1 = 1.H; then g.(a") = (1.H)" by Th41 .= 1.H by GROUP_1:16; hence a" in A; end; then consider B being strict Subgroup of G such that A7: the carrier of B = A by A1,A2,GROUP_2:61; now let a; now let b; assume b in B |^ a; then consider c being Element of G such that A8: b = c |^ a and A9: c in B by GROUP_3:70; c in A by A7,A9,RLVECT_1:def 1; then ex a1 st c = a1 & g.a1 = 1.H; then g.b = (1.H) |^ (g.a) by A8,Th42 .= 1.H by GROUP_3:22; then b in A; hence b in B by A7,RLVECT_1:def 1; end; hence B |^ a is Subgroup of B by GROUP_2:67; end; then B is normal Subgroup of G by GROUP_3:145; hence thesis by A7,Def10; end; end; theorem Th50: a in Ker h iff h.a = 1.H proof thus a in Ker h implies h.a = 1.H proof assume a in Ker h; then a in the carrier of Ker h by RLVECT_1:def 1; then a in {b : h.b = 1.H} by Def10; then ex b st a = b & h.b = 1.H; hence thesis; end; assume h.a = 1.H; then a in {b : h.b = 1.H}; then a in the carrier of Ker h by Def10; hence thesis by RLVECT_1:def 1; end; theorem for G,H being strict Group holds Ker 1:(G,H) = G proof let G,H be strict Group; now let a be Element of G; 1:(G,H).a = 1.H by Def8; hence a in Ker 1:(G,H) by Th50; end; hence thesis by GROUP_2:71; end; theorem Th52: for N being strict normal Subgroup of G holds Ker nat_hom N = N proof let N be strict normal Subgroup of G; let a; thus a in Ker nat_hom N implies a in N proof assume a in Ker nat_hom N; then (nat_hom N).a = 1.(G./.N) & (nat_hom N).a = a * N & 1.(G./.N) = carr N by Def9,Th29,Th50; hence a in N by GROUP_2:136; end; assume a in N; then a * N = carr N & (nat_hom N).a = a * N & 1.(G./.N) = carr N by Def9,Th29,GROUP_2:136; hence thesis by Th50; end; definition let G,H,g; func Image g -> strict Subgroup of H means :Def11: the carrier of it = g .: (the carrier of G); existence 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: dom g = the carrier of G & X /\ X = X & X <> {} by FUNCT_2:def 1; then X meets X by XBOOLE_0:def 7; then A2: S <> {} by A1,RELAT_1:151; A3: now let c,d; assume that A4: c in S and A5: d in S; consider a such that a in X and A6: c = g.a by A4,FUNCT_2:116; consider b such that b in X and A7: d = g.b by A5,FUNCT_2:116; c * d = g.(a * b) & a * b in the carrier of G by A6,A7,Def7; hence c * d in S by FUNCT_2:43; end; now let c; assume c in S; then consider a such that a in X and A8: c = g.a by FUNCT_2:116; a" in the carrier of G & g.(a") = c" by A8,Th41; hence c" in S by FUNCT_2:43; end; then consider D being strict Subgroup of H such that A9: the carrier of D = S by A2,A3,GROUP_2:61; take D; thus thesis by A9; end; uniqueness by GROUP_2:68; end; theorem Th53: rng g = the carrier of Image g proof the carrier of Image g = g .: (the carrier of G) by Def11 .= g .: (dom g) by FUNCT_2:def 1 .= rng g by RELAT_1:146; hence thesis; end; theorem Th54: x in Image g iff ex a st x = g.a proof thus x in Image g implies ex a st x = g.a proof assume x in Image g; then x in the carrier of Image g by RLVECT_1:def 1; then x in g .: (the carrier of G) by Def11; then consider y such that y in dom g and A1: y in the carrier of G and A2: g.y = x by FUNCT_1:def 12; reconsider y as Element of G by A1; take y; thus thesis by A2; end; given a such that A3: x = g.a; a in the carrier of 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 12; then x in the carrier of Image g by Def11; hence thesis by RLVECT_1:def 1; end; theorem Image g = gr rng g proof rng g = the carrier of Image g & the carrier of Image g = carr Image g by Th53,GROUP_2:def 9; hence thesis by GROUP_4:40; end; theorem Image 1:(G,H) = (1).H proof set g = 1:(G,H); 1.H in Image g by GROUP_2:55; then 1.H in the carrier of Image g by RLVECT_1:def 1; then A1: {1.H} c= the carrier of Image g by ZFMISC_1:37; the carrier of Image g c= {1.H} proof let x; assume x in the carrier of Image g; then x in g .: (the carrier of G) by Def11; then consider y such that y in dom g and A2: y in the carrier of G and A3: g.y = x by FUNCT_1:def 12; reconsider y as Element of G by A2; g.y = 1.H by Def8; hence thesis by A3,TARSKI:def 1; end; then the carrier of Image g = {1.H} by A1,XBOOLE_0:def 10; hence thesis by GROUP_2:def 7; end; theorem Th57: for N being normal Subgroup of G holds Image nat_hom N = G./.N proof let N be normal Subgroup of G; now let S be Element of G./.N; consider a such that A1: S = a * N & S = N * a by Th26; (nat_hom N).a = a * N by Def9; hence S in Image nat_hom N by A1,Th54; end; hence thesis by GROUP_2:71; end; theorem Th58: h is Homomorphism of G,Image h proof h is Function of the carrier of G, the carrier of Image h proof A1: rng h = the carrier of Image h by Th53; dom h = the carrier of G by FUNCT_2:def 1; hence thesis by A1,FUNCT_2:def 1,RELSET_1:11; end; then reconsider f' = h as Function of the carrier of G, the carrier of Image h; now let a,b; thus f'.a * f'.b = h.a * h.b by GROUP_2:52 .= f'.(a * b) by Def7; end; hence thesis by Def7; end; theorem Th59: G is finite implies Image g is finite proof assume G is finite; then the carrier of G is finite by GROUP_1:def 13; then g .: (the carrier of G) is finite by FINSET_1:17; then the carrier of Image g is finite by Def11; hence thesis by GROUP_1:def 13; end; Lm2: for A be commutative Group, a, b be Element of A holds a * b = b * a; theorem G is commutative Group implies Image g is commutative proof assume A1: G is commutative Group; let h1,h2 be Element of Image g; reconsider c = h1, d = h2 as Element of H by GROUP_2:51; h1 in Image g by RLVECT_1:def 1; then consider a such that A2: h1 = g.a by Th54; h2 in Image g by RLVECT_1:def 1; then consider b such that A3: h2 = g.b by Th54; thus h1 * h2 = c * d by GROUP_2:52 .= g.(a * b) by A2,A3,Def7 .= g.(b * a) by A1,Lm2 .= d * c by A2,A3,Def7 .= h2 * h1 by GROUP_2:52; end; theorem Th61: Ord Image g <=` Ord G proof A1: Card (g .: (the carrier of G)) <=` Card (the carrier of G) by CARD_2:3; Ord Image g = Card (the carrier of Image g) by GROUP_1:def 12 .= Card (g .: (the carrier of G)) by Def11; hence thesis by A1,GROUP_1:def 12; end; theorem G is finite implies ord Image g <= ord G proof assume A1: G is finite; then A2: Image g is finite by Th59; consider c being finite set such that A3: c = the carrier of G & ord G = card c by A1,GROUP_1:def 14; consider ci being finite set such that A4: ci = the carrier of Image g & ord Image g = card ci by A2,GROUP_1:def 14; Ord Image g <=` Ord G by Th61; then Card (the carrier of Image g) <=` Ord G by GROUP_1:def 12; then Card (the carrier of Image g) <=` Card (the carrier of G) by GROUP_1:def 12; hence thesis by A3,A4,CARD_2:57; end; definition let G,H,h; attr h is being_monomorphism means :Def12: h is one-to-one; synonym h is_monomorphism; attr h is being_epimorphism means :Def13: rng h = the carrier of H; synonym h is_epimorphism; end; theorem h is_monomorphism & c in Image h implies h.(h".c) = c proof assume that A1: h is_monomorphism and A2: c in Image h; reconsider h' = h as Function of the carrier of G,the carrier of Image h by Th58; A3: h' is one-to-one by A1,Def12; h'.(h'".c) = c proof A4: rng h' = the carrier of Image h by Th53; c in the carrier of Image h by A2,RLVECT_1:def 1; hence thesis by A3,A4,FUNCT_1:57; end; hence thesis; end; theorem Th64: h is_monomorphism implies h".(h.a) = a proof assume h is one-to-one; hence thesis by FUNCT_2:32; end; theorem Th65: h is_monomorphism implies h" is Homomorphism of Image h,G proof assume A1: h is one-to-one; then A2: h is_monomorphism by Def12; reconsider Imh = Image h as Group; h" is Function of the carrier of Imh,the carrier of G proof A3: h is Function of the carrier of G,the carrier of Imh by Th58; rng h = the carrier of Imh by Th53; hence thesis by A1,A3,FUNCT_2:31; end; then reconsider h' = h" as Function of the carrier of Imh, the carrier of G; now let a,b be Element of Imh; reconsider a' = a as Element of H by GROUP_2:51; reconsider b' = b as Element of H by GROUP_2:51; A4: a' in Imh & b' in Imh by RLVECT_1:def 1; then consider a1 being Element of G such that A5: h.a1 = a' by Th54; consider b1 being Element of G such that A6: h.b1 = b' by A4,Th54; thus h'.(a * b) = h'.(h.a1 * h.b1) by A5,A6,GROUP_2:52 .= h'.(h.(a1 * b1)) by Def7 .= a1 * b1 by A2,Th64 .= h'.a * b1 by A2,A5,Th64 .= h'.a * h'.b by A2,A6,Th64; end; hence thesis by Def7; end; theorem Th66: h is_monomorphism iff Ker h = (1).G proof thus h is_monomorphism implies Ker h = (1).G proof assume A1: h is one-to-one; now let x; thus x in the carrier of Ker h iff x = 1.G proof thus x in the carrier of Ker h implies x = 1.G proof assume A2: x in the carrier of Ker h; then x in Ker h by RLVECT_1:def 1; then x in G by GROUP_2:49; then reconsider a = x as Element of G by RLVECT_1:def 1; a in Ker h by A2,RLVECT_1:def 1; then h.a = 1.H by Th50 .= h.(1.G) by Th40; hence thesis by A1,Th1; end; assume A3: x = 1.G; then reconsider a = x as Element of G; h.a = 1.H by A3,Th40; then a in Ker h by Th50; hence thesis by RLVECT_1:def 1; end; end; then the carrier of Ker h = {1.G} by TARSKI:def 1; hence thesis by GROUP_2:def 7; end; assume Ker h = (1).G; then A4: the carrier of Ker h = {1.G} by GROUP_2:def 7; now let a,b; assume that A5: a <> b and A6: h.a = h.b; h.a * h.(a") = h.(a * a") by Def7 .= h.(1.G) by GROUP_1:def 5 .= 1.H by Th40; then 1.H = h.(b * a") by A6,Def7; then b * a" in Ker h by Th50; then A7: b * a" in the carrier of Ker h by RLVECT_1:def 1; a = 1.G * a by GROUP_1:def 4 .= b * a" * a by A4,A7,TARSKI:def 1 .= b * (a" * a) by VECTSP_1:def 16 .= b * 1.G by GROUP_1:def 5 .= b by GROUP_1:def 4; hence contradiction by A5; end; then for a,b st h.a = h.b holds a = b; then h is one-to-one by Th1; hence thesis by Def12; end; theorem Th67: for H being strict Group, h being Homomorphism of G,H holds h is_epimorphism iff Image h = H proof let H be strict Group, h be Homomorphism of G,H; thus h is_epimorphism implies Image h = H proof assume rng h = the carrier of H; then the carrier of Image h = the carrier of H by Th53; hence thesis by GROUP_2:70; end; assume A1: Image h = H; the carrier of H c= rng h proof let x; assume x in the carrier of H; then x in h .: (the carrier of G) by A1,Def11; then ex y st y in dom h & y in the carrier of G & h.y = x by FUNCT_1:def 12; hence thesis by FUNCT_1:def 5; end; then rng h = the carrier of H by XBOOLE_0:def 10; hence thesis by Def13; end; theorem Th68: for H being strict Group, h being Homomorphism of G,H holds h is_epimorphism implies for c being Element of H ex a st h.a = c proof let H be strict Group, h be Homomorphism of G,H; assume h is_epimorphism; then A1: Image h = H by Th67; now let c be Element of H; c in Image h by A1,RLVECT_1:def 1; hence ex a st h.a = c by Th54; end; hence thesis; end; theorem Th69: for N being normal Subgroup of G holds nat_hom N is_epimorphism proof let N be normal Subgroup of G; Image nat_hom N = G./.N by Th57; hence thesis by Th67; end; definition let G,H,h; attr h is being_isomorphism means :Def14: h is_epimorphism & h is_monomorphism; synonym h is_isomorphism; end; theorem Th70: h is_isomorphism iff rng h = the carrier of H & h is one-to-one proof thus h is_isomorphism implies rng h = the carrier of H & h is one-to-one proof assume h is_epimorphism & h is_monomorphism; hence thesis by Def12,Def13; end; assume rng h = the carrier of H & h is one-to-one; hence h is_epimorphism & h is_monomorphism by Def12,Def13; end; theorem h is_isomorphism implies dom h = the carrier of G & rng h = the carrier of H proof assume h is_isomorphism; then h is_epimorphism by Def14; hence thesis by Def13,FUNCT_2:def 1; end; theorem Th72: for H being strict Group, h being Homomorphism of G,H holds h is_isomorphism implies h" is Homomorphism of H,G proof let H be strict Group, h be Homomorphism of G,H; assume A1: h is_epimorphism & h is_monomorphism; then H = Image h by Th67; hence thesis by A1,Th65; end; theorem Th73: h is_isomorphism & g1 = h" implies g1 is_isomorphism proof assume that A1: h is_isomorphism and A2: g1 = h"; A3: h is one-to-one by A1,Th70; then A4: g1 is one-to-one by A2,FUNCT_1:62; A5: dom h = the carrier of G by FUNCT_2:def 1; rng g1 = dom h by A2,A3,FUNCT_1:55; hence thesis by A4,A5,Th70; end; theorem Th74: h is_isomorphism & h1 is_isomorphism implies h1 * h is_isomorphism proof assume A1: h is_isomorphism & h1 is_isomorphism; then A2: h is one-to-one & h1 is one-to-one by Th70; A3: rng(h1 * h) = the carrier of I proof A4: dom h1 = the carrier of H by FUNCT_2:def 1; rng h = the carrier of H by A1,Th70; hence rng(h1 * h) = rng h1 by A4,RELAT_1:47 .= the carrier of I by A1,Th70; end; h1 * h is one-to-one by A2,FUNCT_1:46; hence thesis by A3,Th70; end; theorem Th75: for G being Group holds nat_hom (1).G is_isomorphism proof let G be Group; set g = nat_hom (1).G; Ker g = (1).G by Th52; then g is_monomorphism & g is_epimorphism by Th66,Th69; hence nat_hom (1).G is_isomorphism by Def14; end; definition let G,H; pred G,H are_isomorphic means :Def15: ex h st h is_isomorphism; reflexivity proof let G; reconsider i = id the carrier of G as Homomorphism of G,G by Th47; i is one-to-one & rng i = the carrier of G by FUNCT_2:def 3; then i is_isomorphism by Th70; hence thesis; end; end; canceled; theorem Th77: for G,H being strict Group holds G,H are_isomorphic implies H,G are_isomorphic proof let G,H be strict Group; assume G,H are_isomorphic; then consider h being Homomorphism of G,H such that A1: h is_isomorphism by Def15; reconsider g = h" as Homomorphism of H,G by A1,Th72; take g; thus thesis by A1,Th73; end; theorem G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic proof assume that A1: G,H are_isomorphic and A2: H,I are_isomorphic; consider g such that A3: g is_isomorphism by A1,Def15; consider h1 such that A4: h1 is_isomorphism by A2,Def15; (h1 * g) is_isomorphism by A3,A4,Th74; hence thesis by Def15; end; theorem h is_monomorphism implies G,Image h are_isomorphic proof assume A1: h is one-to-one; reconsider ih = h as Homomorphism of G,Image h by Th58; take ih; A2: ih is_monomorphism by A1,Def12; now the carrier of Image h = rng ih by Th53; hence ih is_epimorphism by Def13; end; hence thesis by A2,Def14; end; theorem Th80: for G,H being strict Group holds G is trivial & H is trivial implies G,H are_isomorphic proof let G,H be strict Group; assume G is trivial & H is trivial; then A1: G = (1).G & H = (1).H by Th13; take 1:(G,H); set h = 1:(G,H); A2: h is_epimorphism proof the carrier of (1).G = {1.G} by GROUP_2:def 7; then rng h = {h.(1.G)} by A1,FUNCT_2:62 .= {1.H} by Def8 .= the carrier of (1).H by GROUP_2:def 7; hence thesis by A1,Def13; end; h is_monomorphism proof now let a,b be Element of G; assume h.a = h.b; a in the carrier of (1).G & b in the carrier of (1).G by A1; then a in {1.G} & b in {1.G} by GROUP_2:def 7; then a = 1.G & b = 1.G by TARSKI:def 1; hence a = b; end; then h is one-to-one by Th1; hence thesis by Def12; end; hence thesis by A2,Def14; end; theorem (1).G,(1).H are_isomorphic proof (1).G is trivial & (1).H is trivial by Th11; hence thesis by Th80; end; theorem for G being strict Group holds G,G./.(1).G are_isomorphic & G./.(1).G,G are_isomorphic proof let G be strict Group; nat_hom (1).G is_isomorphism by Th75; hence G,G./.(1).G are_isomorphic by Def15; hence thesis by Th77; end; theorem for G being Group holds G./.(Omega).G is trivial proof let G be Group; the carrier of G./.(Omega).G = Cosets (Omega).G by Th22 .= Left_Cosets (Omega).G by Def3 .= {the carrier of G} by GROUP_2:172; hence thesis by Def2; end; theorem Th84: for G,H being strict Group, h being Homomorphism of G,H holds G,H are_isomorphic implies Ord G = Ord H proof let G,H be strict Group, h be Homomorphism of G,H; assume A1: G,H are_isomorphic; then consider h being Homomorphism of G,H such that A2: h is_isomorphism by Def15; H,G are_isomorphic by A1,Th77; then consider g1 being Homomorphism of H,G such that A3: g1 is_isomorphism by Def15; h is_epimorphism by A2,Def14; then Image h = H by Th67; then A4: Ord H <=` Ord G by Th61; g1 is_epimorphism by A3,Def14; then Image g1 = G by Th67; then Ord G <=` Ord H by Th61; hence thesis by A4,XBOOLE_0:def 10; end; Lm3: G,H are_isomorphic & G is finite implies H is finite proof assume that A1: G,H are_isomorphic and A2: G is finite; consider h such that A3: h is_isomorphism by A1,Def15; h is_epimorphism by A3,Def14; then A4: rng h = the carrier of H by Def13; the carrier of G is finite by A2,GROUP_1:def 13; then dom h is finite by FUNCT_2:def 1; then the carrier of H is finite by A4,FINSET_1:26; hence thesis by GROUP_1:def 13; end; Lm4: for G,H being strict Group holds G,H are_isomorphic & H is finite implies G is finite proof let G,H be strict Group; assume that A1: G,H are_isomorphic and A2: H is finite; H,G are_isomorphic by A1,Th77; hence thesis by A2,Lm3; end; theorem for G,H being strict Group holds G,H are_isomorphic & (G is finite or H is finite) implies (G is finite & H is finite) by Lm3,Lm4; theorem Th86: for G,H being strict Group holds G,H are_isomorphic & (G is finite or H is finite) implies ord G = ord H proof let G,H be strict Group; assume that A1: G,H are_isomorphic and A2: G is finite or H is finite; Ord G = Ord H by A1,Th84; then A3: Card (the carrier of G) = Ord H by GROUP_1:def 12 .= Card (the carrier of H) by GROUP_1:def 12 ; A4: H is finite & G is finite by A1,A2,Lm3,Lm4; then consider cH being finite set such that A5: cH = the carrier of H & ord H = card cH by GROUP_1:def 14; consider cG being finite set such that A6: cG = the carrier of G & ord G = card cG by A4,GROUP_1:def 14; thus thesis by A3,A5,A6; end; theorem for G,H being strict Group holds G,H are_isomorphic & G is trivial implies H is trivial proof let G,H be strict Group; assume that A1: G,H are_isomorphic and A2: G is trivial; A3: ord G = 1 & G is finite by A2,Th12; then A4: ord H = 1 by A1,Th86; H is finite by A1,A3,Lm3; hence thesis by A4,Th12; end; Lm5: for G,H being strict Group holds G,H are_isomorphic & G is trivial implies H is trivial proof let G,H be strict Group; assume that A1: G,H are_isomorphic and A2: G is trivial; A3: ord G = 1 & G is finite by A2,Th12; then A4: ord H = 1 by A1,Th86; H is finite by A1,A3,Lm3; hence thesis by A4,Th12; end; Lm6: for G,H being strict Group holds G,H are_isomorphic & H is trivial implies G is trivial proof let G,H be strict Group; assume that A1: G,H are_isomorphic and A2: H is trivial; H,G are_isomorphic by A1,Th77; hence thesis by A2,Lm5; end; theorem for G,H being strict Group holds G,H are_isomorphic & (G is trivial or H is trivial) implies G is trivial & H is trivial by Lm5,Lm6; Lm7: for H being strict Group, h being Homomorphism of G,H holds G,H are_isomorphic & G is commutative Group implies H is commutative Group proof let H be strict Group, h be Homomorphism of G,H; assume that A1: G,H are_isomorphic and A2: G is commutative Group; consider h being Homomorphism of G,H such that A3: h is_isomorphism by A1,Def15; A4: h is_epimorphism by A3,Def14; now let c,d be Element of H; consider a such that A5: h.a = c by A4,Th68; consider b such that A6: h.b = d by A4,Th68; thus c * d = h.(a * b) by A5,A6,Def7 .= h.(b * a) by A2,Lm2 .= d * c by A5,A6,Def7; end; hence thesis by VECTSP_1:def 17; end; Lm8: for G,H being strict Group, h being Homomorphism of G,H holds G,H are_isomorphic & H is commutative Group implies G is commutative Group proof let G,H be strict Group, h be Homomorphism of G,H; assume that A1: G,H are_isomorphic and A2: H is commutative Group; H,G are_isomorphic by A1,Th77; hence thesis by A2,Lm7; end; theorem for G,H being strict Group, h being Homomorphism of G,H holds G,H are_isomorphic & (G is commutative Group or H is commutative Group) implies (G is commutative Group & H is commutative Group) by Lm7,Lm8; Lm9: G./.Ker g,Image g are_isomorphic & Image g, G./.Ker g are_isomorphic & ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism & g = h * nat_hom Ker g proof set I = G./.Ker g; set J = Image g; defpred P[set,set] means for a st $1 = a * Ker g holds $2 = g.a; A1: for S being Element of I ex T being Element of J st P[S,T] proof let S be Element of I; consider a such that A2: S = a * Ker g & S = Ker g * a by Th26; g.a in J by Th54; then reconsider T = g.a as Element of J by RLVECT_1:def 1; take T; let b; assume S = b * Ker g; then a" * b in Ker g by A2,GROUP_2:137; then 1.H = g.(a" * b) by Th50 .= g.(a") * g.b by Def7 .= (g.a)" * g.b by Th41; then g.b = (g.a)"" by GROUP_1:20; hence thesis by GROUP_1:19; end; consider f being Function of the carrier of I,the carrier of J such that A3: for S being Element of I holds P[S,f.S] from FuncExD(A1); now let S,T be Element of G./.Ker g; consider a such that A4: S = a * Ker g and S = Ker g * a by Th26; consider b such that A5: T = b * Ker g and A6: T = Ker g * b by Th26; f.S = g.a & f.T = g.b by A3,A4,A5; then A7: f.S * f.T = g.a * g.b by GROUP_2:52 .= g.(a * b) by Def7; @S = S & @T = T by Def6; then S * T = (a * Ker g) * (Ker g * b) by A4,A6,Th24 .= (a * Ker g) * Ker g * b by GROUP_3:12 .= a * Ker g * b by Th6 .= a * (Ker g * b) by GROUP_2:128 .= a * (b * Ker g) by GROUP_3:140 .= a * b * Ker g by GROUP_2:127; hence f.(S * T) = f.S * f.T by A3,A7; end; then reconsider f as Homomorphism of G./.Ker g,J by Def7; the carrier of J c= rng f proof let x; assume x in the carrier of J; then x in Image g by RLVECT_1:def 1; then consider a such that A8: x = g.a by Th54; reconsider S = a * Ker g as Element of I by Th27; f.S = g.a & S in the carrier of I & the carrier of I = dom f by A3,FUNCT_2:def 1; hence thesis by A8,FUNCT_1:def 5; end; then A9: rng f = the carrier of J by XBOOLE_0:def 10; A10: f is one-to-one proof let y1,y2; assume y1 in dom f & y2 in dom f; then reconsider S = y1, T = y2 as Element of I by FUNCT_2:def 1; consider a such that A11: S = a * Ker g and S = Ker g * a by Th26; consider b such that A12: T = b * Ker g and T = Ker g * b by Th26; assume A13: f.y1 = f.y2; f.S = g.a & f.T = g.b by A3,A11,A12; then (g.b)" * g.a = 1.H by A13,GROUP_1:def 5; then 1.H = g.(b") * g.a by Th41 .= g.(b" * a) by Def7; then b" * a in Ker g by Th50; hence thesis by A11,A12,GROUP_2:137; end; then f is_isomorphism by A9,Th70; hence G./.Ker g,Image g are_isomorphic by Def15; hence Image g,G./.Ker g are_isomorphic by Th77; take f; A14: dom nat_hom Ker g = the carrier of G & dom g = the carrier of G by FUNCT_2:def 1; thus f is_isomorphism by A9,A10,Th70; A15: now let x; thus x in dom g implies x in dom nat_hom Ker g & (nat_hom Ker g).x in dom f proof assume A16: x in dom g; hence x in dom nat_hom Ker g by A14; (nat_hom Ker g).x in rng nat_hom Ker g & rng nat_hom Ker g c= the carrier of I & dom f = the carrier of I by A14,A16,FUNCT_1:def 5,FUNCT_2:def 1; hence (nat_hom Ker g).x in dom f; end; assume that A17: x in dom nat_hom Ker g and (nat_hom Ker g).x in dom f ; thus x in dom g by A14,A17; end; now let x; assume x in dom g; then reconsider a = x as Element of G by FUNCT_2:def 1 ; (nat_hom Ker g).a = a * Ker g by Def9; hence g.x = f.((nat_hom Ker g).x) by A3; end; hence thesis by A15,FUNCT_1:20; end; theorem G./.Ker g,Image g are_isomorphic & Image g, G./.Ker g are_isomorphic by Lm9; theorem ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism & g = h * nat_hom Ker g by Lm9; theorem 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 M be strict normal Subgroup of G; let J be strict normal Subgroup of G./.M; assume that A1: J = N./.(N,M)`*` and A2: M is Subgroup of N; defpred P[set,set] means for a st $1 = a * M holds $2 = a * N; A3: for x being Element of G./.M ex y being Element of G./.N st P[x,y] proof let x be Element of G./.M; consider a such that A4: x = a * M and x = M * a by Th26; reconsider y = a * N as Element of G./.N by Th27; take y; let b; assume x = b * M; then a" * b in M by A4,GROUP_2:137; then a" * b in N by A2,GROUP_2:49; hence thesis by GROUP_2:137; end; consider f being Function of the carrier of G./.M, the carrier of G./.N such that A5: for x being Element of G./.M holds P[x,f.x] from FuncExD(A3); now let x,y be Element of G./.M; consider a such that A6: x = a * M and x = M * a by Th26; consider b such that A7: y = b * M and y = M * b by Th26; A8: f.x = @(f.x) & f.y = @(f.y) by Def6; A9: f.x = a * N & f.y = b * N by A5,A6,A7; A10: f.x * f.y = @(f.x) * @(f.y) by Th24 .= a * N * b * N by A8,A9,GROUP_3:10 .= a * (N * b) * N by GROUP_2:128 .= a * (b * N) * N by GROUP_3:140 .= a * ((b * N) * N) by GROUP_3:9 .= a * (b * N) by Th6 .= a * b * N by GROUP_2:127; A11: @x = x & @y = y by Def6; x * y = @x * @y by Th24 .= a * M * b * M by A6,A7,A11,GROUP_3:10 .= a * (M * b) * M by GROUP_2:128 .= a * (b * M) * M by GROUP_3:140 .= a * ((b * M) * M) by GROUP_3:9 .= a * (b * M) by Th6 .= a * b * M by GROUP_2:127; hence f.(x * y) = f.x * f.y by A5,A10; end; then reconsider f as Homomorphism of G./.M,G./.N by Def7; A12: Ker f = J proof let S be Element of G./.M; thus S in Ker f implies S in J proof assume S in Ker f; then A13: f.S = 1.(G./.N) by Th50 .= carr N by Th29; consider a such that A14: S = a * M & S = M * a by Th26; f.S = a * N by A5,A14; then a in N by A13,GROUP_2:136; then reconsider q = a as Element of N by RLVECT_1:def 1; (N,M)`*` = M by A2,Def1; then S = q * (N,M)`*` & S = (N,M)`*` * q by A14,Th2; hence thesis by A1,Th28; end; assume S in J; then consider a being Element of N such that A15: S = a * (N,M)`*` & S = (N,M)`*` * a by A1,Th28; reconsider a' = a as Element of G by GROUP_2:51; (N,M)`*` = M by A2,Def1; then S = a' * M by A15,Th2; then f.S = a' * N & a in N by A5,RLVECT_1:def 1; then f.S = carr N by GROUP_2:136 .= 1.(G./.N) by Th29; hence thesis by Th50; end; the carrier of G./.N c= rng f proof let x; assume x in the carrier of G./.N; then x in G./.N by RLVECT_1:def 1; then consider a such that A16: x = a * N & x = N * a by Th28; reconsider S = a * M as Element of G./.M by Th27; f.S = a * N & S in the carrier of G./.M & dom f = the carrier of G./.M by A5, FUNCT_2:def 1; hence thesis by A16,FUNCT_1:def 5; end; then rng f = the carrier of G./.N by XBOOLE_0:def 10; then f is_epimorphism by Def13; then Image f = G./.N by Th67; hence thesis by A12,Lm9; end; theorem for N being strict normal Subgroup of G holds (B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic proof let N be strict normal Subgroup of G; set f = nat_hom N; set g = f | (the carrier of B); set I = (B "\/" N)./.(B "\/" N,N)`*`; set J = (B "\/" N,N)`*`; A1: B is Subgroup of B "\/" N by GROUP_4:78; A2: dom g = dom f /\ (the carrier of B) & dom f = the carrier of G & the carrier of B c= the carrier of G by FUNCT_2:def 1,GROUP_2:def 5, RELAT_1:90; then A3: dom g = the carrier of B by XBOOLE_1:28; A4: N is Subgroup of B "\/" N by GROUP_4:78; then A5: N = (B "\/" N,N)`*` by Def1; A6: I is Subgroup of G./.N by A4,Th34; rng g c= the carrier of I proof let y; assume y in rng g; then consider x such that A7: x in dom g and A8: g.x = y by FUNCT_1:def 5; reconsider x as Element of B by A2,A7,XBOOLE_1:28; reconsider x'' = x as Element of B "\/" N by A1,GROUP_2:51; reconsider x' = x as Element of G by GROUP_2:51; A9: g.x = f.x' by A7,FUNCT_1:70 .= x' * N by Def9; then A10: g.x = N * x' by GROUP_3:140; x'' * (B "\/" N,N)`*` = x' * N & N * x' = (B "\/" N,N)`*` * x'' by A5,Th2; then y in I by A8,A9,A10,Th28; hence thesis by RLVECT_1:def 1; end; then reconsider g as Function of the carrier of B, the carrier of (B "\/" N)./. (B "\/" N,N)`*` by A3,FUNCT_2:def 1,RELSET_1:11; now let a,b be Element of B; reconsider a' = a, b' = b as Element of G by GROUP_2:51; A11: f.a' = g.a & f.b' = g.b by FUNCT_1:72; a * b in the carrier of B & a * b = a' * b' & a' * b' in the carrier of G by GROUP_2:52; hence g.(a * b) = f.(a' * b') by FUNCT_1:72 .= f.a' * f.b' by Def7 .= g.a * g.b by A6,A11,GROUP_2:52; end; then reconsider g as Homomorphism of B,(B "\/" N)./.(B "\/" N,N)`*` by Def7; A12: Ker g = B /\ N proof let b be Element of B; reconsider c = b as Element of G by GROUP_2:51; A13: g.b = f.c by FUNCT_1:72 .= c * N by Def9; thus b in Ker g implies b in B /\ N proof assume b in Ker g; then g.b = 1.I by Th50 .= carr J by Th29 .= the carrier of N by A5,GROUP_2:def 9 .= carr N by GROUP_2:def 9; then b in B & b in N by A13,GROUP_2:136,RLVECT_1:def 1; hence thesis by GROUP_2:99; end; assume b in B /\ N; then b in N by GROUP_2:99; then c * N = carr N by GROUP_2:136 .= the carrier of J by A5,GROUP_2:def 9 .= carr J by GROUP_2:def 9 .= 1.I by Th29; hence thesis by A13,Th50; end; the carrier of I c= rng g proof let x; assume x in the carrier of I; then x in I by RLVECT_1:def 1; then consider b being Element of B "\/" N such that A14: x = b * J & x = J * b by Th28; B * N = N * B & b in B "\/" N by GROUP_5:8,RLVECT_1:def 1; then consider a1,a2 such that A15: b = a1 * a2 and A16: a1 in B & a2 in N by GROUP_5:5; A17: a1 in the carrier of B & a1 in the carrier of G by A16,RLVECT_1: def 1; x = a1 * a2 * N by A5,A14,A15,Th2 .= a1 * (a2 * N) by GROUP_2:127 .= a1 * carr N by A16,GROUP_2:136 .= a1 * N by GROUP_2:def 13 .= f.a1 by Def9 .= g.a1 by A17,FUNCT_1:72; hence thesis by A3,A17,FUNCT_1:def 5; end; then the carrier of I = rng g by XBOOLE_0:def 10; then g is_epimorphism by Def13; then Image g = (B "\/" N)./.(B "\/" N,N)`*` by Th67; hence thesis by A12,Lm9; end;