let O be set ; :: thesis: for G, H being strict GroupWithOperators of O st G,H are_isomorphic & G is simple holds

H is simple

let G, H be strict GroupWithOperators of O; :: thesis: ( G,H are_isomorphic & G is simple implies H is simple )

assume A1: G,H are_isomorphic ; :: thesis: ( not G is simple or H is simple )

assume A2: G is simple ; :: thesis: H is simple

assume A3: not H is simple ; :: thesis: contradiction

H is simple

let G, H be strict GroupWithOperators of O; :: thesis: ( G,H are_isomorphic & G is simple implies H is simple )

assume A1: G,H are_isomorphic ; :: thesis: ( not G is simple or H is simple )

assume A2: G is simple ; :: thesis: H is simple

assume A3: not H is simple ; :: thesis: contradiction

per cases
( H is trivial or ex H9 being strict normal StableSubgroup of H st

( H9 <> (Omega). H & H9 <> (1). H ) ) by A3;

end;

( H9 <> (Omega). H & H9 <> (1). H ) ) by A3;

suppose
ex H9 being strict normal StableSubgroup of H st

( H9 <> (Omega). H & H9 <> (1). H ) ; :: thesis: contradiction

( H9 <> (Omega). H & H9 <> (1). H ) ; :: thesis: contradiction

then consider H9 being strict normal StableSubgroup of H such that

A4: H9 <> (Omega). H and

A5: H9 <> (1). H ;

consider f being Homomorphism of G,H such that

A6: f is bijective by A1;

