let A be non empty set ; for o, o9 being BinOp of A st o9 is commutative holds
( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
let o, o9 be BinOp of A; ( o9 is commutative implies ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )
assume A1:
o9 is commutative
; ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
( ( for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
proof
thus
( ( for
a,
b,
c being
Element of
A holds
(
o9 . (
a,
(o . (b,c)))
= o . (
(o9 . (a,b)),
(o9 . (a,c))) &
o9 . (
(o . (a,b)),
c)
= o . (
(o9 . (a,c)),
(o9 . (b,c))) ) ) implies for
a,
b,
c being
Element of
A holds
o9 . (
(o . (a,b)),
c)
= o . (
(o9 . (a,c)),
(o9 . (b,c))) )
;
( ( for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) implies for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )
assume A2:
for
a,
b,
c being
Element of
A holds
o9 . (
(o . (a,b)),
c)
= o . (
(o9 . (a,c)),
(o9 . (b,c)))
;
for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
let a,
b,
c be
Element of
A;
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
thus o9 . (
a,
(o . (b,c))) =
o9 . (
(o . (b,c)),
a)
by A1
.=
o . (
(o9 . (b,a)),
(o9 . (c,a)))
by A2
.=
o . (
(o9 . (a,b)),
(o9 . (c,a)))
by A1
.=
o . (
(o9 . (a,b)),
(o9 . (a,c)))
by A1
;
o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)))
thus
o9 . (
(o . (a,b)),
c)
= o . (
(o9 . (a,c)),
(o9 . (b,c)))
by A2;
verum
end;
hence
( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
by Th11; verum