let K be Field; for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds
(B + C) * A = (B * A) + (C * A)
let A, B, C be Matrix of K; ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 implies (B + C) * A = (B * A) + (C * A) )
assume that
A1:
len B = len C
and
A2:
width B = width C
and
A3:
len A = width B
and
A4:
len B > 0
and
A5:
len A > 0
; (B + C) * A = (B * A) + (C * A)
A6:
width (B + C) = width B
by MATRIX_3:def 3;
then A7:
width ((B + C) * A) = width A
by A3, MATRIX_3:def 4;
len (B + C) = len B
by MATRIX_3:def 3;
then A8:
len ((B + C) * A) = len B
by A3, A6, MATRIX_3:def 4;
then reconsider M1 = (B + C) * A as Matrix of len B, width A,K by A4, A7, MATRIX_0:20;
A9:
len (B * A) = len B
by A3, MATRIX_3:def 4;
A10:
width (B * A) = width A
by A3, MATRIX_3:def 4;
then A11:
Indices M1 = Indices (B * A)
by A8, A7, A9, Th55;
A12:
( len ((B * A) + (C * A)) = len (B * A) & width ((B * A) + (C * A)) = width (B * A) )
by MATRIX_3:def 3;
then reconsider M2 = (B * A) + (C * A) as Matrix of len B, width A,K by A4, A9, A10, MATRIX_0:20;
( len (C * A) = len C & width (C * A) = width A )
by A2, A3, MATRIX_3:def 4;
then A13:
Indices M1 = Indices (C * A)
by A1, A8, A7, Th55;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
len (Col (A,j)) = width B
by A3, MATRIX_0:def 8;
then A14:
len (Col (A,j)) = len (Line (B,i))
by MATRIX_0:def 7;
reconsider q1 =
Line (
B,
i),
q2 =
Line (
C,
i),
q3 =
Col (
A,
j) as
Element of
(len A) -tuples_on the
carrier of
K by A2, A3;
A15:
len (mlt ((Line (B,i)),(Col (A,j)))) =
len (mlt (q1,q3))
.=
len A
by CARD_1:def 7
.=
len (mlt (q2,q3))
by CARD_1:def 7
.=
len (mlt ((Line (C,i)),(Col (A,j))))
;
1
+ 0 <= width B
by A3, A5, NAT_1:13;
then A16:
1
in Seg (width B)
by FINSEQ_1:1;
len (Col (A,j)) = width C
by A2, A3, MATRIX_0:def 8;
then A17:
len (Col (A,j)) = len (Line (C,i))
by MATRIX_0:def 7;
assume A18:
[i,j] in Indices M1
;
M1 * (i,j) = M2 * (i,j)
then A19:
M2 * (
i,
j) =
((B * A) * (i,j)) + ((C * A) * (i,j))
by A11, MATRIX_3:def 3
.=
((Line (B,i)) "*" (Col (A,j))) + ((C * A) * (i,j))
by A3, A11, A18, MATRIX_3:def 4
.=
((Line (B,i)) "*" (Col (A,j))) + ((Line (C,i)) "*" (Col (A,j)))
by A2, A3, A13, A18, MATRIX_3:def 4
.=
((Line (B,i)) "*" (Col (A,j))) + (Sum (mlt ((Line (C,i)),(Col (A,j)))))
by FVSUM_1:def 9
.=
(Sum (mlt ((Line (B,i)),(Col (A,j))))) + (Sum (mlt ((Line (C,i)),(Col (A,j)))))
by FVSUM_1:def 9
;
i in dom (B * A)
by A11, A18, ZFMISC_1:87;
then
i in Seg (len B)
by A9, FINSEQ_1:def 3;
then
i in dom B
by FINSEQ_1:def 3;
then A20:
[i,1] in Indices B
by A16, ZFMISC_1:87;
M1 * (
i,
j) =
(Line ((B + C),i)) "*" (Col (A,j))
by A3, A6, A18, MATRIX_3:def 4
.=
Sum (mlt ((Line ((B + C),i)),(Col (A,j))))
by FVSUM_1:def 9
.=
Sum (mlt (((Line (B,i)) + (Line (C,i))),(Col (A,j))))
by A2, A20, Th59
.=
Sum ((mlt ((Line (B,i)),(Col (A,j)))) + (mlt ((Line (C,i)),(Col (A,j)))))
by A14, A17, Th56
.=
(Sum (mlt ((Line (B,i)),(Col (A,j))))) + (Sum (mlt ((Line (C,i)),(Col (A,j)))))
by A15, Th61
;
hence
M1 * (
i,
j)
= M2 * (
i,
j)
by A19;
verum
end;
hence
(B + C) * A = (B * A) + (C * A)
by A8, A7, A9, A10, A12, MATRIX_0:21; verum