let n, m be Nat; for f1, f2 being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
let f1, f2 be n -element real-valued FinSequence; for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
let M be Matrix of n,m,F_Real; (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
set f12 = f1 + f2;
set T = Mx2Tran M;
per cases
( n <> 0 or n = 0 )
;
suppose A1:
n <> 0
;
(Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)per cases
( m = 0 or m > 0 )
;
suppose
m > 0
;
(Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)then A3:
m >= 1
by NAT_1:14;
A4:
len M = n
by A1, MATRIX13:1;
set L2 =
LineVec2Mx (@ f2);
set L1 =
LineVec2Mx (@ f1);
A5:
len (LineVec2Mx (@ f2)) = 1
by MATRIX13:1;
A6:
len f2 = n
by CARD_1:def 7;
then A7:
width (LineVec2Mx (@ f2)) = n
by MATRIX13:1;
A8:
width M = m
by A1, MATRIX13:1;
then A9:
width ((LineVec2Mx (@ f2)) * M) = m
by A7, A4, MATRIX_3:def 4;
A10:
len f1 = n
by CARD_1:def 7;
then A11:
width (LineVec2Mx (@ f1)) = n
by MATRIX13:1;
then A12:
width ((LineVec2Mx (@ f1)) * M) = m
by A4, A8, MATRIX_3:def 4;
A13:
len (LineVec2Mx (@ f1)) = 1
by MATRIX13:1;
then
len ((LineVec2Mx (@ f1)) * M) = 1
by A11, A4, MATRIX_3:def 4;
then A14:
[1,1] in Indices ((LineVec2Mx (@ f1)) * M)
by A12, A3, MATRIX_0:30;
A15:
(
@ ((Mx2Tran M) . f1) = Line (
((LineVec2Mx (@ f1)) * M),1) &
@ ((Mx2Tran M) . f2) = Line (
((LineVec2Mx (@ f2)) * M),1) )
by A1, Def3;
@ (f1 + f2) = (@ f1) + (@ f2)
by RVSUM_1:def 4;
then (LineVec2Mx (@ (f1 + f2))) * M =
((LineVec2Mx (@ f1)) + (LineVec2Mx (@ f2))) * M
by A10, A6, MATRIX15:27
.=
((LineVec2Mx (@ f1)) * M) + ((LineVec2Mx (@ f2)) * M)
by A1, A13, A5, A11, A7, A4, MATRIX_4:63
;
hence (Mx2Tran M) . (f1 + f2) =
Line (
(((LineVec2Mx (@ f1)) * M) + ((LineVec2Mx (@ f2)) * M)),1)
by A1, Def3
.=
(Line (((LineVec2Mx (@ f1)) * M),1)) + (Line (((LineVec2Mx (@ f2)) * M),1))
by A12, A9, A14, MATRIX_4:59
.=
((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
by A15, RVSUM_1:def 4
;
verum end; end; end; end;