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