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