deffunc H1( Element of S) -> Function of (the_subsets_of_card n,E),(the_subsets_of_card n,E) = the_extension_of_left_translation_of n,$1,LO;
set EE = the_subsets_of_card n,E;
A2:
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_extension_of_left_translation_of n,
(s1 * s2),
LO;
set f1 =
the_extension_of_left_translation_of n,
s1,
LO;
set f2 =
the_extension_of_left_translation_of n,
s2,
LO;
the_extension_of_left_translation_of n,
s1,
LO in Funcs (the_subsets_of_card n,E),
(the_subsets_of_card n,E)
by FUNCT_2:12;
then A3:
ex
f being
Function st
(
the_extension_of_left_translation_of n,
s1,
LO = f &
dom f = the_subsets_of_card n,
E &
rng f c= the_subsets_of_card n,
E )
by FUNCT_2:def 2;
the_extension_of_left_translation_of n,
s2,
LO in Funcs (the_subsets_of_card n,E),
(the_subsets_of_card n,E)
by FUNCT_2:12;
then A4:
ex
f being
Function st
(
the_extension_of_left_translation_of n,
s2,
LO = f &
dom f = the_subsets_of_card n,
E &
rng f c= the_subsets_of_card n,
E )
by FUNCT_2:def 2;
the_extension_of_left_translation_of n,
(s1 * s2),
LO in Funcs (the_subsets_of_card n,E),
(the_subsets_of_card n,E)
by FUNCT_2:12;
then A5:
ex
f being
Function st
(
the_extension_of_left_translation_of n,
(s1 * s2),
LO = f &
dom f = the_subsets_of_card n,
E &
rng f c= the_subsets_of_card n,
E )
by FUNCT_2:def 2;
A6:
now let x be
set ;
( ( x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO) implies ( x in dom (the_extension_of_left_translation_of n,s2,LO) & (the_extension_of_left_translation_of n,s2,LO) . x in dom (the_extension_of_left_translation_of n,s1,LO) ) ) & ( x in dom (the_extension_of_left_translation_of n,s2,LO) & (the_extension_of_left_translation_of n,s2,LO) . x in dom (the_extension_of_left_translation_of n,s1,LO) implies x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO) ) )hereby ( x in dom (the_extension_of_left_translation_of n,s2,LO) & (the_extension_of_left_translation_of n,s2,LO) . x in dom (the_extension_of_left_translation_of n,s1,LO) implies x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO) )
assume A7:
x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO)
;
( x in dom (the_extension_of_left_translation_of n,s2,LO) & (the_extension_of_left_translation_of n,s2,LO) . x in dom (the_extension_of_left_translation_of n,s1,LO) )hence
x in dom (the_extension_of_left_translation_of n,s2,LO)
by A4;
(the_extension_of_left_translation_of n,s2,LO) . x in dom (the_extension_of_left_translation_of n,s1,LO)
(the_extension_of_left_translation_of n,s2,LO) . x in rng (the_extension_of_left_translation_of n,s2,LO)
by A4, A7, FUNCT_1:12;
hence
(the_extension_of_left_translation_of n,s2,LO) . x in dom (the_extension_of_left_translation_of n,s1,LO)
by A3;
verum
end; assume that A8:
x in dom (the_extension_of_left_translation_of n,s2,LO)
and
(the_extension_of_left_translation_of n,s2,LO) . x in dom (the_extension_of_left_translation_of n,s1,LO)
;
x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO)thus
x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO)
by A5, A8;
verum end;
now let x be
set ;
( x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO) implies (the_extension_of_left_translation_of n,(s1 * s2),LO) . x = (the_extension_of_left_translation_of n,s1,LO) . ((the_extension_of_left_translation_of n,s2,LO) . x) )assume A9:
x in dom (the_extension_of_left_translation_of n,(s1 * s2),LO)
;
(the_extension_of_left_translation_of n,(s1 * s2),LO) . x = (the_extension_of_left_translation_of n,s1,LO) . ((the_extension_of_left_translation_of n,s2,LO) . x)then reconsider X1 =
x as
Element of
the_subsets_of_card n,
E ;
(the_extension_of_left_translation_of n,s2,LO) . x in rng (the_extension_of_left_translation_of n,s2,LO)
by A4, A9, FUNCT_1:12;
then reconsider X2 =
(the_extension_of_left_translation_of n,s2,LO) . x as
Element of
the_subsets_of_card n,
E ;
thus (the_extension_of_left_translation_of n,(s1 * s2),LO) . x =
(LO ^ (s1 * s2)) .: X1
by A1, Def4
.=
((LO ^ s1) * (LO ^ s2)) .: X1
by Def1
.=
(LO ^ s1) .: ((LO ^ s2) .: X1)
by RELAT_1:159
.=
(LO ^ s1) .: X2
by A1, Def4
.=
(the_extension_of_left_translation_of n,s1,LO) . ((the_extension_of_left_translation_of n,s2,LO) . x)
by A1, Def4
;
verum end;
hence
H1(
s1 * s2)
= H1(
s1)
* H1(
s2)
by A6, FUNCT_1:20;
verum
end;
A10:
H1( 1_ S) = id (the_subsets_of_card n,E)
proof
set f =
the_extension_of_left_translation_of n,
(1_ S),
LO;
A11:
now let x be
set ;
( x in the_subsets_of_card n,E implies (the_extension_of_left_translation_of n,(1_ S),LO) . x = x )assume
x in the_subsets_of_card n,
E
;
(the_extension_of_left_translation_of n,(1_ S),LO) . x = xthen reconsider X =
x as
Element of
the_subsets_of_card n,
E ;
not
the_subsets_of_card n,
E is
empty
by A1, Th2;
then
X in the_subsets_of_card n,
E
;
then consider X9 being
Subset of
E such that A12:
X9 = X
and
card X9 = n
;
(the_extension_of_left_translation_of n,(1_ S),LO) . X = (LO ^ (1_ S)) .: X
by A1, Def4;
then (the_extension_of_left_translation_of n,(1_ S),LO) . x =
(id E) .: X9
by A12, Def1
.=
X9
by FUNCT_1:162
;
hence
(the_extension_of_left_translation_of n,(1_ S),LO) . x = x
by A12;
verum end;
the_extension_of_left_translation_of n,
(1_ S),
LO in Funcs (the_subsets_of_card n,E),
(the_subsets_of_card n,E)
by FUNCT_2:12;
then
ex
f9 being
Function st
(
the_extension_of_left_translation_of n,
(1_ S),
LO = f9 &
dom f9 = the_subsets_of_card n,
E &
rng f9 c= the_subsets_of_card n,
E )
by FUNCT_2:def 2;
hence
H1(
1_ S)
= id (the_subsets_of_card n,E)
by A11, FUNCT_1:34;
verum
end;
ex T being LeftOperation of S,(the_subsets_of_card n,E) st
for s being Element of S holds T . s = H1(s)
from GROUP_10:sch 1(A10, A2);
hence
ex b1 being LeftOperation of S,(the_subsets_of_card n,E) st
for s being Element of S holds b1 . s = the_extension_of_left_translation_of n,s,LO
; verum