let K be Field; :: thesis: for V being finite-dimensional VectSp of K
for b being OrdBasis of V ex T being linear-transformation of V,((dim V) -VectSp_over K) st
( T is bijective & ( for x being Element of V holds T . x = x |-- b ) )
let V be finite-dimensional VectSp of K; :: thesis: for b being OrdBasis of V ex T being linear-transformation of V,((dim V) -VectSp_over K) st
( T is bijective & ( for x being Element of V holds T . x = x |-- b ) )
let b be OrdBasis of V; :: thesis: ex T being linear-transformation of V,((dim V) -VectSp_over K) st
( T is bijective & ( for x being Element of V holds T . x = x |-- b ) )
set W = (dim V) -VectSp_over K;
set W0 = (dim V) -Group_over K;
A1: (dim V) -Group_over K = addLoopStr(# ((dim V) -tuples_on the carrier of K),(product ( the addF of K,(dim V))),((dim V) |-> (0. K)) #) by PRVECT_1:def 3;
A2: addLoopStr(# the carrier of ((dim V) -VectSp_over K), the addF of ((dim V) -VectSp_over K), the ZeroF of ((dim V) -VectSp_over K) #) = (dim V) -Group_over K by PRVECT_1:def 5;
defpred S1[ object , object ] means ex x being Element of V st
( $1 = x & $2 = x |-- b );
A3: the carrier of ((dim V) -VectSp_over K) = (dim V) -tuples_on the carrier of K by MATRIX13:102;
A4: for x being Element of the carrier of V ex y being Element of the carrier of ((dim V) -VectSp_over K) st S1[x,y]
proof
let x be Element of the carrier of V; :: thesis: ex y being Element of the carrier of ((dim V) -VectSp_over K) st S1[x,y]
set y = x |-- b;
len (x |-- b) = len b by MATRLIN:def 7
.= dim V by MATRLIN2:21 ;
then x |-- b is Element of (dim V) -tuples_on the carrier of K by FINSEQ_2:92;
hence ex y being Element of the carrier of ((dim V) -VectSp_over K) st S1[x,y] by A3; :: thesis: verum
end;
consider f being Function of the carrier of V, the carrier of ((dim V) -VectSp_over K) such that
A5: for x being Element of the carrier of V holds S1[x,f . x] from FUNCT_2:sch 3(A4);
 A6: for x being Element of V holds f . x = x |-- b
proof
let x be Element of V; :: thesis: f . x = x |-- b
ex x0 being Element of V st
( x = x0 & f . x = x0 |-- b ) by A5;
hence f . x = x |-- b ; :: thesis: verum
end;
for x, y being Element of V holds f . (x + y) = (f . x) + (f . y)
proof
let x, y be Element of V; :: thesis: f . (x + y) = (f . x) + (f . y)
thus f . (x + y) = (x + y) |-- b by A6
.= (x |-- b) + (y |-- b) by MATRLIN2:17
.= the addF of K .: ((f . x),(y |-- b)) by A6
.= the addF of K .: ((f . x),(f . y)) by A6
.= (f . x) + (f . y) by A1, A2, PRVECT_1:def 1 ; :: thesis: verum
end;
then A12: f is additive ;
for a being Scalar of K
for x being Vector of V holds f . (a * x) = a * (f . x)
proof
let a be Scalar of K; :: thesis: for x being Vector of V holds f . (a * x) = a * (f . x)
let x be Element of V; :: thesis: f . (a * x) = a * (f . x)
A13: f . x = x |-- b by A6;
len (x |-- b) = len b by MATRLIN:def 7
.= dim V by MATRLIN2:21 ;
then A14: f . x is Element of (dim V) -tuples_on the carrier of K by A13, FINSEQ_2:92;
thus f . (a * x) = (a * x) |-- b by A6
.= a * (x |-- b) by MATRLIN2:18
.= ( the multF of K [;] (a,(id the carrier of K))) * (f . x) by A6
.= the multF of K [;] (a,(f . x)) by A14, FINSEQOP:22
.= ((dim V) -Mult_over K) . (a,(f . x)) by A14, PRVECT_1:def 4
.= a * (f . x) by PRVECT_1:def 5 ; :: thesis: verum
end;
then A15: f is linear-transformation of V,((dim V) -VectSp_over K) by A12, MOD_2:def 2;
for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y
proof
let x, y be object ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume A16: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
reconsider x0 = x, y0 = y as Element of V by A16;
x0 |-- b = f . x0 by A6
.= y0 |-- b by A6, A16 ;
hence x = y by MATRLIN:34; :: thesis: verum
end;
then A17: f is one-to-one by FUNCT_1:def 4;
for y being object st y in the carrier of ((dim V) -VectSp_over K) holds
ex x being object st
( x in the carrier of V & y = f . x )
proof
let y0 be object ; :: thesis: ( y0 in the carrier of ((dim V) -VectSp_over K) implies ex x being object st
( x in the carrier of V & y0 = f . x ) )
assume y0 in the carrier of ((dim V) -VectSp_over K) ; :: thesis: ex x being object st
( x in the carrier of V & y0 = f . x )
then reconsider y = y0 as Element of (dim V) -tuples_on the carrier of K by MATRIX13:102;
A18: len y = dim V by CARD_1:def 7
.= len b by MATRLIN2:21 ;
reconsider x = Sum (lmlt (y,b)) as Element of the carrier of V ;
take x ; :: thesis: ( x in the carrier of V & y0 = f . x )
thus x in the carrier of V ; :: thesis: y0 = f . x
thus y0 = x |-- b by A18, MATRLIN:36
.= f . x by A6 ; :: thesis: verum
end;
then rng f = the carrier of ((dim V) -VectSp_over K) by FUNCT_2:10;
then f is onto by FUNCT_2:def 3;
hence ex T being linear-transformation of V,((dim V) -VectSp_over K) st
( T is bijective & ( for x being Element of V holds T . x = x |-- b ) ) by A15, A6, A17; :: thesis: verum