let x1, x2 be FinSequence of REAL ; ( len x1 = len x2 & len x1 > 0 implies ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) )
assume that
A1:
len x1 = len x2
and
A2:
len x1 > 0
; ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2)
A3:
width (ColVec2Mx x1) = 1
by A2, Def9;
A4:
Seg (width (ColVec2Mx x1)) = Seg 1
by A2, Def9;
A5:
dom x1 = dom x2
by A1, FINSEQ_3:29;
A6:
len (ColVec2Mx x1) = len x1
by A2, Def9;
then A7:
dom (ColVec2Mx x1) = dom x1
by FINSEQ_3:29;
( len (ColVec2Mx x2) = len x2 & width (ColVec2Mx x2) = 1 )
by A1, A2, Def9;
then A8:
Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1)
by A1, A6, A3, MATRIX_4:55;
A9:
len (x1 + x2) = len x1
by A1, RVSUM_1:115;
then A10:
dom (x1 + x2) = dom x1
by FINSEQ_3:29;
A11:
( len (ColVec2Mx (x1 + x2)) = len (x1 + x2) & width (ColVec2Mx (x1 + x2)) = 1 )
by A2, A9, Def9;
then A12:
Indices (ColVec2Mx (x1 + x2)) = Indices (ColVec2Mx x1)
by A1, A6, A3, MATRIX_4:55, RVSUM_1:115;
for i, j being Nat st [i,j] in Indices (ColVec2Mx x1) holds
(ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j))
proof
let i,
j be
Nat;
( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) )
thus
(
[i,j] in Indices (ColVec2Mx x1) implies
(ColVec2Mx (x1 + x2)) * (
i,
j)
= ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) )
verumproof
assume A13:
[i,j] in Indices (ColVec2Mx x1)
;
(ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j))
then consider q1 being
FinSequence of
REAL such that A14:
q1 = (ColVec2Mx x1) . i
and A15:
(ColVec2Mx x1) * (
i,
j)
= q1 . j
by MATRIX_0:def 5;
j in Seg 1
by A4, A13, ZFMISC_1:87;
then
( 1
<= j &
j <= 1 )
by FINSEQ_1:1;
then A16:
j = 1
by XXREAL_0:1;
A17:
i in dom x1
by A7, A13, ZFMISC_1:87;
then
(ColVec2Mx x1) . i = <*(x1 . i)*>
by A2, Def9;
then A18:
q1 . j = x1 . i
by A16, A14, FINSEQ_1:40;
consider p being
FinSequence of
REAL such that A19:
p = (ColVec2Mx (x1 + x2)) . i
and A20:
(ColVec2Mx (x1 + x2)) * (
i,
j)
= p . j
by A12, A13, MATRIX_0:def 5;
consider q2 being
FinSequence of
REAL such that A21:
q2 = (ColVec2Mx x2) . i
and A22:
(ColVec2Mx x2) * (
i,
j)
= q2 . j
by A8, A13, MATRIX_0:def 5;
(ColVec2Mx x2) . i = <*(x2 . i)*>
by A1, A2, A5, A17, Def9;
then A23:
q2 . j = x2 . i
by A16, A21, FINSEQ_1:40;
(ColVec2Mx (x1 + x2)) . i = <*((x1 + x2) . i)*>
by A2, A9, A10, A17, Def9;
then
p . j = (x1 + x2) . i
by A16, A19, FINSEQ_1:40;
hence
(ColVec2Mx (x1 + x2)) * (
i,
j)
= ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j))
by A10, A17, A20, A15, A18, A22, A23, VALUED_1:def 1;
verum
end;
end;
hence
ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2)
by A1, A6, A11, A3, Th26, RVSUM_1:115; verum