deffunc H1( Element of S) -> Function of [: the carrier of S,Z:],[: the carrier of S,Z:] = the_left_translation_of ($1,Z);
set E = [: the carrier of S,Z:];
A1:
for s1, s2 being Element of S holds H1(s1 * s2) = H1(s1) * H1(s2)
proof
let s1,
s2 be
Element of
S;
H1(s1 * s2) = H1(s1) * H1(s2)
set f12 =
the_left_translation_of (
(s1 * s2),
Z);
set f1 =
the_left_translation_of (
s1,
Z);
set f2 =
the_left_translation_of (
s2,
Z);
the_left_translation_of (
s1,
Z)
in Funcs (
[: the carrier of S,Z:],
[: the carrier of S,Z:])
by FUNCT_2:9;
then A2:
ex
f being
Function st
(
the_left_translation_of (
s1,
Z)
= f &
dom f = [: the carrier of S,Z:] &
rng f c= [: the carrier of S,Z:] )
by FUNCT_2:def 2;
the_left_translation_of (
s2,
Z)
in Funcs (
[: the carrier of S,Z:],
[: the carrier of S,Z:])
by FUNCT_2:9;
then A3:
ex
f being
Function st
(
the_left_translation_of (
s2,
Z)
= f &
dom f = [: the carrier of S,Z:] &
rng f c= [: the carrier of S,Z:] )
by FUNCT_2:def 2;
A4:
now for x being object st x in dom (the_left_translation_of ((s1 * s2),Z)) holds
(the_left_translation_of ((s1 * s2),Z)) . x = (the_left_translation_of (s1,Z)) . ((the_left_translation_of (s2,Z)) . x)let x be
object ;
( x in dom (the_left_translation_of ((s1 * s2),Z)) implies (the_left_translation_of ((s1 * s2),Z)) . x = (the_left_translation_of (s1,Z)) . ((the_left_translation_of (s2,Z)) . x) )assume A5:
x in dom (the_left_translation_of ((s1 * s2),Z))
;
(the_left_translation_of ((s1 * s2),Z)) . x = (the_left_translation_of (s1,Z)) . ((the_left_translation_of (s2,Z)) . x)then reconsider z19 =
x as
Element of
[: the carrier of S,Z:] ;
reconsider z1999 =
x as
Element of
[: the carrier of S,Z:] by A5;
consider z29 being
Element of
[: the carrier of S,Z:],
s19,
s29 being
Element of
S,
z9 being
Element of
Z such that A6:
z29 = (the_left_translation_of (s2,Z)) . z19
and A7:
s29 = s2 * s19
and A8:
z19 = [s19,z9]
and A9:
z29 = [s29,z9]
by Def6;
(the_left_translation_of (s2,Z)) . x in rng (the_left_translation_of (s2,Z))
by A3, A5, FUNCT_1:3;
then reconsider z199 =
(the_left_translation_of (s2,Z)) . x as
Element of
[: the carrier of S,Z:] ;
consider z299 being
Element of
[: the carrier of S,Z:],
s199,
s299 being
Element of
S,
z99 being
Element of
Z such that A10:
z299 = (the_left_translation_of (s1,Z)) . z199
and A11:
s299 = s1 * s199
and A12:
z199 = [s199,z99]
and A13:
z299 = [s299,z99]
by Def6;
A14:
z99 = z9
by A6, A9, A12, XTUPLE_0:1;
consider z2999 being
Element of
[: the carrier of S,Z:],
s1999,
s2999 being
Element of
S,
z999 being
Element of
Z such that A15:
z2999 = (the_left_translation_of ((s1 * s2),Z)) . z1999
and A16:
s2999 = (s1 * s2) * s1999
and A17:
z1999 = [s1999,z999]
and A18:
z2999 = [s2999,z999]
by Def6;
s2999 =
(s1 * s2) * s19
by A8, A16, A17, XTUPLE_0:1
.=
s1 * (s2 * s19)
by GROUP_1:def 3
.=
s299
by A6, A7, A9, A11, A12, XTUPLE_0:1
;
hence
(the_left_translation_of ((s1 * s2),Z)) . x = (the_left_translation_of (s1,Z)) . ((the_left_translation_of (s2,Z)) . x)
by A8, A10, A13, A15, A17, A18, A14, XTUPLE_0:1;
verum end;
the_left_translation_of (
(s1 * s2),
Z)
in Funcs (
[: the carrier of S,Z:],
[: the carrier of S,Z:])
by FUNCT_2:9;
then A19:
ex
f being
Function st
(
the_left_translation_of (
(s1 * s2),
Z)
= f &
dom f = [: the carrier of S,Z:] &
rng f c= [: the carrier of S,Z:] )
by FUNCT_2:def 2;
now for x being object holds
( ( x in dom (the_left_translation_of ((s1 * s2),Z)) implies ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) ) ) & ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) implies x in dom (the_left_translation_of ((s1 * s2),Z)) ) )let x be
object ;
( ( x in dom (the_left_translation_of ((s1 * s2),Z)) implies ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) ) ) & ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) implies x in dom (the_left_translation_of ((s1 * s2),Z)) ) )hereby ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) implies x in dom (the_left_translation_of ((s1 * s2),Z)) )
assume A20:
x in dom (the_left_translation_of ((s1 * s2),Z))
;
( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) )hence
x in dom (the_left_translation_of (s2,Z))
by A3;
(the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z))
(the_left_translation_of (s2,Z)) . x in rng (the_left_translation_of (s2,Z))
by A3, A20, FUNCT_1:3;
hence
(the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z))
by A2;
verum
end; assume that A21:
x in dom (the_left_translation_of (s2,Z))
and
(the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z))
;
x in dom (the_left_translation_of ((s1 * s2),Z))thus
x in dom (the_left_translation_of ((s1 * s2),Z))
by A19, A21;
verum end;
hence
H1(
s1 * s2)
= H1(
s1)
* H1(
s2)
by A4, FUNCT_1:10;
verum
end;
A22:
H1( 1_ S) = id [: the carrier of S,Z:]
proof
set f =
the_left_translation_of (
(1_ S),
Z);
A23:
now for x being object st x in [: the carrier of S,Z:] holds
(the_left_translation_of ((1_ S),Z)) . x = xlet x be
object ;
( x in [: the carrier of S,Z:] implies (the_left_translation_of ((1_ S),Z)) . x = x )assume
x in [: the carrier of S,Z:]
;
(the_left_translation_of ((1_ S),Z)) . x = xthen reconsider z1 =
x as
Element of
[: the carrier of S,Z:] ;
ex
z2 being
Element of
[: the carrier of S,Z:] ex
s1,
s2 being
Element of
S ex
z being
Element of
Z st
(
z2 = (the_left_translation_of ((1_ S),Z)) . z1 &
s2 = (1_ S) * s1 &
z1 = [s1,z] &
z2 = [s2,z] )
by Def6;
hence
(the_left_translation_of ((1_ S),Z)) . x = x
by GROUP_1:def 4;
verum end;
thus
H1(
1_ S)
= id [: the carrier of S,Z:]
by A23;
verum
end;
ex T being LeftOperation of S,[: the carrier of S,Z:] st
for s being Element of S holds T . s = H1(s)
from GROUP_10:sch 1(A22, A1);
hence
ex b1 being LeftOperation of S,[: the carrier of S,Z:] st
for s being Element of S holds b1 . s = the_left_translation_of (s,Z)
; verum