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