let x1, x2 be FinSequence of REAL ; ( len x1 = len x2 implies LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2) )
A1:
( width (LineVec2Mx x1) = len x1 & len (LineVec2Mx x1) = 1 )
by MATRIXR1:def 10;
A2: Seg (width (LineVec2Mx x1)) =
Seg (len x1)
by MATRIXR1:def 10
.=
dom x1
by FINSEQ_1:def 3
;
A3: dom (LineVec2Mx x1) =
Seg (len (LineVec2Mx x1))
by FINSEQ_1:def 3
.=
Seg 1
by MATRIXR1:def 10
;
assume A4:
len x1 = len x2
; LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)
then A5:
dom x1 = dom x2
by FINSEQ_3:29;
A6:
( width (LineVec2Mx x2) = len x2 & len (LineVec2Mx x2) = 1 )
by MATRIXR1:def 10;
then A7:
Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1)
by A4, A1, MATRIX_4:55;
A8:
len (x1 - x2) = len x1
by A4, RVSUM_1:116;
then A9:
dom (x1 - x2) = dom x1
by FINSEQ_3:29;
A10:
( width (LineVec2Mx (x1 - x2)) = len (x1 - x2) & len (LineVec2Mx (x1 - x2)) = 1 )
by MATRIXR1:def 10;
then A11:
Indices (LineVec2Mx (x1 - x2)) = Indices (LineVec2Mx x1)
by A4, A1, MATRIX_4:55, RVSUM_1:116;
for i, j being Nat st [i,j] in Indices (LineVec2Mx x1) holds
(LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (LineVec2Mx x1) implies (LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j)) )
assume A12:
[i,j] in Indices (LineVec2Mx x1)
;
(LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j))
then consider q1 being
FinSequence of
REAL such that
q1 = (LineVec2Mx x1) . i
and A13:
(LineVec2Mx x1) * (
i,
j)
= q1 . j
by MATRIX_0:def 5;
i in Seg 1
by A3, A12, ZFMISC_1:87;
then
( 1
<= i &
i <= 1 )
by FINSEQ_1:1;
then A14:
i = 1
by XXREAL_0:1;
A15:
j in dom x1
by A2, A12, ZFMISC_1:87;
then A16:
q1 . j = x1 . j
by A14, A13, MATRIXR1:def 10;
consider p being
FinSequence of
REAL such that
p = (LineVec2Mx (x1 - x2)) . i
and A17:
(LineVec2Mx (x1 - x2)) * (
i,
j)
= p . j
by A11, A12, MATRIX_0:def 5;
consider q2 being
FinSequence of
REAL such that
q2 = (LineVec2Mx x2) . i
and A18:
(LineVec2Mx x2) * (
i,
j)
= q2 . j
by A7, A12, MATRIX_0:def 5;
A19:
q2 . j = x2 . j
by A5, A15, A14, A18, MATRIXR1:def 10;
p . j = (x1 - x2) . j
by A9, A15, A14, A17, MATRIXR1:def 10;
hence
(LineVec2Mx (x1 - x2)) * (
i,
j)
= ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j))
by A4, A17, A13, A16, A18, A19, Lm1;
verum
end;
hence
LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)
by A4, A8, A10, A1, A6, Th22; verum