let V be torsion-free Z_Module; for i being non zero Integer
for r1, r2 being non zero Element of F_Rat st r2 = r1 / i holds
EMbedding (r1,V) is Submodule of EMbedding (r2,V)
let i be non zero Integer; for r1, r2 being non zero Element of F_Rat st r2 = r1 / i holds
EMbedding (r1,V) is Submodule of EMbedding (r2,V)
let r1, r2 be non zero Element of F_Rat; ( r2 = r1 / i implies EMbedding (r1,V) is Submodule of EMbedding (r2,V) )
assume A1:
r2 = r1 / i
; EMbedding (r1,V) is Submodule of EMbedding (r2,V)
A2:
for x being Vector of (DivisibleMod V) st x in EMbedding (r1,V) holds
x in EMbedding (r2,V)
proof
let x be
Vector of
(DivisibleMod V);
( x in EMbedding (r1,V) implies x in EMbedding (r2,V) )
assume B1:
x in EMbedding (
r1,
V)
;
x in EMbedding (r2,V)
consider T1 being
linear-transformation of
(EMbedding V),
(EMbedding (r1,V)) such that B2:
( ( for
v being
Element of
(Z_MQ_VectSp V) st
v in EMbedding V holds
T1 . v = r1 * v ) &
T1 is
bijective )
by rSB03A;
consider T2 being
linear-transformation of
(EMbedding V),
(EMbedding (r2,V)) such that B3:
( ( for
v being
Element of
(Z_MQ_VectSp V) st
v in EMbedding V holds
T2 . v = r2 * v ) &
T2 is
bijective )
by rSB03A;
reconsider ii =
i as
Element of
INT.Ring by INT_1:def 2;
reconsider ir =
i as
Element of
F_Rat by INT_1:def 2, NUMBERS:14;
reconsider iv = 1
/ i as
Element of
F_Rat by RAT_1:def 1;
x in rng T1
by B1, B2, FUNCT_2:def 3;
then consider v being
object such that B4:
(
v in the
carrier of
(EMbedding V) &
x = T1 . v )
by FUNCT_2:11;
reconsider vv =
v as
Vector of
(Z_MQ_VectSp V) by B4, SB01;
B5:
vv in EMbedding V
by B4;
then
T2 . vv = r2 * vv
by B3;
then reconsider rv =
r2 * vv as
Vector of
(EMbedding (r2,V)) by B4, FUNCT_2:5;
B7:
ir * iv =
i / i
.=
1. F_Rat
by XCMPLX_1:60
;
ii * rv =
ir * (r2 * vv)
by rSB01
.=
(ir * r2) * vv
by VECTSP_1:def 16
.=
(r1 * (ir * iv)) * vv
by A1
.=
x
by B2, B4, B5, B7
;
hence
x in EMbedding (
r2,
V)
;
verum
end;
( EMbedding (r1,V) is Submodule of DivisibleMod V & EMbedding (r2,V) is Submodule of DivisibleMod V )
by ThDivisible3;
hence
EMbedding (r1,V) is Submodule of EMbedding (r2,V)
by A2, ZMODUL01:44; verum