let D be non empty set ; :: thesis: for I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g))
let I, J be non empty set ; :: thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g))
let F, G be BinOp of D; :: thesis: for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g))
let f be Function of I,D; :: thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g))
let g be Function of J,D; :: thesis: for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g))
let X be Element of Fin I; :: thesis: for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g))
let Y be Element of Fin J; :: thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g)) )
assume A1:
( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F )
; :: thesis: for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g))
now let x be
Element of
I;
:: thesis: for Y being Element of Fin J holds S1[Y]defpred S1[
Element of
Fin J]
means F $$ [:{.x.},$1:],
(G * f,g) = F $$ {.x.},
(G [:] f,(F $$ $1,g));
A2:
S1[
{}. J]
proof
reconsider T =
{}. [:I,J:] as
Element of
Fin [:I,J:] ;
A3:
T = [:{x},({}. J):]
by ZFMISC_1:113;
A4:
dom f = I
by FUNCT_2:def 1;
set z =
the_unity_wrt F;
dom <:f,((dom f) --> (the_unity_wrt F)):> =
(dom f) /\ (dom ((dom f) --> (the_unity_wrt F)))
by FUNCT_3:def 8
.=
(dom f) /\ (dom f)
by FUNCOP_1:19
.=
dom f
;
then A5:
x in dom <:f,((dom f) --> (the_unity_wrt F)):>
by A4;
A6:
rng f c= D
by RELAT_1:def 19;
A7:
{(the_unity_wrt F)} c= D
by ZFMISC_1:37;
rng ((dom f) --> (the_unity_wrt F)) c= {(the_unity_wrt F)}
by FUNCOP_1:19;
then A8:
rng ((dom f) --> (the_unity_wrt F)) c= D
by A7, XBOOLE_1:1;
A9:
dom G = [:D,D:]
by FUNCT_2:def 1;
A10:
rng <:f,((dom f) --> (the_unity_wrt F)):> c= [:(rng f),(rng ((dom f) --> (the_unity_wrt F))):]
by FUNCT_3:71;
[:(rng f),(rng ((dom f) --> (the_unity_wrt F))):] c= [:D,D:]
by A6, A8, ZFMISC_1:119;
then
x in dom (G * <:f,((dom f) --> (the_unity_wrt F)):>)
by A5, A9, A10, RELAT_1:46, XBOOLE_1:1;
then A11:
x in dom (G [:] f,(the_unity_wrt F))
by FUNCOP_1:def 4;
F $$ {.x.},
(G [:] f,(F $$ ({}. J),g)) =
F $$ {.x.},
(G [:] f,(the_unity_wrt F))
by A1, SETWISEO:40
.=
(G [:] f,(the_unity_wrt F)) . x
by A1, SETWISEO:26
.=
G . (f . x),
(the_unity_wrt F)
by A11, FUNCOP_1:35
.=
the_unity_wrt F
by A1, FINSEQOP:70
;
hence
S1[
{}. J]
by A1, A3, SETWISEO:40;
:: thesis: verum
end; A12:
for
Y1 being
Element of
Fin J for
y being
Element of
J st
S1[
Y1] holds
S1[
Y1 \/ {.y.}]
proof
let Y1 be
Element of
Fin J;
:: thesis: for y being Element of J st S1[Y1] holds
S1[Y1 \/ {.y.}]let y be
Element of
J;
:: thesis: ( S1[Y1] implies S1[Y1 \/ {.y.}] )
assume A13:
F $$ [:{.x.},Y1:],
(G * f,g) = F $$ {.x.},
(G [:] f,(F $$ Y1,g))
;
:: thesis: S1[Y1 \/ {.y.}]
reconsider s =
{.y.} as
Element of
Fin J ;
per cases
( y in Y1 or not y in Y1 )
;
suppose
not
y in Y1
;
:: thesis: S1[Y1 \/ {.y.}]then A14:
Y1 misses {y}
by ZFMISC_1:56;
then A15:
[:{x},Y1:] misses [:{x},s:]
by ZFMISC_1:127;
thus F $$ [:{.x.},(Y1 \/ {.y.}):],
(G * f,g) =
F $$ ([:{.x.},Y1:] \/ [:{.x.},s:]),
(G * f,g)
by ZFMISC_1:120
.=
F . (F $$ [:{.x.},Y1:],(G * f,g)),
(F $$ [:{.x.},s:],(G * f,g))
by A1, A15, SETWOP_2:6
.=
F . (F $$ {.x.},(G [:] f,(F $$ Y1,g))),
(F $$ {.x.},(G [:] f,(F $$ s,g)))
by A1, A13, Th26
.=
F $$ {.x.},
(F .: (G [:] f,(F $$ Y1,g)),(G [:] f,(F $$ s,g)))
by A1, SETWOP_2:12
.=
F $$ {.x.},
(G [:] f,(F . (F $$ Y1,g),(F $$ s,g)))
by A1, FINSEQOP:37
.=
F $$ {.x.},
(G [:] f,(F $$ (Y1 \/ {.y.}),g))
by A1, A14, SETWOP_2:6
;
:: thesis: verum end;
end; thus
for
Y being
Element of
Fin J holds
S1[
Y]
from SETWISEO:sch 4(A2, A12); :: thesis: verum end;
hence
for x being Element of I holds F $$ [:{.x.},Y:],(G * f,g) = F $$ {.x.},(G [:] f,(F $$ Y,g))
; :: thesis: verum