set f = { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ;
set E = the_sylow_p-subgroups_of_prime p,G;
A1:
now let x,
y1,
y2 be
set ;
:: thesis: ( [x,y1] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } & [x,y2] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies y1 = y2 )assume
[x,y1] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) }
;
:: thesis: ( [x,y2] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies y1 = y2 )then consider P1',
P2' being
Element of
the_sylow_p-subgroups_of_prime p,
G such that A2:
(
[x,y1] = [P1',P2'] & ex
H1,
H2 being
strict Subgroup of
G ex
g being
Element of
G st
(
P1' = H1 &
P2' = H2 &
h " = g &
H2 = H1 |^ g ) )
;
assume
[x,y2] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) }
;
:: thesis: y1 = y2then consider P1'',
P2'' being
Element of
the_sylow_p-subgroups_of_prime p,
G such that A3:
(
[x,y2] = [P1'',P2''] & ex
H1,
H2 being
strict Subgroup of
G ex
g being
Element of
G st
(
P1'' = H1 &
P2'' = H2 &
h " = g &
H2 = H1 |^ g ) )
;
A4:
(
x = P1' &
y1 = P2' )
by A2, ZFMISC_1:33;
(
x = P1'' &
y2 = P2'' )
by A3, ZFMISC_1:33;
hence
y1 = y2
by A2, A3, A4;
:: thesis: verum end;
now let x be
set ;
:: thesis: ( x in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies ex y, z being set st x = [y,z] )assume
x in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) }
;
:: thesis: ex y, z being set st x = [y,z]then consider P1,
P2 being
Element of
the_sylow_p-subgroups_of_prime p,
G such that A5:
(
x = [P1,P2] & ex
H1,
H2 being
strict Subgroup of
G ex
g being
Element of
G st
(
P1 = H1 &
P2 = H2 &
h " = g &
H2 = H1 |^ g ) )
;
reconsider y =
P1,
z =
P2 as
set ;
take y =
y;
:: thesis: ex z being set st x = [y,z]take z =
z;
:: thesis: x = [y,z]thus
x = [y,z]
by A5;
:: thesis: verum end;
then reconsider f = { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime p,G : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;
now let x be
set ;
:: thesis: ( ( x in the_sylow_p-subgroups_of_prime p,G implies ex y being set st [x,y] in f ) & ( ex y being set st [x,y] in f implies x in the_sylow_p-subgroups_of_prime p,G ) )hereby :: thesis: ( ex y being set st [x,y] in f implies x in the_sylow_p-subgroups_of_prime p,G )
assume
x in the_sylow_p-subgroups_of_prime p,
G
;
:: thesis: ex y being set st [x,y] in fthen reconsider P1 =
x as
Element of
the_sylow_p-subgroups_of_prime p,
G ;
P1 in the_sylow_p-subgroups_of_prime p,
G
;
then consider H1 being
Element of
Subgroups G such that A6:
(
P1 = H1 & ex
P being
strict Subgroup of
G st
(
P = H1 &
P is_Sylow_p-subgroup_of_prime p ) )
;
reconsider H1 =
H1 as
strict Subgroup of
G by A6;
A7:
(
H1 is_p-group_of_prime p & not
p divides index H1 )
by A6, Def19;
then consider H' being
finite Group such that A8:
(
H1 = H' &
H' is_p-group_of_prime p )
by Def18;
consider r being
natural number such that A9:
card H' = p |^ r
by A8, Def17;
reconsider g =
h " as
Element of
G by GROUP_2:51;
set H2 =
H1 |^ g;
reconsider H2 =
H1 |^ g as
strict Subgroup of
G ;
A11:
card H1 = card H2
by GROUP_3:79;
A12:
(card H1) * (index H1) =
card G
by GROUP_2:177
.=
(card H1) * (index H2)
by A11, GROUP_2:177
;
reconsider H'' =
H2 as
finite Group ;
card H' = card H''
by A8, GROUP_3:79;
then
H'' is_p-group_of_prime p
by A9, Def17;
then
(
H2 is_p-group_of_prime p & not
p divides index H2 )
by A7, A12, Def18, XCMPLX_1:5;
then A13:
H2 is_Sylow_p-subgroup_of_prime p
by Def19;
reconsider H2' =
H2 as
Element of
Subgroups G by GROUP_3:def 1;
H2' in the_sylow_p-subgroups_of_prime p,
G
by A13;
then reconsider P2 =
H2 as
Element of
the_sylow_p-subgroups_of_prime p,
G ;
reconsider y =
P2 as
set ;
take y =
y;
:: thesis: [x,y] in fthus
[x,y] in f
by A6;
:: thesis: verum
end; given y being
set such that A14:
[x,y] in f
;
:: thesis: x in the_sylow_p-subgroups_of_prime p,Gconsider P1,
P2 being
Element of
the_sylow_p-subgroups_of_prime p,
G such that A15:
(
[x,y] = [P1,P2] & ex
H1,
H2 being
strict Subgroup of
G ex
g being
Element of
G st
(
P1 = H1 &
P2 = H2 &
h " = g &
H2 = H1 |^ g ) )
by A14;
x = P1
by A15, ZFMISC_1:33;
hence
x in the_sylow_p-subgroups_of_prime p,
G
;
:: thesis: verum end;
then A16:
dom f = the_sylow_p-subgroups_of_prime p,G
by RELAT_1:def 4;
now let y be
set ;
:: thesis: ( y in rng f implies y in the_sylow_p-subgroups_of_prime p,G )assume
y in rng f
;
:: thesis: y in the_sylow_p-subgroups_of_prime p,Gthen consider x being
set such that A17:
[x,y] in f
by RELAT_1:def 5;
consider P1,
P2 being
Element of
the_sylow_p-subgroups_of_prime p,
G such that A18:
(
[x,y] = [P1,P2] & ex
H1,
H2 being
strict Subgroup of
G ex
g being
Element of
G st
(
P1 = H1 &
P2 = H2 &
h " = g &
H2 = H1 |^ g ) )
by A17;
y = P2
by A18, ZFMISC_1:33;
hence
y in the_sylow_p-subgroups_of_prime p,
G
;
:: thesis: verum end;
then
rng f c= the_sylow_p-subgroups_of_prime p,G
by TARSKI:def 3;
then reconsider f = f as Function of (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) by A16, FUNCT_2:4;
take
f
; :: thesis: for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
thus
for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
:: thesis: verumproof
let P1 be
Element of
the_sylow_p-subgroups_of_prime p,
G;
:: thesis: ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
set P2 =
f . P1;
[P1,(f . P1)] in f
by A16, FUNCT_1:8;
then consider P1',
P2' being
Element of
the_sylow_p-subgroups_of_prime p,
G such that A19:
(
[P1,(f . P1)] = [P1',P2'] & ex
H1,
H2 being
strict Subgroup of
G ex
g being
Element of
G st
(
P1' = H1 &
P2' = H2 &
h " = g &
H2 = H1 |^ g ) )
;
consider H1,
H2 being
strict Subgroup of
G,
g being
Element of
G such that A20:
(
P1' = H1 &
P2' = H2 &
h " = g &
H2 = H1 |^ g )
by A19;
reconsider P2 =
f . P1 as
Element of
the_sylow_p-subgroups_of_prime p,
G ;
take
P2
;
:: thesis: ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
take
H1
;
:: thesis: ex H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
take
H2
;
:: thesis: ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
take
g
;
:: thesis: ( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
thus
P2 = f . P1
;
:: thesis: ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
thus
(
P1 = H1 &
P2 = H2 &
h " = g &
H2 = H1 |^ g )
by A19, A20, ZFMISC_1:33;
:: thesis: verum
end;