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;
set E = the_sylow_p-subgroups_of_prime p,G;
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;
the_left_translation_of h1,
p in Funcs (the_sylow_p-subgroups_of_prime p,G),
(the_sylow_p-subgroups_of_prime p,G)
by FUNCT_2:12;
then A2:
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;
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 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 FUNCT_2:def 2;
A4:
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 A5:
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 ;
reconsider P1''' =
x as
Element of
the_sylow_p-subgroups_of_prime p,
G by A5;
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 A6:
(
P2' = (the_left_translation_of h2,p) . P1' &
P1' = H1' &
P2' = H2' )
and A7:
h2 " = g2
and A8:
H2' = H1' |^ g2
by Def21;
(the_left_translation_of h2,p) . x in rng (the_left_translation_of h2,p)
by A3, A5, 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 A9:
P2'' = (the_left_translation_of h1,p) . P1''
and A10:
(
P1'' = H1'' &
P2'' = H2'' )
and A11:
h1 " = g1
and A12:
H2'' = H1'' |^ g1
by Def21;
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 A13:
P2''' = (the_left_translation_of (h1 * h2),p) . P1'''
and A14:
P1''' = H1'''
and A15:
P2''' = H2'''
and A16:
(h1 * h2) " = g3
and A17:
H2''' = H1''' |^ g3
by Def21;
g3 = (h2 " ) * (h1 " )
by A16, GROUP_1:25;
then P2''' =
H1''' |^ (g2 * g1)
by A7, A11, A15, A17, GROUP_2:52
.=
P2''
by A6, A8, A10, A12, A14, 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 A9, A13;
:: thesis: verum end;
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)
by FUNCT_2:12;
then A18:
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 FUNCT_2:def 2;
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 A19:
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 A3;
:: 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 A3, A19, FUNCT_1:12;
hence
(the_left_translation_of h2,p) . x in dom (the_left_translation_of h1,p)
by A2;
:: thesis: verum
end; assume that A20:
x in dom (the_left_translation_of h2,p)
and
(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)thus
x in dom (the_left_translation_of (h1 * h2),p)
by A18, A20;
:: thesis: verum end;
hence
H1(
h1 * h2)
= H1(
h1)
* H1(
h2)
by A4, FUNCT_1:20;
:: thesis: verum
end;
A21:
H1( 1_ H) = id (the_sylow_p-subgroups_of_prime p,G)
proof
set f =
the_left_translation_of (1_ H),
p;
A22:
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 A23:
(
P2 = (the_left_translation_of (1_ H),p) . P1 &
P1 = H1 &
P2 = H2 )
and A24:
(1_ H) " = g
and A25:
H2 = H1 |^ g
by Def21;
(1_ H) " = 1_ H
by GROUP_1:16;
then
g = 1_ G
by A24, GROUP_2:53;
hence
(the_left_translation_of (1_ H),p) . x = x
by A23, A25, GROUP_3:73;
:: thesis: verum end;
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
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;
hence
H1(
1_ H)
= id (the_sylow_p-subgroups_of_prime p,G)
by A22, 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(A21, 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