let V be Z_Module; ( V is Mult-cancelable implies ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) is VectSp of F_Rat )
assume AS:
V is Mult-cancelable
; ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) is VectSp of F_Rat
reconsider IT = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) as non empty ModuleStr over F_Rat ;
set F = F_Rat ;
set AD = addCoset V;
set ML = lmultCoset V;
P1:
for x being Element of F_Rat
for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w)
proof
let x be
Element of
F_Rat;
for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w)let v,
w be
Element of
IT;
x * (v + w) = (x * v) + (x * w)
consider i being
Element of
INT.Ring,
z being
Element of
V such that X1:
(
i <> 0 &
v = Class (
(EQRZM V),
[z,i]) )
by AS, LMEQRZM1;
consider j being
Element of
INT.Ring,
y being
Element of
V such that X2:
(
j <> 0 &
w = Class (
(EQRZM V),
[y,j]) )
by AS, LMEQRZM1;
consider m,
n being
Integer such that X3:
(
n <> 0 &
x = m / n )
by RAT_1:1;
reconsider m =
m,
n =
n as
Element of
INT.Ring by Lem1;
X5:
v + w = Class (
(EQRZM V),
[((j * z) + (i * y)),(i * j)])
by X1, X2, DefaddCoset, AS;
X7:
x * v = Class (
(EQRZM V),
[(m * z),(n * i)])
by DeflmultCoset, AS, X1, X3;
X8:
x * w = Class (
(EQRZM V),
[(m * y),(n * j)])
by DeflmultCoset, AS, X2, X3;
X11:
((n * j) * (m * z)) + ((n * i) * (m * y)) =
(((n * j) * m) * z) + ((n * i) * (m * y))
by VECTSP_1:def 16
.=
(((n * m) * j) * z) + (((n * i) * m) * y)
by VECTSP_1:def 16
.=
((n * m) * (j * z)) + (((n * m) * i) * y)
by VECTSP_1:def 16
.=
((n * m) * (j * z)) + ((n * m) * (i * y))
by VECTSP_1:def 16
.=
(n * (m * (j * z))) + ((n * m) * (i * y))
by VECTSP_1:def 16
.=
(n * (m * (j * z))) + (n * (m * (i * y)))
by VECTSP_1:def 16
.=
n * ((m * (j * z)) + (m * (i * y)))
by VECTSP_1:def 14
.=
n * (m * ((j * z) + (i * y)))
by VECTSP_1:def 14
;
(x * v) + (x * w) =
Class (
(EQRZM V),
[(((n * j) * (m * z)) + ((n * i) * (m * y))),((n * i) * (n * j))])
by X1, X2, X3, X7, X8, DefaddCoset, AS
.=
Class (
(EQRZM V),
[(n * (m * ((j * z) + (i * y)))),(n * (n * (i * j)))])
by X11
.=
Class (
(EQRZM V),
[(m * ((j * z) + (i * y))),(n * (i * j))])
by AS, X1, X2, X3, LMEQR003
;
hence
x * (v + w) = (x * v) + (x * w)
by DeflmultCoset, AS, X1, X2, X3, X5;
verum
end;
P2:
for x, y being Element of F_Rat
for v being Element of IT holds (x + y) * v = (x * v) + (y * v)
proof
let x,
y be
Element of
F_Rat;
for v being Element of IT holds (x + y) * v = (x * v) + (y * v)let v be
Element of
IT;
(x + y) * v = (x * v) + (y * v)
consider i being
Element of
INT.Ring,
z being
Element of
V such that X1:
(
i <> 0 &
v = Class (
(EQRZM V),
[z,i]) )
by AS, LMEQRZM1;
consider m,
n being
Integer such that X3:
(
n <> 0 &
x = m / n )
by RAT_1:1;
consider l,
k being
Integer such that Y3:
(
k <> 0 &
y = l / k )
by RAT_1:1;
Y4:
x + y =
(m / n) + (l / k)
by X3, Y3
.=
((k * m) + (n * l)) / (n * k)
by XCMPLX_1:116, X3, Y3
;
reconsider l =
l,
k =
k,
m =
m,
n =
n as
Element of
INT.Ring by Lem1;
X7:
x * v = Class (
(EQRZM V),
[(m * z),(n * i)])
by DeflmultCoset, AS, X1, X3;
X8:
y * v = Class (
(EQRZM V),
[(l * z),(k * i)])
by DeflmultCoset, AS, X1, Y3;
X11:
((k * i) * (m * z)) + ((n * i) * (l * z)) =
(((k * i) * m) * z) + ((n * i) * (l * z))
by VECTSP_1:def 16
.=
((i * (k * m)) * z) + (((i * n) * l) * z)
by VECTSP_1:def 16
.=
(i * ((k * m) * z)) + ((i * (n * l)) * z)
by VECTSP_1:def 16
.=
(i * ((k * m) * z)) + (i * ((n * l) * z))
by VECTSP_1:def 16
.=
i * (((k * m) * z) + ((n * l) * z))
by VECTSP_1:def 14
.=
i * (((k * m) + (n * l)) * z)
by VECTSP_1:def 15
;
(x * v) + (y * v) =
Class (
(EQRZM V),
[(((k * i) * (m * z)) + ((n * i) * (l * z))),((n * i) * (k * i))])
by X1, X3, X7, X8, Y3, DefaddCoset, AS
.=
Class (
(EQRZM V),
[(i * (((k * m) + (n * l)) * z)),(i * ((n * k) * i))])
by X11
.=
Class (
(EQRZM V),
[(((k * m) + (n * l)) * z),((n * k) * i)])
by AS, X1, X3, Y3, LMEQR003
;
hence
(x + y) * v = (x * v) + (y * v)
by DeflmultCoset, AS, X1, X3, Y3, Y4;
verum
end;
P3:
for x, y being Element of F_Rat
for v being Element of IT holds (x * y) * v = x * (y * v)
proof
let x,
y be
Element of
F_Rat;
for v being Element of IT holds (x * y) * v = x * (y * v)let v be
Element of
IT;
(x * y) * v = x * (y * v)
consider i being
Element of
INT.Ring,
z being
Element of
V such that X1:
(
i <> 0 &
v = Class (
(EQRZM V),
[z,i]) )
by AS, LMEQRZM1;
consider m,
n being
Integer such that X3:
(
n <> 0 &
x = m / n )
by RAT_1:1;
consider l,
k being
Integer such that Y3:
(
k <> 0 &
y = l / k )
by RAT_1:1;
reconsider mm =
m,
nn =
n,
ll =
l,
kk =
k as
Element of
INT.Ring by Lem1;
Y4:
x * y =
(m / n) * (l / k)
by X3, Y3
.=
(m * l) / (n * k)
by XCMPLX_1:76
;
X8:
y * v = Class (
(EQRZM V),
[(ll * z),(kk * i)])
by DeflmultCoset, AS, X1, Y3;
x * (y * v) =
Class (
(EQRZM V),
[(mm * (ll * z)),(nn * (kk * i))])
by DeflmultCoset, AS, X1, X3, X8, Y3
.=
Class (
(EQRZM V),
[((mm * ll) * z),((nn * kk) * i)])
by VECTSP_1:def 16
;
hence
(x * y) * v = x * (y * v)
by DeflmultCoset, AS, X1, X3, Y3, Y4;
verum
end;
P4:
for v being Element of IT holds (1. F_Rat) * v = v
proof
let v be
Element of
IT;
(1. F_Rat) * v = v
set i1 =
1. INT.Ring;
reconsider ii1 =
1. INT.Ring as
Integer ;
consider i being
Element of
INT.Ring,
z being
Element of
V such that X1:
(
i <> 0 &
v = Class (
(EQRZM V),
[z,i]) )
by AS, LMEQRZM1;
X2:
1. F_Rat =
1
.=
ii1 / ii1
;
thus (1. F_Rat) * v =
Class (
(EQRZM V),
[((1. INT.Ring) * z),((1. INT.Ring) * i)])
by DeflmultCoset, AS, X1, X2
.=
v
by X1, VECTSP_1:def 17
;
verum
end;
P5:
for v being Element of IT holds v is right_complementable
proof
let v be
Element of
IT;
v is right_complementable
consider i being
Element of
INT.Ring,
z being
Element of
V such that X1:
(
i <> 0 &
v = Class (
(EQRZM V),
[z,i]) )
by AS, LMEQRZM1;
X21:
not
- i in {0}
by X1, TARSKI:def 1;
- i in INT \ {0}
by XBOOLE_0:def 5, X21;
then
[z,(- i)] in [: the carrier of V,(INT \ {0}):]
by ZFMISC_1:87;
then reconsider w =
Class (
(EQRZM V),
[z,(- i)]) as
Element of
IT by EQREL_1:def 3;
X3:
((- i) * z) + (i * z) =
((- i) + i) * z
by VECTSP_1:def 15
.=
0. V
by ZMODUL01:1
;
v + w =
Class (
(EQRZM V),
[(((- i) * z) + (i * z)),(i * (- i))])
by X1, DefaddCoset, AS
.=
0. IT
by AS, X1, X3, defZero
;
hence
v is
right_complementable
by ALGSTR_0:def 11;
verum
end;
P6:
for v, w being Element of IT holds v + w = w + v
proof
let v,
w be
Element of
IT;
v + w = w + v
consider i being
Element of
INT.Ring,
z being
Element of
V such that X1:
(
i <> 0 &
v = Class (
(EQRZM V),
[z,i]) )
by AS, LMEQRZM1;
consider j being
Element of
INT.Ring,
y being
Element of
V such that X2:
(
j <> 0 &
w = Class (
(EQRZM V),
[y,j]) )
by AS, LMEQRZM1;
v + w = Class (
(EQRZM V),
[((j * z) + (i * y)),(i * j)])
by X1, X2, DefaddCoset, AS;
hence
v + w = w + v
by AS, X1, X2, DefaddCoset;
verum
end;
P7:
for u, v, w being Element of IT holds (u + v) + w = u + (v + w)
proof
let u,
v,
w be
Element of
IT;
(u + v) + w = u + (v + w)
consider k being
Element of
INT.Ring,
s being
Element of
V such that X0:
(
k <> 0 &
u = Class (
(EQRZM V),
[s,k]) )
by AS, LMEQRZM1;
consider i being
Element of
INT.Ring,
z being
Element of
V such that X1:
(
i <> 0 &
v = Class (
(EQRZM V),
[z,i]) )
by AS, LMEQRZM1;
consider j being
Element of
INT.Ring,
y being
Element of
V such that X2:
(
j <> 0 &
w = Class (
(EQRZM V),
[y,j]) )
by AS, LMEQRZM1;
X3:
u + v = Class (
(EQRZM V),
[((i * s) + (k * z)),(k * i)])
by X0, X1, DefaddCoset, AS;
X4:
(u + v) + w = Class (
(EQRZM V),
[((j * ((i * s) + (k * z))) + ((k * i) * y)),((k * i) * j)])
by X0, X1, X2, X3, DefaddCoset, AS;
X5:
v + w = Class (
(EQRZM V),
[((j * z) + (i * y)),(i * j)])
by X1, X2, DefaddCoset, AS;
X6:
u + (v + w) = Class (
(EQRZM V),
[(((i * j) * s) + (k * ((j * z) + (i * y)))),(k * (i * j))])
by X0, X1, X2, X5, DefaddCoset, AS;
(j * ((i * s) + (k * z))) + ((k * i) * y) =
((j * (i * s)) + (j * (k * z))) + ((k * i) * y)
by VECTSP_1:def 14
.=
(((j * i) * s) + (j * (k * z))) + ((k * i) * y)
by VECTSP_1:def 16
.=
(((i * j) * s) + (j * (k * z))) + ((k * i) * y)
.=
(((i * j) * s) + (j * (k * z))) + (k * (i * y))
by VECTSP_1:def 16
.=
(((i * j) * s) + ((j * k) * z)) + (k * (i * y))
by VECTSP_1:def 16
.=
(((i * j) * s) + ((k * j) * z)) + (k * (i * y))
.=
(((i * j) * s) + (k * (j * z))) + (k * (i * y))
by VECTSP_1:def 16
.=
((i * j) * s) + ((k * (j * z)) + (k * (i * y)))
by RLVECT_1:def 3
.=
((i * j) * s) + (k * ((j * z) + (i * y)))
by VECTSP_1:def 14
;
hence
(u + v) + w = u + (v + w)
by X4, X6;
verum
end;
for v being Element of IT holds v + (0. IT) = v
proof
let u be
Element of
IT;
u + (0. IT) = u
consider i being
Element of
INT.Ring,
z being
Element of
V such that X1:
(
i <> 0 &
u = Class (
(EQRZM V),
[z,i]) )
by AS, LMEQRZM1;
reconsider i1 =
1. INT.Ring as
Element of
INT.Ring ;
X3:
0. IT = Class (
(EQRZM V),
[(0. V),i1])
by AS, defZero;
X5:
u + (0. IT) = Class (
(EQRZM V),
[((i1 * z) + (i * (0. V))),(i1 * i)])
by AS, X1, X3, DefaddCoset;
(i1 * z) + (i * (0. V)) =
z + (i * (0. V))
by VECTSP_1:def 17
.=
z + (0. V)
by ZMODUL01:1
.=
z
;
hence
u + (0. IT) = u
by X5, X1;
verum
end;
hence
ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) is VectSp of F_Rat
by P1, P2, P3, P4, P5, P6, P7, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17; verum