let O be set ; 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; ( G,H are_isomorphic & G is simple implies H is simple )
assume A1:
G,H are_isomorphic
; ( not G is simple or H is simple )
assume A2:
G is simple
; H is simple
assume A3:
not H is simple
; contradiction
per cases
( H is trivial or ex H9 being strict normal StableSubgroup of H st
( H9 <> (Omega). H & H9 <> (1). H ) )
by A3, Def13;
suppose
ex
H9 being
strict normal StableSubgroup of
H st
(
H9 <> (Omega). H &
H9 <> (1). H )
;
contradictionthen 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, Def22;
reconsider H99 =
multMagma(# the
carrier of
H9,the
multF of
H9 #) as
strict normal Subgroup of
H by Lm7;
multMagma(# the
carrier of
H9,the
multF of
H9 #)
<> multMagma(# the
carrier of
H,the
multF of
H #)
by A4, Lm5;
then consider h being
Element of
H such that A7:
not
h in H99
by GROUP_2:71;
the
carrier of
H9 <> {(1_ H)}
by A5, Def8;
then consider x being
set such that A8:
x in the
carrier of
H9
and A9:
x <> 1_ H
by ZFMISC_1:41;
A10:
x in H99
by A8, STRUCT_0:def 5;
then
x in H
by GROUP_2:49;
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:55;
then
f . (1_ G) in H99
by Lm13;
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 ;
then reconsider A =
A as
Subset of
G by TARSKI:def 3;
then consider G99 being
strict StableSubgroup of
G such that A25:
the
carrier of
G99 = A
by A13, A20, Lm15;
reconsider G9 =
multMagma(# the
carrier of
G99,the
multF of
G99 #) as
strict Subgroup of
G by Lm16;
then
for
H being
strict Subgroup of
G st
H = multMagma(# the
carrier of
G99,the
multF of
G99 #) holds
H is
normal
by GROUP_3:141;
then A31:
G99 is
normal
by Def10;
A32:
y <> 1_ G
by A9, A11, Lm13;
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 assume
g in A
;
contradictionthen
ex
g9 being
Element of
G st
(
g9 = g &
f . g9 in H99 )
;
hence
contradiction
by A7, A12;
verum end; then
G99 <> (Omega). G
by A25;
hence
contradiction
by A2, A33, A31, Def13;
verum end;