now for c1, c2, c3 being Element of COMPLEX holds
( multcomplex . (c1,(addcomplex . (c2,c3))) = addcomplex . ((multcomplex . (c1,c2)),(multcomplex . (c1,c3))) & multcomplex . ((addcomplex . (c1,c2)),c3) = addcomplex . ((multcomplex . (c1,c3)),(multcomplex . (c2,c3))) )let c1,
c2,
c3 be
Element of
COMPLEX ;
( multcomplex . (c1,(addcomplex . (c2,c3))) = addcomplex . ((multcomplex . (c1,c2)),(multcomplex . (c1,c3))) & multcomplex . ((addcomplex . (c1,c2)),c3) = addcomplex . ((multcomplex . (c1,c3)),(multcomplex . (c2,c3))) )thus multcomplex . (
c1,
(addcomplex . (c2,c3))) =
multcomplex . (
c1,
(c2 + c3))
by BINOP_2:def 3
.=
c1 * (c2 + c3)
by BINOP_2:def 5
.=
(c1 * c2) + (c1 * c3)
.=
addcomplex . (
(c1 * c2),
(c1 * c3))
by BINOP_2:def 3
.=
addcomplex . (
(multcomplex . (c1,c2)),
(c1 * c3))
by BINOP_2:def 5
.=
addcomplex . (
(multcomplex . (c1,c2)),
(multcomplex . (c1,c3)))
by BINOP_2:def 5
;
multcomplex . ((addcomplex . (c1,c2)),c3) = addcomplex . ((multcomplex . (c1,c3)),(multcomplex . (c2,c3)))thus multcomplex . (
(addcomplex . (c1,c2)),
c3) =
multcomplex . (
(c1 + c2),
c3)
by BINOP_2:def 3
.=
(c1 + c2) * c3
by BINOP_2:def 5
.=
(c1 * c3) + (c2 * c3)
.=
addcomplex . (
(c1 * c3),
(c2 * c3))
by BINOP_2:def 3
.=
addcomplex . (
(multcomplex . (c1,c3)),
(c2 * c3))
by BINOP_2:def 5
.=
addcomplex . (
(multcomplex . (c1,c3)),
(multcomplex . (c2,c3)))
by BINOP_2:def 5
;
verum end;
hence
multcomplex is_distributive_wrt addcomplex
by BINOP_1:11; verum