for a, b, c being Element of dL-Z_2 holds (a + b) + c = a + (b + c)
by Lm22;
hence
dL-Z_2 is add-associative
; dL-Z_2 is distributive
thus
dL-Z_2 is distributive
verumproof
let a,
b,
d be
Element of
dL-Z_2;
VECTSP_1:def 7 ( a * (b + d) = (a * b) + (a * d) & (b + d) * a = (b * a) + (d * a) )
A1:
( (
a = In (
0,2) &
b = In (
0,2) &
d = In (
0,2) ) or (
a = In (
0,2) &
b = In (
0,2) &
d = In (1,2) ) or (
a = In (
0,2) &
b = In (1,2) &
d = In (
0,2) ) or (
a = In (
0,2) &
b = In (1,2) &
d = In (1,2) ) or (
a = In (1,2) &
b = In (
0,2) &
d = In (
0,2) ) or (
a = In (1,2) &
b = In (
0,2) &
d = In (1,2) ) or (
a = In (1,2) &
b = In (1,2) &
d = In (
0,2) ) or (
a = In (1,2) &
b = In (1,2) &
d = In (1,2) ) )
by Lm3, Lm4, CARD_1:50, TARSKI:def 2;
hence
a * (b + d) = (a * b) + (a * d)
by Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18;
(b + d) * a = (b * a) + (d * a)
thus
(b + d) * a = (b * a) + (d * a)
by A1, Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18;
verum
end;