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 st f is additive & f is homogeneous holds
Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f
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 st f is additive & f is homogeneous holds
Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f
let f be Function of V1,V2; for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st f is additive & f is homogeneous holds
Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f
let b1 be OrdBasis of V1; for b2 being OrdBasis of V2 st f is additive & f is homogeneous holds
Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f
let b2 be OrdBasis of V2; ( f is additive & f is homogeneous implies Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f )
assume A1:
( f is additive & f is homogeneous )
; Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f
set A = AutMt (f,b1,b2);
set M = Mx2Tran ((AutMt (f,b1,b2)),b1,b2);
per cases
( len b1 = 0 or len b1 > 0 )
;
suppose A2:
len b1 = 0
;
Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = fnow for x being object st x in the carrier of V1 holds
f . x = (Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . xA3:
b1 is
one-to-one
by MATRLIN:def 2;
reconsider R =
rng b1 as
Basis of
V1 by MATRLIN:def 2;
let x be
object ;
( x in the carrier of V1 implies f . x = (Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . x )assume A4:
x in the
carrier of
V1
;
f . x = (Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . xA5:
Seg (len b1) = {}
by A2;
dim V1 =
card R
by VECTSP_9:def 1
.=
card (dom b1)
by A3, CARD_1:70
.=
0
by A5, CARD_1:27, FINSEQ_1:def 3
;
then
(Omega). V1 = (0). V1
by VECTSP_9:29;
then
the
carrier of
V1 = {(0. V1)}
by VECTSP_4:def 3;
then
x = 0. V1
by A4, TARSKI:def 1;
hence f . x =
f . ((0. K) * (0. V1))
by VECTSP_1:15
.=
(0. K) * (f . (0. V1))
by A1, MOD_2:def 2
.=
0. V2
by VECTSP_1:15
.=
(Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . x
by A2, A4, Th33
;
verum end; hence
Mx2Tran (
(AutMt (f,b1,b2)),
b1,
b2)
= f
by FUNCT_2:12;
verum end; suppose A6:
len b1 > 0
;
Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = freconsider fb =
f * b1,
Mf =
(Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) * b1 as
FinSequence ;
A7:
rng b1 is
Subset of
V1
by FINSEQ_1:def 4;
dom f = the
carrier of
V1
by FUNCT_2:def 1;
then A8:
len fb = len b1
by A7, FINSEQ_2:29;
dom (Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) = the
carrier of
V1
by FUNCT_2:def 1;
then A9:
len Mf = len b1
by A7, FINSEQ_2:29;
now for i being Nat st 1 <= i & i <= len fb holds
fb . i = Mf . iA10:
dom fb = dom Mf
by A8, A9, FINSEQ_3:29;
let i be
Nat;
( 1 <= i & i <= len fb implies fb . i = Mf . i )assume
( 1
<= i &
i <= len fb )
;
fb . i = Mf . ithen A11:
i in dom fb
by FINSEQ_3:25;
dom fb = dom b1
by A8, FINSEQ_3:29;
then A12:
b1 . i = b1 /. i
by A11, PARTFUN1:def 6;
LineVec2Mx (((Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . (b1 /. i)) |-- b2) =
(LineVec2Mx ((b1 /. i) |-- b1)) * (AutMt (f,b1,b2))
by A6, Th32
.=
LineVec2Mx ((f . (b1 /. i)) |-- b2)
by A1, A6, Th31
;
then ((Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . (b1 /. i)) |-- b2 =
Line (
(LineVec2Mx ((f . (b1 /. i)) |-- b2)),1)
by MATRIX15:25
.=
(f . (b1 /. i)) |-- b2
by MATRIX15:25
;
then
(Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . (b1 /. i) = f . (b1 /. i)
by MATRLIN:34;
hence fb . i =
(Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . (b1 /. i)
by A11, A12, FUNCT_1:12
.=
Mf . i
by A11, A10, A12, FUNCT_1:12
;
verum end; hence
Mx2Tran (
(AutMt (f,b1,b2)),
b1,
b2)
= f
by A1, A6, A8, A9, FINSEQ_1:14, MATRLIN:22;
verum end; end;