let K be Field; for f, g being FinSequence of K st len f = len g holds
(LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)
let f, g be FinSequence of K; ( len f = len g implies (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g) )
set Lf = LineVec2Mx f;
set Lg = LineVec2Mx g;
A1:
len (LineVec2Mx f) = 1
by CARD_1:def 7;
assume A2:
len f = len g
; (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)
then reconsider F = f, G = g as Element of (len f) -tuples_on the carrier of K by FINSEQ_2:92;
A3:
width (LineVec2Mx g) = len f
by A2, MATRIX_1:23;
set FG = F + G;
set Lfg = LineVec2Mx (F + G);
A4:
( len (F + G) = len f & len (LineVec2Mx (F + G)) = 1 )
by CARD_1:def 7;
A5:
width (LineVec2Mx (F + G)) = len (F + G)
by MATRIX_1:23;
A6:
len ((LineVec2Mx f) + (LineVec2Mx g)) = len (LineVec2Mx f)
by MATRIX_3:def 3;
A7:
width ((LineVec2Mx f) + (LineVec2Mx g)) = width (LineVec2Mx f)
by MATRIX_3:def 3;
A8:
width (LineVec2Mx f) = len f
by MATRIX_1:23;
per cases
( len f = 0 or len f > 0 )
;
suppose
len f = 0
;
(LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)then
Seg (len f) = {}
;
then
for
i,
j being
Nat st
[i,j] in Indices ((LineVec2Mx f) + (LineVec2Mx g)) holds
((LineVec2Mx f) + (LineVec2Mx g)) * (
i,
j)
= (LineVec2Mx (F + G)) * (
i,
j)
by A7, A8, ZFMISC_1:90;
hence
(LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)
by A4, A1, A6, A7, A8, A5, MATRIX_1:21;
verum end; suppose A9:
len f > 0
;
(LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)A10:
(
dom (LineVec2Mx f) = Seg 1 & 1
in Seg 1 )
by A1, FINSEQ_1:def 3;
len f in Seg (len f)
by A9, FINSEQ_1:3;
then
[1,(len f)] in Indices (LineVec2Mx f)
by A8, A10, ZFMISC_1:87;
then Line (
((LineVec2Mx f) + (LineVec2Mx g)),1) =
(Line ((LineVec2Mx f),1)) + (Line ((LineVec2Mx g),1))
by A3, MATRIX_1:23, MATRIX_4:59
.=
f + (Line ((LineVec2Mx g),1))
by Th25
.=
f + g
by Th25
;
hence
(LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)
by A1, A6, Th25;
verum end;