let K be Field; 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; 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; 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; 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; 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; 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 for x being object st x in the carrier of V1 holds
(Mx2Tran ((a * A),b1,B2)) . x = (a * (Mx2Tran (A,b1,B2))) . xlet x be
object ;
( 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
;
(Mx2Tran ((a * A),b1,B2)) . x = (a * (Mx2Tran (A,b1,B2))) . xthen 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 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;
( 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))
;
(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
;
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
;
verum end;
hence
a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)
by FUNCT_2:12; verum