let V be Z_Module; ( V is Mult-cancelable implies ex I being Function of V,(Z_MQ_VectSp V) st
( I is one-to-one & ( for v being Element of V holds I . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
I . (i * v) = q * (I . v) ) & I . (0. V) = 0. (Z_MQ_VectSp V) ) )
assume AS:
V is Mult-cancelable
; ex I being Function of V,(Z_MQ_VectSp V) st
( I is one-to-one & ( for v being Element of V holds I . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
I . (i * v) = q * (I . v) ) & I . (0. V) = 0. (Z_MQ_VectSp V) )
then Z0:
Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #)
by defZMQVSp;
X1:
1 in INT
by INT_1:def 2;
not 1 in {0}
by TARSKI:def 1;
then X2:
1 in INT \ {0}
by XBOOLE_0:def 5, X1;
set i1 = 1. INT.Ring;
defpred S1[ Element of V, Element of (Z_MQ_VectSp V)] means $2 = Class ((EQRZM V),[$1,1]);
A2:
for x being Element of V ex v being Element of (Z_MQ_VectSp V) st S1[x,v]
proof
let x be
Element of
V;
ex v being Element of (Z_MQ_VectSp V) st S1[x,v]
X1:
1
in INT
by INT_1:def 2;
not 1
in {0}
by TARSKI:def 1;
then
1
in INT \ {0}
by XBOOLE_0:def 5, X1;
then
[x,1] in [: the carrier of V,(INT \ {0}):]
by ZFMISC_1:87;
then reconsider z =
Class (
(EQRZM V),
[x,1]) as
Element of
(Z_MQ_VectSp V) by Z0, EQREL_1:def 3;
z = Class (
(EQRZM V),
[x,1])
;
hence
ex
z being
Element of
(Z_MQ_VectSp V) st
S1[
x,
z]
;
verum
end;
consider F being Function of V,(Z_MQ_VectSp V) such that
X3:
for x being Element of V holds S1[x,F . x]
from FUNCT_2:sch 3(A2);
take
F
; ( F is one-to-one & ( for v being Element of V holds F . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds F . (v + w) = (F . v) + (F . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F . (i * v) = q * (F . v) ) & F . (0. V) = 0. (Z_MQ_VectSp V) )
S2:
now for x1, x2 being object st x1 in the carrier of V & x2 in the carrier of V & F . x1 = F . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in the carrier of V & x2 in the carrier of V & F . x1 = F . x2 implies x1 = x2 )assume A1:
(
x1 in the
carrier of
V &
x2 in the
carrier of
V &
F . x1 = F . x2 )
;
x1 = x2then reconsider x10 =
x1,
x20 =
x2 as
Element of
V ;
P1:
F . x1 = Class (
(EQRZM V),
[x10,1])
by X3;
P2:
[x10,1] in [: the carrier of V,(INT \ {0}):]
by X2, ZFMISC_1:87;
Class (
(EQRZM V),
[x10,(1. INT.Ring)])
= Class (
(EQRZM V),
[x20,(1. INT.Ring)])
by A1, P1, X3;
then P3:
[[x10,(1. INT.Ring)],[x20,(1. INT.Ring)]] in EQRZM V
by P2, EQREL_1:35;
thus x1 =
(1. INT.Ring) * x10
by VECTSP_1:def 17
.=
(1. INT.Ring) * x20
by AS, P3, LMEQR001
.=
x2
by VECTSP_1:def 17
;
verum end;
S3:
for v, w being Element of V holds F . (v + w) = (F . v) + (F . w)
proof
let v,
w be
Element of
V;
F . (v + w) = (F . v) + (F . w)
P1:
F . v = Class (
(EQRZM V),
[v,1])
by X3;
P2:
F . w = Class (
(EQRZM V),
[w,1])
by X3;
P8:
((1. INT.Ring) * v) + ((1. INT.Ring) * w) =
(1. INT.Ring) * (v + w)
by VECTSP_1:def 14
.=
v + w
by VECTSP_1:def 17
;
(F . v) + (F . w) =
Class (
(EQRZM V),
[(((1. INT.Ring) * v) + ((1. INT.Ring) * w)),((1. INT.Ring) * (1. INT.Ring))])
by AS, P1, P2, Z0, DefaddCoset
.=
F . (v + w)
by P8, X3
;
hence
F . (v + w) = (F . v) + (F . w)
;
verum
end;
S4:
for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F . (i * v) = q * (F . v)
F . (0. V) =
Class ((EQRZM V),[(0. V),1])
by X3
.=
0. (Z_MQ_VectSp V)
by AS, Z0, defZero
;
hence
( F is one-to-one & ( for v being Element of V holds F . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds F . (v + w) = (F . v) + (F . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F . (i * v) = q * (F . v) ) & F . (0. V) = 0. (Z_MQ_VectSp V) )
by S2, S3, S4, X3, FUNCT_2:19; verum