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_1:def 8;
A5:
len (Line B,i) = width B
by MATRIX_1:def 8;
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:27;
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
Element of
NAT by ORDINAL1:def 13;
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
Element of
NAT by ORDINAL1:def 13;
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:106;
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_1:def 8;
hence
((Line A,i) - (Line B,i)) . j = (A - B) * i,
j
by A2, A11, A10, A8, MATRIX_1:def 8;
verum
end;
len ((Line A,i) - (Line B,i)) = len (Line A,i)
by A2, A4, A5, RVSUM_1:146;
hence
Line (A - B),i = (Line A,i) - (Line B,i)
by A4, A3, A7, MATRIX_1:def 8; verum