let i be Nat; for K being Field
for j being Nat
for A, B being Matrix of K st width A = width B & ex j being Nat st [i,j] in Indices A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let K be Field; for j being Nat
for A, B being Matrix of K st width A = width B & ex j being Nat st [i,j] in Indices A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let j be Nat; for A, B being Matrix of K st width A = width B & ex j being Nat st [i,j] in Indices A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let A, B be Matrix of K; ( width A = width B & ex j being Nat st [i,j] in Indices A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
assume that
A1:
width A = width B
and
A2:
ex j being Nat st [i,j] in Indices A
; Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
reconsider wA = width A as Element of NAT by ORDINAL1:def 12;
reconsider a = Line (A,i), b = Line (B,i) as Element of wA -tuples_on the carrier of K by A1;
A3:
width (A + B) = width A
by MATRIX_3:def 3;
i in dom A
by A2, ZFMISC_1:87;
then A4:
i in Seg (len A)
by FINSEQ_1:def 3;
A5:
len (A + B) = len A
by MATRIX_3:def 3;
then A6:
Indices (A + B) = Indices A
by A3, Th55;
A7:
for k being Nat st 1 <= k & k <= len (Line ((A + B),i)) holds
(Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k
proof
let k be
Nat;
( 1 <= k & k <= len (Line ((A + B),i)) implies (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k )
assume A8:
( 1
<= k &
k <= len (Line ((A + B),i)) )
;
(Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k
A9:
len (Line ((A + B),i)) = width A
by A3, MATRIX_0:def 7;
then A10:
k in Seg (width (A + B))
by A3, A8, FINSEQ_1:1;
len (Line (B,i)) = width B
by MATRIX_0:def 7;
then
k in Seg (len (Line (B,i)))
by A1, A8, A9, FINSEQ_1:1;
then
k in dom (Line (B,i))
by FINSEQ_1:def 3;
then reconsider e =
(Line (B,i)) . k as
Element of
K by FINSEQ_2:11;
i in dom (A + B)
by A5, A4, FINSEQ_1:def 3;
then A11:
[i,k] in Indices (A + B)
by A10, ZFMISC_1:87;
A12:
(Line ((A + B),i)) . k =
(A + B) * (
i,
k)
by A10, MATRIX_0:def 7
.=
(A * (i,k)) + (B * (i,k))
by A6, A11, MATRIX_3:def 3
;
A13:
len (Line (A,i)) = width A
by MATRIX_0:def 7;
then A14:
k in Seg (len (Line (A,i)))
by A8, A9, FINSEQ_1:1;
then
k in dom (Line (A,i))
by FINSEQ_1:def 3;
then reconsider d =
(Line (A,i)) . k as
Element of
K by FINSEQ_2:11;
len ((Line (A,i)) + (Line (B,i))) =
len (a + b)
.=
width A
by CARD_1:def 7
.=
len (Line (A,i))
by CARD_1:def 7
;
then
k in dom ((Line (A,i)) + (Line (B,i)))
by A14, FINSEQ_1:def 3;
then A15:
((Line (A,i)) + (Line (B,i))) . k = d + e
by FVSUM_1:17;
(Line (A,i)) . k = A * (
i,
k)
by A13, A14, MATRIX_0:def 7;
hence
(Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k
by A1, A13, A12, A14, A15, MATRIX_0:def 7;
verum
end;
A16: len ((Line (A,i)) + (Line (B,i))) =
len (a + b)
.=
width A
by CARD_1:def 7
;
len (Line ((A + B),i)) = width A
by A3, MATRIX_0:def 7;
hence
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
by A16, A7, FINSEQ_1:14; verum