let A, B be Matrix of REAL ; :: thesis: ( 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 A1:
( len A = len B & width A = width B )
; :: thesis: for i being Nat st 1 <= i & i <= len A holds
Line (A - B),i = (Line A,i) - (Line B,i)
let i be Nat; :: thesis: ( 1 <= i & i <= len A implies Line (A - B),i = (Line A,i) - (Line B,i) )
assume
( 1 <= i & i <= len A )
; :: thesis: Line (A - B),i = (Line A,i) - (Line B,i)
then A2:
i in dom A
by FINSEQ_3:27;
A3:
len (Line A,i) = width A
by MATRIX_1:def 8;
A4:
len (Line B,i) = width B
by MATRIX_1:def 8;
A5:
( len (A - B) = len A & width (A - B) = width A )
by A1, Th6;
A6:
len ((Line A,i) - (Line B,i)) = len (Line A,i)
by A1, A3, A4, EUCLID_2:7;
for j being Nat st j in Seg (width (A - B)) holds
((Line A,i) - (Line B,i)) . j = (A - B) * i,j
proof
let j be
Nat;
:: thesis: ( j in Seg (width (A - B)) implies ((Line A,i) - (Line B,i)) . j = (A - B) * i,j )
assume A7:
j in Seg (width (A - B))
;
:: thesis: ((Line A,i) - (Line B,i)) . j = (A - B) * i,j
then A8:
j in Seg (width A)
by A1, Th6;
A9:
[i,j] in Indices A
by A2, A5, A7, ZFMISC_1:106;
A10:
(Line A,i) . j = A * i,
j
by A8, MATRIX_1:def 8;
reconsider i2 =
i as
Element of
NAT by ORDINAL1:def 13;
reconsider j2 =
j as
Element of
NAT by ORDINAL1:def 13;
A11:
(A - B) * i2,
j2 = (A * i2,j2) - (B * i2,j2)
by A1, A9, Th6;
((Line A,i2) - (Line B,i2)) . j = ((Line A,i2) . j2) - ((Line B,i2) . j2)
by A1, A3, A4, Lm1;
hence
((Line A,i) - (Line B,i)) . j = (A - B) * i,
j
by A1, A8, A10, A11, MATRIX_1:def 8;
:: thesis: verum
end;
hence
Line (A - B),i = (Line A,i) - (Line B,i)
by A3, A5, A6, MATRIX_1:def 8; :: thesis: verum