let V be torsion-free Z_Module; :: thesis: for r being Element of F_Rat st r <> 0. F_Rat holds
ex T being linear-transformation of (EMbedding V),(EMbedding (r,V)) st
( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective )
let r be Element of F_Rat; :: thesis: ( r <> 0. F_Rat implies ex T being linear-transformation of (EMbedding V),(EMbedding (r,V)) st
( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective ) )
assume AS: r <> 0. F_Rat ; :: thesis: ex T being linear-transformation of (EMbedding V),(EMbedding (r,V)) st
( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective )
set EZV = Z_MQ_VectSp V;
deffunc H1( Vector of (Z_MQ_VectSp V)) -> Element of the carrier of (Z_MQ_VectSp V) = r * $1;
consider T being Function of the carrier of (Z_MQ_VectSp V), the carrier of (Z_MQ_VectSp V) such that
P1: for x being Element of the carrier of (Z_MQ_VectSp V) holds T . x = H1(x) from FUNCT_2:sch 4();
 set T0 = T | the carrier of (EMbedding V);
D0: the carrier of (EMbedding V) = rng (MorphsZQ V) by defEmbedding;
dom T = the carrier of (Z_MQ_VectSp V) by FUNCT_2:def 1;
then P3: dom (T | the carrier of (EMbedding V)) = the carrier of (EMbedding V) by D0, RELAT_1:62;
D1: the carrier of (EMbedding (r,V)) = r * (rng (MorphsZQ V)) by defriV;
RX0: for y being object holds
( y in rng (T | the carrier of (EMbedding V)) iff y in the carrier of (EMbedding (r,V)) )
proof
let y be object ; :: thesis: ( y in rng (T | the carrier of (EMbedding V)) iff y in the carrier of (EMbedding (r,V)) )
hereby :: thesis: ( y in the carrier of (EMbedding (r,V)) implies y in rng (T | the carrier of (EMbedding V)) )
assume y in rng (T | the carrier of (EMbedding V)) ; :: thesis: y in the carrier of (EMbedding (r,V))
then consider x being object such that
A2: ( x in dom (T | the carrier of (EMbedding V)) & y = (T | the carrier of (EMbedding V)) . x ) by FUNCT_1:def 3;
reconsider x = x as Element of (Z_MQ_VectSp V) by A2;
(T | the carrier of (EMbedding V)) . x = T . x by FUNCT_1:49, A2, P3
.= r * x by P1 ;
hence y in the carrier of (EMbedding (r,V)) by A2, D0, D1, P3; :: thesis: verum
end;
assume y in the carrier of (EMbedding (r,V)) ; :: thesis: y in rng (T | the carrier of (EMbedding V))
then y in r * (rng (MorphsZQ V)) by defriV;
then consider x being Vector of (Z_MQ_VectSp V) such that
A4: ( y = r * x & x in rng (MorphsZQ V) ) ;
A5: x in the carrier of (EMbedding V) by A4, defEmbedding;
(T | the carrier of (EMbedding V)) . x = T . x by FUNCT_1:49, A5
.= y by A4, P1 ;
hence y in rng (T | the carrier of (EMbedding V)) by A5, P3, FUNCT_1:def 3; :: thesis: verum
end;
then rng (T | the carrier of (EMbedding V)) = the carrier of (EMbedding (r,V)) by TARSKI:2;
then reconsider T0 = T | the carrier of (EMbedding V) as Function of (EMbedding V),(EMbedding (r,V)) by P3, FUNCT_2:1;
B0: T0 is additive
proof
let x, y be Element of (EMbedding V); :: according to VECTSP_1:def 19 :: thesis: T0 . (x + y) = (T0 . x) + (T0 . y)
F1: ( x in EMbedding V & y in EMbedding V ) ;
reconsider x0 = x, y0 = y as Vector of (Z_MQ_VectSp V) by SB01;
F2: x0 + y0 in EMbedding V by F1, SB02;
F3: T . x0 = T0 . x by FUNCT_1:49;
F4: T . y0 = T0 . y by FUNCT_1:49;
thus T0 . (x + y) = T0 . (x0 + y0) by SB01
.= T . (x0 + y0) by FUNCT_1:49, F2
.= r * (x0 + y0) by P1
.= (r * x0) + (r * y0) by VECTSP_1:def 14
.= (T . x0) + (r * y0) by P1
.= (T . x0) + (T . y0) by P1
.= (T0 . x) + (T0 . y) by rSB01, F3, F4 ; :: thesis: verum
end;
for x being Element of (EMbedding V)
for i being Element of INT.Ring holds T0 . (i * x) = i * (T0 . x)
proof
let x be Element of (EMbedding V); :: thesis: for i being Element of INT.Ring holds T0 . (i * x) = i * (T0 . x)
let i be Element of INT.Ring; :: thesis: T0 . (i * x) = i * (T0 . x)
F1: x in EMbedding V ;
reconsider x0 = x as Vector of (Z_MQ_VectSp V) by SB01;
reconsider j = i as Element of F_Rat by NUMBERS:14;
F2: j * x0 in EMbedding V by F1, SB02;
F3: T . x0 = T0 . x by FUNCT_1:49;
thus T0 . (i * x) = T0 . (j * x0) by SB01
.= T . (j * x0) by FUNCT_1:49, F2
.= r * (j * x0) by P1
.= (r * j) * x0 by VECTSP_1:def 16
.= j * (r * x0) by VECTSP_1:def 16
.= i * (T0 . x) by rSB01, F3, P1 ; :: thesis: verum
end;
then ( T0 is additive & T0 is homogeneous ) by B0;
then reconsider T0 = T0 as linear-transformation of (EMbedding V),(EMbedding (r,V)) ;
take T0 ; :: thesis: ( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T0 . v = r * v ) & T0 is bijective )
thus XX1: for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T0 . v = r * v :: thesis: T0 is bijective
proof
let x be Element of (Z_MQ_VectSp V); :: thesis: ( x in EMbedding V implies T0 . x = r * x )
assume F1: x in EMbedding V ; :: thesis: T0 . x = r * x
thus T0 . x = T . x by FUNCT_1:49, F1
.= r * x by P1 ; :: thesis: verum
end;
for x1, x2 being object st x1 in the carrier of (EMbedding V) & x2 in the carrier of (EMbedding V) & T0 . x1 = T0 . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in the carrier of (EMbedding V) & x2 in the carrier of (EMbedding V) & T0 . x1 = T0 . x2 implies x1 = x2 )
assume AS2: ( x1 in the carrier of (EMbedding V) & x2 in the carrier of (EMbedding V) & T0 . x1 = T0 . x2 ) ; :: thesis: x1 = x2
then reconsider xx1 = x1, xx2 = x2 as Element of (Z_MQ_VectSp V) by D0;
Q0: ( xx1 in EMbedding V & xx2 in EMbedding V ) by AS2;
Q1: T0 . x1 = r * xx1 by Q0, XX1;
Q2: (r ") * (r * xx1) = (r ") * (r * xx2) by AS2, Q0, Q1, XX1;
(r ") * (r * xx1) = xx1 by AS, VECTSP_1:20;
hence x1 = x2 by Q2, AS, VECTSP_1:20; :: thesis: verum
end;
then T1: T0 is one-to-one by FUNCT_2:19;
T0 is onto by RX0, FUNCT_2:def 3, TARSKI:2;
hence T0 is bijective by T1; :: thesis: verum