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;
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:9;
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:9;
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 for x being object st x in dom (the_left_translation_of ((h1 * h2),p)) holds
(the_left_translation_of ((h1 * h2),p)) . x = (the_left_translation_of (h1,p)) . ((the_left_translation_of (h2,p)) . x)let x be
object ;
( 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))
;
(the_left_translation_of ((h1 * h2),p)) . x = (the_left_translation_of (h1,p)) . ((the_left_translation_of (h2,p)) . x)then reconsider P19 =
x as
Element of
the_sylow_p-subgroups_of_prime (
p,
G) ;
reconsider P1999 =
x as
Element of
the_sylow_p-subgroups_of_prime (
p,
G)
by A5;
consider P29 being
Element of
the_sylow_p-subgroups_of_prime (
p,
G),
H19,
H29 being
strict Subgroup of
G,
g2 being
Element of
G such that A6:
(
P29 = (the_left_translation_of (h2,p)) . P19 &
P19 = H19 &
P29 = H29 )
and A7:
h2 " = g2
and A8:
H29 = H19 |^ g2
by Def20;
(the_left_translation_of (h2,p)) . x in rng (the_left_translation_of (h2,p))
by A3, A5, FUNCT_1:3;
then reconsider P199 =
(the_left_translation_of (h2,p)) . x as
Element of
the_sylow_p-subgroups_of_prime (
p,
G) ;
consider P299 being
Element of
the_sylow_p-subgroups_of_prime (
p,
G),
H199,
H299 being
strict Subgroup of
G,
g1 being
Element of
G such that A9:
P299 = (the_left_translation_of (h1,p)) . P199
and A10:
(
P199 = H199 &
P299 = H299 )
and A11:
h1 " = g1
and A12:
H299 = H199 |^ g1
by Def20;
consider P2999 being
Element of
the_sylow_p-subgroups_of_prime (
p,
G),
H1999,
H2999 being
strict Subgroup of
G,
g3 being
Element of
G such that A13:
P2999 = (the_left_translation_of ((h1 * h2),p)) . P1999
and A14:
P1999 = H1999
and A15:
P2999 = H2999
and A16:
(h1 * h2) " = g3
and A17:
H2999 = H1999 |^ g3
by Def20;
g3 = (h2 ") * (h1 ")
by A16, GROUP_1:17;
then P2999 =
H1999 |^ (g2 * g1)
by A7, A11, A15, A17, GROUP_2:43
.=
P299
by A6, A8, A10, A12, A14, GROUP_3:60
;
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;
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:9;
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 for x being object holds
( ( 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)) ) )let x be
object ;
( ( 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 ( 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))
;
( 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;
(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:3;
hence
(the_left_translation_of (h2,p)) . x in dom (the_left_translation_of (h1,p))
by A2;
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))
;
x in dom (the_left_translation_of ((h1 * h2),p))thus
x in dom (the_left_translation_of ((h1 * h2),p))
by A18, A20;
verum end;
hence
H1(
h1 * h2)
= H1(
h1)
* H1(
h2)
by A4, FUNCT_1:10;
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 for x being object st x in the_sylow_p-subgroups_of_prime (p,G) holds
(the_left_translation_of ((1_ H),p)) . x = xlet x be
object ;
( 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)
;
(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 Def20;
(1_ H) " = 1_ H
by GROUP_1:8;
then
g = 1_ G
by A24, GROUP_2:44;
hence
(the_left_translation_of ((1_ H),p)) . x = x
by A23, A25, GROUP_3:61;
verum end;
thus
H1(
1_ H)
= id (the_sylow_p-subgroups_of_prime (p,G))
by A22;
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)
; verum