let K be Field; for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
let V1, V2 be finite-dimensional VectSp of K; for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
let f be Function of V1,V2; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2
for v1 being Element of V1
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
let b2 be OrdBasis of V2; for v1 being Element of V1
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
let v1 be Element of V1; for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
let M be OrdBasis of (len b2) -VectSp_over K; ( M = MX2FinS (1. (K,(len b2))) implies for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2 )
assume A1:
M = MX2FinS (1. (K,(len b2)))
; for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
let A be Matrix of len b1, len M,K; ( A = AutMt (f,b1,b2) & f is additive & f is homogeneous implies (Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2 )
assume that
A2:
A = AutMt (f,b1,b2)
and
A3:
( f is additive & f is homogeneous )
; (Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
reconsider f9 = f as linear-transformation of V1,V2 by A3;
set MM = Mx2Tran (A,b1,M);
per cases
( len b1 = 0 or len b1 > 0 )
;
suppose A5:
len b1 > 0
;
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2then LineVec2Mx (((Mx2Tran (A,b1,M)) . v1) |-- M) =
(LineVec2Mx (v1 |-- b1)) * A
by Th32
.=
LineVec2Mx ((f . v1) |-- b2)
by A2, A3, A5, Th31
;
hence (f . v1) |-- b2 =
Line (
(LineVec2Mx (((Mx2Tran (A,b1,M)) . v1) |-- M)),1)
by MATRIX15:25
.=
((Mx2Tran (A,b1,M)) . v1) |-- M
by MATRIX15:25
.=
(Mx2Tran (A,b1,M)) . v1
by A1, Th46
;
verum end; end;