let p be prime Element of INT.Ring; for V being free Z_Module
for I being Basis of V
for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
let V be free Z_Module; for I being Basis of V
for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
let I be Basis of V; for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
let X be non empty Subset of (Z_MQ_VectSp (V,p)); ( X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I ) )
assume A1:
X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I }
; ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
set ZQ = Z_MQ_VectSp (V,p);
defpred S1[ Element of X, Element of V] means ( $2 in $1 & $2 in I );
A2:
for x being Element of X ex v being Element of V st S1[x,v]
consider F being Function of X, the carrier of V such that
A4:
for x being Element of X holds S1[x,F . x]
from FUNCT_2:sch 3(A2);
take
F
; ( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
thus
for v being Vector of V st v in I holds
F . (ZMtoMQV (V,p,v)) = v
( F is one-to-one & dom F = X & rng F = I )proof
let v be
Vector of
V;
( v in I implies F . (ZMtoMQV (V,p,v)) = v )
assume A5:
v in I
;
F . (ZMtoMQV (V,p,v)) = v
then
ZMtoMQV (
V,
p,
v)
in X
by A1;
then reconsider w =
ZMtoMQV (
V,
p,
v) as
Element of
X ;
A6:
(
F . w in w &
F . w in I )
by A4;
ZMtoMQV (
V,
p,
(F . w))
= ZMtoMQV (
V,
p,
v)
by A4, ZMODUL01:67;
hence
F . (ZMtoMQV (V,p,v)) = v
by A5, A6, Th21;
verum
end;
now for x1, x2 being object st x1 in X & x2 in X & F . x1 = F . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in X & x2 in X & F . x1 = F . x2 implies x1 = x2 )assume A7:
(
x1 in X &
x2 in X &
F . x1 = F . x2 )
;
x1 = x2then reconsider x10 =
x1,
x20 =
x2 as
Element of
X ;
consider v1 being
Vector of
V such that A8:
(
x1 = ZMtoMQV (
V,
p,
v1) &
v1 in I )
by A7, A1;
consider v2 being
Vector of
V such that A9:
(
x2 = ZMtoMQV (
V,
p,
v2) &
v2 in I )
by A7, A1;
(
F . x10 in ZMtoMQV (
V,
p,
v1) &
F . x10 in ZMtoMQV (
V,
p,
v2) )
by A7, A8, A9, A4;
then
F . x10 in (ZMtoMQV (V,p,v1)) /\ (ZMtoMQV (V,p,v2))
by XBOOLE_0:def 4;
hence
x1 = x2
by A8, A9, Lm2;
verum end;
hence
F is one-to-one
by FUNCT_2:19; ( dom F = X & rng F = I )
thus
dom F = X
by FUNCT_2:def 1; rng F = I
then A11:
rng F c= I
;
now for y being object st y in I holds
y in rng Flet y be
object ;
( y in I implies y in rng F )assume A12:
y in I
;
y in rng Fthen reconsider u =
y as
Vector of
V ;
ZMtoMQV (
V,
p,
u)
in X
by A12, A1;
then reconsider z =
ZMtoMQV (
V,
p,
u) as
Element of
X ;
A13:
(
F . z in z &
F . z in I )
by A4;
ZMtoMQV (
V,
p,
(F . z))
= ZMtoMQV (
V,
p,
u)
by A4, ZMODUL01:67;
then
F . z = u
by Th21, A13, A12;
hence
y in rng F
by FUNCT_2:4;
verum end;
then
I c= rng F
;
hence
I = rng F
by A11, XBOOLE_0:def 10; verum