reconsider H99 = multMagma(# the carrier of H9, the multF of H9 #) as strict normal Subgroup of H by Lm6;

multMagma(# the carrier of H9, the multF of H9 #) <> multMagma(# the carrier of H, the multF of H #) by A4, Lm4;

then consider h being Element of H such that

A7: not h in H99 by GROUP_2:62;

the carrier of H9 <> {(1_ H)} by A5, Def8;

then consider x being object such that

A8: x in the carrier of H9 and

A9: x <> 1_ H by ZFMISC_1:35;

A10: x in H99 by A8, STRUCT_0:def 5;

then x in H by GROUP_2:40;

then reconsider x = x as Element of H by STRUCT_0:def 5;

consider y being Element of G such that

A11: f . y = x by A6, Th52;

set A = { g where g is Element of G : f . g in H99 } ;

consider g being Element of G such that

A12: f . g = h by A6, Th52;

1_ H in H99 by GROUP_2:46;

then f . (1_ G) in H99 by Lm12;

then 1_ G in { g where g is Element of G : f . g in H99 } ;

then reconsider A = { g where g is Element of G : f . g in H99 } as non empty set ;

A25: the carrier of G99 = A by A13, A20, Lm14;

reconsider G9 = multMagma(# the carrier of G99, the multF of G99 #) as strict Subgroup of G by Lm15;

H is normal by GROUP_3:118;

then A31: G99 is normal ;

A32: y <> 1_ G by A9, A11, Lm12;

y in the carrier of G99 by A25, A10, A11;

then the carrier of G99 <> {(1_ G)} by A32, TARSKI:def 1;

then A33: G99 <> (1). G by Def8;

hence contradiction by A2, A33, A31; :: thesis: verum

end;A4: H9 <> (Omega). H and

A5: H9 <> (1). H ;

consider f being Homomorphism of G,H such that

A6: f is bijective by A1;

reconsider H99 = multMagma(# the carrier of H9, the multF of H9 #) as strict normal Subgroup of H by Lm6;

multMagma(# the carrier of H9, the multF of H9 #) <> multMagma(# the carrier of H, the multF of H #) by A4, Lm4;

then consider h being Element of H such that

A7: not h in H99 by GROUP_2:62;

the carrier of H9 <> {(1_ H)} by A5, Def8;

then consider x being object such that

A8: x in the carrier of H9 and

A9: x <> 1_ H by ZFMISC_1:35;

A10: x in H99 by A8, STRUCT_0:def 5;

then x in H by GROUP_2:40;

then reconsider x = x as Element of H by STRUCT_0:def 5;

consider y being Element of G such that

A11: f . y = x by A6, Th52;

set A = { g where g is Element of G : f . g in H99 } ;

consider g being Element of G such that

A12: f . g = h by A6, Th52;

1_ H in H99 by GROUP_2:46;

then f . (1_ G) in H99 by Lm12;

then 1_ G in { g where g is Element of G : f . g in H99 } ;

then reconsider A = { g where g is Element of G : f . g in H99 } as non empty set ;

now :: thesis: for x being object st x in A holds

x in the carrier of G

then reconsider A = A as Subset of G by TARSKI:def 3;x in the carrier of G

let x be object ; :: thesis: ( x in A implies x in the carrier of G )

assume x in A ; :: thesis: x in the carrier of G

then ex g being Element of G st

( x = g & f . g in H99 ) ;

hence x in the carrier of G ; :: thesis: verum

end;assume x in A ; :: thesis: x in the carrier of G

then ex g being Element of G st

( x = g & f . g in H99 ) ;

hence x in the carrier of G ; :: thesis: verum

A13: now :: thesis: for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A

g1 * g2 in A

let g1, g2 be Element of G; :: thesis: ( g1 in A & g2 in A implies g1 * g2 in A )

assume that

A14: g1 in A and

A15: g2 in A ; :: thesis: g1 * g2 in A

consider b being Element of G such that

A16: b = g2 and

A17: f . b in H99 by A15;

consider a being Element of G such that

A18: a = g1 and

A19: f . a in H99 by A14;

set fb = f . b;

set fa = f . a;

( f . (a * b) = (f . a) * (f . b) & (f . a) * (f . b) in H99 ) by A19, A17, GROUP_2:50, GROUP_6:def 6;

hence g1 * g2 in A by A18, A16; :: thesis: verum

end;assume that

A14: g1 in A and

A15: g2 in A ; :: thesis: g1 * g2 in A

consider b being Element of G such that

A16: b = g2 and

A17: f . b in H99 by A15;

consider a being Element of G such that

A18: a = g1 and

A19: f . a in H99 by A14;

set fb = f . b;

set fa = f . a;

( f . (a * b) = (f . a) * (f . b) & (f . a) * (f . b) in H99 ) by A19, A17, GROUP_2:50, GROUP_6:def 6;

hence g1 * g2 in A by A18, A16; :: thesis: verum

A20: now :: thesis: for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A

for g being Element of G st g in A holds

(G ^ o) . g in A

let o be Element of O; :: thesis: for g being Element of G st g in A holds

(G ^ o) . g in A

let g be Element of G; :: thesis: ( g in A implies (G ^ o) . g in A )

assume g in A ; :: thesis: (G ^ o) . g in A

then consider a being Element of G such that

A21: a = g and

A22: f . a in H99 ;

f . a in the carrier of H99 by A22, STRUCT_0:def 5;

then f . a in H9 by STRUCT_0:def 5;

then (H ^ o) . (f . g) in H9 by A21, Lm9;

then f . ((G ^ o) . g) in H9 by Def18;

then f . ((G ^ o) . g) in the carrier of H9 by STRUCT_0:def 5;

then f . ((G ^ o) . g) in H99 by STRUCT_0:def 5;

hence (G ^ o) . g in A ; :: thesis: verum

end;(G ^ o) . g in A

let g be Element of G; :: thesis: ( g in A implies (G ^ o) . g in A )

assume g in A ; :: thesis: (G ^ o) . g in A

then consider a being Element of G such that

A21: a = g and

A22: f . a in H99 ;

f . a in the carrier of H99 by A22, STRUCT_0:def 5;

then f . a in H9 by STRUCT_0:def 5;

then (H ^ o) . (f . g) in H9 by A21, Lm9;

then f . ((G ^ o) . g) in H9 by Def18;

then f . ((G ^ o) . g) in the carrier of H9 by STRUCT_0:def 5;

then f . ((G ^ o) . g) in H99 by STRUCT_0:def 5;

hence (G ^ o) . g in A ; :: thesis: verum

now :: thesis: for g being Element of G st g in A holds

g " in A

then consider G99 being strict StableSubgroup of G such that g " in A

let g be Element of G; :: thesis: ( g in A implies g " in A )

assume g in A ; :: thesis: g " in A

then consider a being Element of G such that

A23: a = g and

A24: f . a in H99 ;

(f . a) " in H99 by A24, GROUP_2:51;

then f . (a ") in H99 by Lm13;

hence g " in A by A23; :: thesis: verum

end;assume g in A ; :: thesis: g " in A

then consider a being Element of G such that

A23: a = g and

A24: f . a in H99 ;

(f . a) " in H99 by A24, GROUP_2:51;

then f . (a ") in H99 by Lm13;

hence g " in A by A23; :: thesis: verum

A25: the carrier of G99 = A by A13, A20, Lm14;

reconsider G9 = multMagma(# the carrier of G99, the multF of G99 #) as strict Subgroup of G by Lm15;

now :: thesis: for g being Element of G holds g * G9 c= G9 * g

then
for H being strict Subgroup of G st H = multMagma(# the carrier of G99, the multF of G99 #) holds let g be Element of G; :: thesis: g * G9 c= G9 * g

end;now :: thesis: for x being object st x in g * G9 holds

x in G9 * g

hence
g * G9 c= G9 * g
; :: thesis: verumx in G9 * g

let x be object ; :: thesis: ( x in g * G9 implies x in G9 * g )

A26: H99 |^ ((f . g) ") = H99 by GROUP_3:def 13;

assume x in g * G9 ; :: thesis: x in G9 * g

then consider h being Element of G such that

A27: x = g * h and

A28: h in A by A25, GROUP_2:27;

set h9 = (g * h) * (g ");

A29: f . ((g * h) * (g ")) = (f . (g * h)) * (f . (g ")) by GROUP_6:def 6

.= ((f . g) * (f . h)) * (f . (g ")) by GROUP_6:def 6

.= ((((f . g) ") ") * (f . h)) * ((f . g) ") by Lm13

.= (f . h) |^ ((f . g) ") by GROUP_3:def 2 ;

ex a being Element of G st

( a = h & f . a in H99 ) by A28;

then f . ((g * h) * (g ")) in H99 by A26, A29, GROUP_3:58;

then A30: (g * h) * (g ") in A ;

((g * h) * (g ")) * g = (g * h) * ((g ") * g) by GROUP_1:def 3

.= (g * h) * (1_ G) by GROUP_1:def 5

.= x by A27, GROUP_1:def 4 ;

hence x in G9 * g by A25, A30, GROUP_2:28; :: thesis: verum

end;A26: H99 |^ ((f . g) ") = H99 by GROUP_3:def 13;

assume x in g * G9 ; :: thesis: x in G9 * g

then consider h being Element of G such that

A27: x = g * h and

A28: h in A by A25, GROUP_2:27;

set h9 = (g * h) * (g ");

A29: f . ((g * h) * (g ")) = (f . (g * h)) * (f . (g ")) by GROUP_6:def 6

.= ((f . g) * (f . h)) * (f . (g ")) by GROUP_6:def 6

.= ((((f . g) ") ") * (f . h)) * ((f . g) ") by Lm13

.= (f . h) |^ ((f . g) ") by GROUP_3:def 2 ;

ex a being Element of G st

( a = h & f . a in H99 ) by A28;

then f . ((g * h) * (g ")) in H99 by A26, A29, GROUP_3:58;

then A30: (g * h) * (g ") in A ;

((g * h) * (g ")) * g = (g * h) * ((g ") * g) by GROUP_1:def 3

.= (g * h) * (1_ G) by GROUP_1:def 5

.= x by A27, GROUP_1:def 4 ;

hence x in G9 * g by A25, A30, GROUP_2:28; :: thesis: verum

H is normal by GROUP_3:118;

then A31: G99 is normal ;

A32: y <> 1_ G by A9, A11, Lm12;

y in the carrier of G99 by A25, A10, A11;

then the carrier of G99 <> {(1_ G)} by A32, TARSKI:def 1;

then A33: G99 <> (1). G by Def8;

now :: thesis: not g in A

then
G99 <> (Omega). G
by A25;assume
g in A
; :: thesis: contradiction

then ex g9 being Element of G st

( g9 = g & f . g9 in H99 ) ;

hence contradiction by A7, A12; :: thesis: verum

end;then ex g9 being Element of G st

( g9 = g & f . g9 in H99 ) ;

hence contradiction by A7, A12; :: thesis: verum

hence contradiction by A2, A33, A31; :: thesis: verum