set E = the_sylow_p-subgroups_of_prime p,G;
deffunc H1( Element of H) -> Function of (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) = the_left_translation_of $1,p;
A1:
for h1, h2 being Element of H holds H1(h1 * h2) = H1(h1) * H1(h2)
proof
let h1,
h2 be
Element of
H;
:: thesis: H1(h1 * h2) = H1(h1) * H1(h2)
set f12 =
the_left_translation_of (h1 * h2),
p;
set f1 =
the_left_translation_of h1,
p;
set f2 =
the_left_translation_of h2,
p;
A2:
(
the_left_translation_of (h1 * h2),
p in Funcs (the_sylow_p-subgroups_of_prime p,G),
(the_sylow_p-subgroups_of_prime p,G) &
the_left_translation_of h1,
p in Funcs (the_sylow_p-subgroups_of_prime p,G),
(the_sylow_p-subgroups_of_prime p,G) &
the_left_translation_of h2,
p in Funcs (the_sylow_p-subgroups_of_prime p,G),
(the_sylow_p-subgroups_of_prime p,G) )
by FUNCT_2:12;
then A3:
ex
f being
Function st
(
the_left_translation_of h1,
p = f &
dom f = the_sylow_p-subgroups_of_prime p,
G &
rng f c= the_sylow_p-subgroups_of_prime p,
G )
by FUNCT_2:def 2;
A4:
ex
f being
Function st
(
the_left_translation_of h2,
p = f &
dom f = the_sylow_p-subgroups_of_prime p,
G &
rng f c= the_sylow_p-subgroups_of_prime p,
G )
by A2, FUNCT_2:def 2;
A5:
ex
f being
Function st
(
the_left_translation_of (h1 * h2),
p = f &
dom f = the_sylow_p-subgroups_of_prime p,
G &
rng f c= the_sylow_p-subgroups_of_prime p,
G )
by A2, FUNCT_2:def 2;
A6:
now let x be
set ;
:: thesis: ( ( x in dom (the_left_translation_of (h1 * h2),p) implies ( x in dom (the_left_translation_of h2,p) & (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) ) ) & ( x in dom (the_left_translation_of h2,p) & (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) implies x in dom (the_left_translation_of (h1 * h2),p) ) )hereby :: thesis: ( x in dom (the_left_translation_of h2,p) & (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) implies x in dom (the_left_translation_of (h1 * h2),p) )
assume A7:
x in dom (the_left_translation_of (h1 * h2),p)
;
:: thesis: ( x in dom (the_left_translation_of h2,p) & (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) )hence
x in dom (the_left_translation_of h2,p)
by A4;
:: thesis: (the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p)
(the_left_translation_of h2,p) . x in rng (the_left_translation_of h2,p)
by A4, A7, FUNCT_1:12;
hence
(the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p)
by A3;
:: thesis: verum
end; assume
(
x in dom (the_left_translation_of h2,p) &
(the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p) )
;
:: thesis: x in dom (the_left_translation_of (h1 * h2),p)hence
x in dom (the_left_translation_of (h1 * h2),p)
by A5;
:: thesis: verum end;
now let x be
set ;
:: thesis: ( x in dom (the_left_translation_of (h1 * h2),p) implies (the_left_translation_of (h1 * h2),p) . x = (the_left_translation_of h1,p) . ((the_left_translation_of h2,p) . x) )assume A8:
x in dom (the_left_translation_of (h1 * h2),p)
;
:: thesis: (the_left_translation_of (h1 * h2),p) . x = (the_left_translation_of h1,p) . ((the_left_translation_of h2,p) . x)then reconsider P1' =
x as
Element of
the_sylow_p-subgroups_of_prime p,
G ;
consider P2' being
Element of
the_sylow_p-subgroups_of_prime p,
G,
H1',
H2' being
strict Subgroup of
G,
g2 being
Element of
G such that A9:
(
P2' = (the_left_translation_of h2,p) . P1' &
P1' = H1' &
P2' = H2' &
h2 " = g2 &
H2' = H1' |^ g2 )
by Def21;
(the_left_translation_of h2,p) . x in rng (the_left_translation_of h2,p)
by A4, A8, FUNCT_1:12;
then reconsider P1'' =
(the_left_translation_of h2,p) . x as
Element of
the_sylow_p-subgroups_of_prime p,
G ;
consider P2'' being
Element of
the_sylow_p-subgroups_of_prime p,
G,
H1'',
H2'' being
strict Subgroup of
G,
g1 being
Element of
G such that A10:
(
P2'' = (the_left_translation_of h1,p) . P1'' &
P1'' = H1'' &
P2'' = H2'' &
h1 " = g1 &
H2'' = H1'' |^ g1 )
by Def21;
reconsider P1''' =
x as
Element of
the_sylow_p-subgroups_of_prime p,
G by A8;
consider P2''' being
Element of
the_sylow_p-subgroups_of_prime p,
G,
H1''',
H2''' being
strict Subgroup of
G,
g3 being
Element of
G such that A11:
(
P2''' = (the_left_translation_of (h1 * h2),p) . P1''' &
P1''' = H1''' &
P2''' = H2''' &
(h1 * h2) " = g3 &
H2''' = H1''' |^ g3 )
by Def21;
g3 = (h2 " ) * (h1 " )
by A11, GROUP_1:25;
then P2''' =
H1''' |^ (g2 * g1)
by A9, A10, A11, GROUP_2:52
.=
P2''
by A9, A10, A11, GROUP_3:72
;
hence
(the_left_translation_of (h1 * h2),p) . x = (the_left_translation_of h1,p) . ((the_left_translation_of h2,p) . x)
by A10, A11;
:: thesis: verum end;
hence
H1(
h1 * h2)
= H1(
h1)
* H1(
h2)
by A6, FUNCT_1:20;
:: thesis: verum
end;
A12:
H1( 1_ H) = id (the_sylow_p-subgroups_of_prime p,G)
proof
set f =
the_left_translation_of (1_ H),
p;
the_left_translation_of (1_ H),
p in Funcs (the_sylow_p-subgroups_of_prime p,G),
(the_sylow_p-subgroups_of_prime p,G)
by FUNCT_2:12;
then A13:
ex
f' being
Function st
(
the_left_translation_of (1_ H),
p = f' &
dom f' = the_sylow_p-subgroups_of_prime p,
G &
rng f' c= the_sylow_p-subgroups_of_prime p,
G )
by FUNCT_2:def 2;
now let x be
set ;
:: thesis: ( x in the_sylow_p-subgroups_of_prime p,G implies (the_left_translation_of (1_ H),p) . x = x )assume
x in the_sylow_p-subgroups_of_prime p,
G
;
:: thesis: (the_left_translation_of (1_ H),p) . x = xthen reconsider P1 =
x as
Element of
the_sylow_p-subgroups_of_prime p,
G ;
consider P2 being
Element of
the_sylow_p-subgroups_of_prime p,
G,
H1,
H2 being
strict Subgroup of
G,
g being
Element of
G such that A14:
(
P2 = (the_left_translation_of (1_ H),p) . P1 &
P1 = H1 &
P2 = H2 &
(1_ H) " = g &
H2 = H1 |^ g )
by Def21;
(1_ H) " = 1_ H
by GROUP_1:16;
then
g = 1_ G
by A14, GROUP_2:53;
hence
(the_left_translation_of (1_ H),p) . x = x
by A14, GROUP_3:73;
:: thesis: verum end;
hence
H1(
1_ H)
= id (the_sylow_p-subgroups_of_prime p,G)
by A13, FUNCT_1:34;
:: thesis: verum
end;
ex T being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) st
for h being Element of H holds T . h = H1(h)
from GROUP_10:sch 1(A12, A1);
hence
ex b1 being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) st
for h being Element of H holds b1 . h = the_left_translation_of h,p
; :: thesis: verum