let D be non empty set ; for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
let S be non empty Subset of D; for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
let f1, f2 be BinOp of D; for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
let g1, g2 be BinOp of S; ( g1 = f1 || S & g2 = f2 || S implies ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) )
assume that
A1:
g1 = f1 || S
and
A2:
g2 = f2 || S
; ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
thus
( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 )
( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 )proof
assume A3:
for
a,
b,
c being
Element of
D holds
f1 . (
a,
(f2 . (b,c)))
= f2 . (
(f1 . (a,b)),
(f1 . (a,c)))
;
BINOP_1:def 18 g1 is_left_distributive_wrt g2
let a,
b,
c be
Element of
S;
BINOP_1:def 18 g1 . (a,(g2 . (b,c))) = g2 . ((g1 . (a,b)),(g1 . (a,c)))
set ab =
g1 . (
a,
b);
set ac =
g1 . (
a,
c);
set bc =
g2 . (
b,
c);
reconsider a9 =
a,
b9 =
b,
c9 =
c as
Element of
D ;
A4:
(
f2 . [b9,c9] = f2 . (
b9,
c9) &
f1 . [a9,b9] = f1 . (
a9,
b9) )
;
A5:
(
f1 . [a9,c9] = f1 . (
a9,
c9) &
f1 . [a,(g2 . (b,c))] = f1 . (
a,
(g2 . (b,c))) )
;
dom g2 = [:S,S:]
by FUNCT_2:def 1;
then A6:
(
g2 . [b,c] = f2 . [b,c] &
g2 . [(g1 . (a,b)),(g1 . (a,c))] = f2 . [(g1 . (a,b)),(g1 . (a,c))] )
by A2, FUNCT_1:47;
A7:
f2 . [(g1 . (a,b)),(g1 . (a,c))] = f2 . (
(g1 . (a,b)),
(g1 . (a,c)))
;
A8:
dom g1 = [:S,S:]
by FUNCT_2:def 1;
then A9:
g1 . [a,(g2 . (b,c))] = f1 . [a,(g2 . (b,c))]
by A1, FUNCT_1:47;
(
g1 . [a,b] = f1 . [a,b] &
g1 . [a,c] = f1 . [a,c] )
by A1, A8, FUNCT_1:47;
hence
g1 . (
a,
(g2 . (b,c)))
= g2 . (
(g1 . (a,b)),
(g1 . (a,c)))
by A3, A4, A9, A5, A6, A7;
verum
end;
assume A10:
for a, b, c being Element of D holds f1 . ((f2 . (a,b)),c) = f2 . ((f1 . (a,c)),(f1 . (b,c)))
; BINOP_1:def 19 g1 is_right_distributive_wrt g2
let a, b, c be Element of S; BINOP_1:def 19 g1 . ((g2 . (a,b)),c) = g2 . ((g1 . (a,c)),(g1 . (b,c)))
set ab = g2 . (a,b);
set ac = g1 . (a,c);
set bc = g1 . (b,c);
A11:
f2 . [(g1 . (a,c)),(g1 . (b,c))] = f2 . ((g1 . (a,c)),(g1 . (b,c)))
;
A12:
dom g1 = [:S,S:]
by FUNCT_2:def 1;
then A13:
g1 . [(g2 . (a,b)),c] = f1 . [(g2 . (a,b)),c]
by A1, FUNCT_1:47;
dom g2 = [:S,S:]
by FUNCT_2:def 1;
then A14:
( g2 . [a,b] = f2 . [a,b] & g2 . [(g1 . (a,c)),(g1 . (b,c))] = f2 . [(g1 . (a,c)),(g1 . (b,c))] )
by A2, FUNCT_1:47;
reconsider a9 = a, b9 = b, c9 = c as Element of D ;
A15:
( f1 . [b9,c9] = f1 . (b9,c9) & f2 . [a9,b9] = f2 . (a9,b9) )
;
A16:
( f1 . [a9,c9] = f1 . (a9,c9) & f1 . [(g2 . (a,b)),c] = f1 . ((g2 . (a,b)),c) )
;
( g1 . [b,c] = f1 . [b,c] & g1 . [a,c] = f1 . [a,c] )
by A1, A12, FUNCT_1:47;
hence
g1 . ((g2 . (a,b)),c) = g2 . ((g1 . (a,c)),(g1 . (b,c)))
by A10, A15, A13, A16, A14, A11; verum