let A, B be Matrix of REAL; ( len A = len B & width A = width B implies for i being Nat st 1 <= i & i <= width A holds
Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) )
assume that
A1:
len A = len B
and
A2:
width A = width B
; for i being Nat st 1 <= i & i <= width A holds
Col ((A - B),i) = (Col (A,i)) - (Col (B,i))
A3:
len (A - B) = len A
by A1, A2, Th6;
let i be Nat; ( 1 <= i & i <= width A implies Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) )
A4:
len (Col (A,i)) = len A
by MATRIX_0:def 8;
assume
( 1 <= i & i <= width A )
; Col ((A - B),i) = (Col (A,i)) - (Col (B,i))
then A5:
i in Seg (width A)
;
A6:
len (Col (B,i)) = len B
by MATRIX_0:def 8;
A7:
dom A = dom B
by A1, FINSEQ_3:29;
A8:
for j being Nat st j in dom (A - B) holds
((Col (A,i)) - (Col (B,i))) . j = (A - B) * (j,i)
proof
let j be
Nat;
( j in dom (A - B) implies ((Col (A,i)) - (Col (B,i))) . j = (A - B) * (j,i) )
assume
j in dom (A - B)
;
((Col (A,i)) - (Col (B,i))) . j = (A - B) * (j,i)
then
j in Seg (len (A - B))
by FINSEQ_1:def 3;
then A9:
j in dom A
by A3, FINSEQ_1:def 3;
then A10:
[j,i] in Indices A
by A5, ZFMISC_1:87;
reconsider j =
j as
Nat ;
(
(Col (A,i)) . j = A * (
j,
i) &
(Col (B,i)) . j = B * (
j,
i) )
by A7, A9, MATRIX_0:def 8;
then
((Col (A,i)) . j) - ((Col (B,i)) . j) = (A - B) * (
j,
i)
by A1, A2, A10, Th6;
hence
((Col (A,i)) - (Col (B,i))) . j = (A - B) * (
j,
i)
by A1, A4, A6, Lm1;
verum
end;
len ((Col (A,i)) - (Col (B,i))) = len (Col (A,i))
by A1, A4, A6, RVSUM_1:116;
hence
Col ((A - B),i) = (Col (A,i)) - (Col (B,i))
by A4, A3, A8, MATRIX_0:def 8; verum