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