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