let x1, x2 be FinSequence of REAL ; ( len x1 = len x2 implies LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) )
assume A1:
len x1 = len x2
; LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2)
then A2:
dom x1 = dom x2
by FINSEQ_3:29;
len (x1 + x2) = len x1
by A1, RVSUM_1:115;
then A3:
dom (x1 + x2) = dom x1
by FINSEQ_3:29;
A4:
( width (LineVec2Mx x1) = len x1 & len (LineVec2Mx x1) = 1 )
by Def10;
( width (LineVec2Mx x2) = len x2 & len (LineVec2Mx x2) = 1 )
by Def10;
then A5:
Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1)
by A1, A4, MATRIX_4:55;
A6: Seg (width (LineVec2Mx x1)) =
Seg (len x1)
by Def10
.=
dom x1
by FINSEQ_1:def 3
;
A7: dom (LineVec2Mx x1) =
Seg (len (LineVec2Mx x1))
by FINSEQ_1:def 3
.=
Seg 1
by Def10
;
A8:
( width (LineVec2Mx (x1 + x2)) = len (x1 + x2) & len (LineVec2Mx (x1 + x2)) = 1 )
by Def10;
then A9:
Indices (LineVec2Mx (x1 + x2)) = Indices (LineVec2Mx x1)
by A1, A4, MATRIX_4:55, RVSUM_1:115;
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 A10:
[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 A11:
(LineVec2Mx x1) * (
i,
j)
= q1 . j
by MATRIX_0:def 5;
consider p being
FinSequence of
REAL such that
p = (LineVec2Mx (x1 + x2)) . i
and A12:
(LineVec2Mx (x1 + x2)) * (
i,
j)
= p . j
by A9, A10, MATRIX_0:def 5;
consider q2 being
FinSequence of
REAL such that
q2 = (LineVec2Mx x2) . i
and A13:
(LineVec2Mx x2) * (
i,
j)
= q2 . j
by A5, A10, MATRIX_0:def 5;
A14:
j in dom x1
by A6, A10, ZFMISC_1:87;
i in Seg 1
by A7, A10, ZFMISC_1:87;
then
( 1
<= i &
i <= 1 )
by FINSEQ_1:1;
then A15:
i = 1
by XXREAL_0:1;
then A16:
q1 . j = x1 . j
by A14, A11, Def10;
A17:
q2 . j = x2 . j
by A2, A14, A15, A13, Def10;
p . j = (x1 + x2) . j
by A3, A14, A15, A12, Def10;
hence
(LineVec2Mx (x1 + x2)) * (
i,
j)
= ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j))
by A3, A14, A12, A11, A16, A13, A17, VALUED_1:def 1;
verum
end;
hence
LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2)
by A1, A8, A4, Th26, RVSUM_1:115; verum