let K be Field; :: thesis: for a being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)
let a be Element of K; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)
let B2 be FinSequence of V2; :: thesis: for A being Matrix of len b1, len B2,K holds a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)
let A be Matrix of len b1, len B2,K; :: thesis: a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)
set aA = a * A;
set aM = Mx2Tran ((a * A),b1,B2);
set M = Mx2Tran (A,b1,B2);
now :: thesis: for x being object st x in the carrier of V1 holds
(Mx2Tran ((a * A),b1,B2)) . x = (a * (Mx2Tran (A,b1,B2))) . x
let x be object ; :: thesis: ( x in the carrier of V1 implies (Mx2Tran ((a * A),b1,B2)) . x = (a * (Mx2Tran (A,b1,B2))) . x )
assume x in the carrier of V1 ; :: thesis: (Mx2Tran ((a * A),b1,B2)) . x = (a * (Mx2Tran (A,b1,B2))) . x
then reconsider v = x as Element of V1 ;
set L = LineVec2Mx (v |-- b1);
set amA = lmlt ((a * (Line (((LineVec2Mx (v |-- b1)) * A),1))),B2);
set mA = lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2);
A1: ( width (LineVec2Mx (v |-- b1)) = len (v |-- b1) & len (v |-- b1) = len b1 ) by MATRIX_0:23, MATRLIN:def 7;
A2: len A = len b1 by MATRIX_0:def 2;
len (LineVec2Mx (v |-- b1)) = 1 by MATRIX_0:23;
then A3: len ((LineVec2Mx (v |-- b1)) * A) = 1 by A1, A2, MATRIX_3:def 4;
A4: dom (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) = (dom (Line (((LineVec2Mx (v |-- b1)) * A),1))) /\ (dom B2) by Lm1;
len (a * (Line (((LineVec2Mx (v |-- b1)) * A),1))) = len (Line (((LineVec2Mx (v |-- b1)) * A),1)) by MATRIXR1:16;
then A5: dom (a * (Line (((LineVec2Mx (v |-- b1)) * A),1))) = dom (Line (((LineVec2Mx (v |-- b1)) * A),1)) by FINSEQ_3:29;
A6: dom (lmlt ((a * (Line (((LineVec2Mx (v |-- b1)) * A),1))),B2)) = (dom (a * (Line (((LineVec2Mx (v |-- b1)) * A),1)))) /\ (dom B2) by Lm1;
then A7: len (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) = len (lmlt ((a * (Line (((LineVec2Mx (v |-- b1)) * A),1))),B2)) by A5, A4, FINSEQ_3:29;
A8: now :: thesis: for k being Nat st k in dom (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) holds
(lmlt ((a * (Line (((LineVec2Mx (v |-- b1)) * A),1))),B2)) . k = a * ((lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) /. k)
let k be Nat; :: thesis: ( k in dom (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) implies (lmlt ((a * (Line (((LineVec2Mx (v |-- b1)) * A),1))),B2)) . k = a * ((lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) /. k) )
assume A9: k in dom (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) ; :: thesis: (lmlt ((a * (Line (((LineVec2Mx (v |-- b1)) * A),1))),B2)) . k = a * ((lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) /. k)
A10: (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) . k = (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) /. k by A9, PARTFUN1:def 6;
k in dom (Line (((LineVec2Mx (v |-- b1)) * A),1)) by A4, A9, XBOOLE_0:def 4;
then A11: (Line (((LineVec2Mx (v |-- b1)) * A),1)) . k = (Line (((LineVec2Mx (v |-- b1)) * A),1)) /. k by PARTFUN1:def 6;
k in dom B2 by A4, A9, XBOOLE_0:def 4;
then A12: B2 . k = B2 /. k by PARTFUN1:def 6;
k in dom (a * (Line (((LineVec2Mx (v |-- b1)) * A),1))) by A5, A4, A9, XBOOLE_0:def 4;
then (a * (Line (((LineVec2Mx (v |-- b1)) * A),1))) . k = a * ((Line (((LineVec2Mx (v |-- b1)) * A),1)) /. k) by A11, FVSUM_1:50;
hence (lmlt ((a * (Line (((LineVec2Mx (v |-- b1)) * A),1))),B2)) . k = (a * ((Line (((LineVec2Mx (v |-- b1)) * A),1)) /. k)) * (B2 /. k) by A6, A5, A4, A9, A12, FUNCOP_1:22
.= a * (((Line (((LineVec2Mx (v |-- b1)) * A),1)) /. k) * (B2 /. k)) by VECTSP_1:def 16
.= a * ((lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2)) /. k) by A9, A11, A12, A10, FUNCOP_1:22 ;
:: thesis: verum
end;
thus (Mx2Tran ((a * A),b1,B2)) . x = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * (a * A)),1)),B2)) by Def3
.= Sum (lmlt ((Line ((a * ((LineVec2Mx (v |-- b1)) * A)),1)),B2)) by A1, A2, MATRIXR1:22
.= Sum (lmlt ((a * (Line (((LineVec2Mx (v |-- b1)) * A),1))),B2)) by A3, MATRIXR1:20
.= a * (Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * A),1)),B2))) by A7, A8, RLVECT_2:67
.= a * ((Mx2Tran (A,b1,B2)) . v) by Def3
.= (a * (Mx2Tran (A,b1,B2))) . x by MATRLIN:def 4 ; :: thesis: verum
end;
hence a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2) by FUNCT_2:12; :: thesis: verum