let x1, x2 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 & len x1 > 0 implies LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2) )
assume A1:
( len x1 = len x2 & len x1 > 0 )
; :: thesis: LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)
then A2:
len (x1 - x2) = len x1
by EUCLID_2:7;
A3:
dom x1 = dom x2
by A1, FINSEQ_3:31;
A4:
width (LineVec2Mx (x1 - x2)) = len (x1 - x2)
by MATRIXR1:def 10;
A5:
width (LineVec2Mx x1) = len x1
by MATRIXR1:def 10;
A6:
width (LineVec2Mx x2) = len x2
by MATRIXR1:def 10;
A7:
dom (x1 - x2) = dom x1
by A2, FINSEQ_3:31;
A8:
len (LineVec2Mx (x1 - x2)) = 1
by MATRIXR1:def 10;
A9:
len (LineVec2Mx x1) = 1
by MATRIXR1:def 10;
A10:
len (LineVec2Mx x2) = 1
by MATRIXR1:def 10;
A11:
Indices (LineVec2Mx (x1 - x2)) = Indices (LineVec2Mx x1)
by A1, A4, A5, A8, A9, EUCLID_2:7, MATRIX_4:55;
A12:
Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1)
by A1, A5, A6, A9, A10, MATRIX_4:55;
A13: dom (LineVec2Mx x1) =
Seg (len (LineVec2Mx x1))
by FINSEQ_1:def 3
.=
Seg 1
by MATRIXR1:def 10
;
A14: Seg (width (LineVec2Mx x1)) =
Seg (len x1)
by MATRIXR1:def 10
.=
dom x1
by FINSEQ_1:def 3
;
for i, j being Element of 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
Element of
NAT ;
:: thesis: ( [i,j] in Indices (LineVec2Mx x1) implies (LineVec2Mx (x1 - x2)) * i,j = ((LineVec2Mx x1) * i,j) - ((LineVec2Mx x2) * i,j) )
assume A15:
[i,j] in Indices (LineVec2Mx x1)
;
:: thesis: (LineVec2Mx (x1 - x2)) * i,j = ((LineVec2Mx x1) * i,j) - ((LineVec2Mx x2) * i,j)
then A16:
(
i in Seg 1 &
j in dom x1 )
by A13, A14, ZFMISC_1:106;
then
( 1
<= i &
i <= 1 )
by FINSEQ_1:3;
then A17:
i = 1
by XXREAL_0:1;
consider p being
FinSequence of
REAL such that A18:
(
p = (LineVec2Mx (x1 - x2)) . i &
(LineVec2Mx (x1 - x2)) * i,
j = p . j )
by A11, A15, MATRIX_1:def 6;
A19:
p . j = (x1 - x2) . j
by A7, A16, A17, A18, MATRIXR1:def 10;
consider q1 being
FinSequence of
REAL such that A20:
(
q1 = (LineVec2Mx x1) . i &
(LineVec2Mx x1) * i,
j = q1 . j )
by A15, MATRIX_1:def 6;
A21:
q1 . j = x1 . j
by A16, A17, A20, MATRIXR1:def 10;
consider q2 being
FinSequence of
REAL such that A22:
(
q2 = (LineVec2Mx x2) . i &
(LineVec2Mx x2) * i,
j = q2 . j )
by A12, A15, MATRIX_1:def 6;
q2 . j = x2 . j
by A3, A16, A17, A22, MATRIXR1:def 10;
hence
(LineVec2Mx (x1 - x2)) * i,
j = ((LineVec2Mx x1) * i,j) - ((LineVec2Mx x2) * i,j)
by A1, A18, A19, A20, A21, A22, Lm1;
:: thesis: verum
end;
hence
LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)
by A1, A2, A4, A5, A6, A8, A9, A10, Th22; :: thesis: verum