let V be Z_Module; :: thesis: ( V is Mult-cancelable implies ModuleStr(# (Class ()),(),(),() #) is VectSp of F_Rat )
assume AS: V is Mult-cancelable ; :: thesis: ModuleStr(# (Class ()),(),(),() #) is VectSp of F_Rat
reconsider IT = ModuleStr(# (Class ()),(),(),() #) as non empty ModuleStr over F_Rat ;
set F = F_Rat ;
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; :: thesis: for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w)
let v, w be Element of IT; :: thesis: 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 ((),[z,i]) ) by ;
consider j being Element of INT.Ring, y being Element of V such that
X2: ( j <> 0 & w = Class ((),[y,j]) ) by ;
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 ((),[((j * z) + (i * y)),(i * j)]) by ;
X7: x * v = Class ((),[(m * z),(n * i)]) by ;
X8: x * w = Class ((),[(m * y),(n * j)]) by ;
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 ((),[(((n * j) * (m * z)) + ((n * i) * (m * y))),((n * i) * (n * j))]) by X1, X2, X3, X7, X8, DefaddCoset, AS
.= Class ((),[(n * (m * ((j * z) + (i * y)))),(n * (n * (i * j)))]) by X11
.= Class ((),[(m * ((j * z) + (i * y))),(n * (i * j))]) by AS, X1, X2, X3, LMEQR003 ;
hence x * (v + w) = (x * v) + (x * w) by ; :: thesis: 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; :: thesis: for v being Element of IT holds (x + y) * v = (x * v) + (y * v)
let v be Element of IT; :: thesis: (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 ((),[z,i]) ) by ;
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 ;
reconsider l = l, k = k, m = m, n = n as Element of INT.Ring by Lem1;
X7: x * v = Class ((),[(m * z),(n * i)]) by ;
X8: y * v = Class ((),[(l * z),(k * i)]) by ;
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 ((),[(((k * i) * (m * z)) + ((n * i) * (l * z))),((n * i) * (k * i))]) by X1, X3, X7, X8, Y3, DefaddCoset, AS
.= Class ((),[(i * (((k * m) + (n * l)) * z)),(i * ((n * k) * i))]) by X11
.= Class ((),[(((k * m) + (n * l)) * z),((n * k) * i)]) by AS, X1, X3, Y3, LMEQR003 ;
hence (x + y) * v = (x * v) + (y * v) by ; :: thesis: 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; :: thesis: for v being Element of IT holds (x * y) * v = x * (y * v)
let v be Element of IT; :: thesis: (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 ((),[z,i]) ) by ;
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 ((),[(ll * z),(kk * i)]) by ;
x * (y * v) = Class ((),[(mm * (ll * z)),(nn * (kk * i))]) by
.= Class ((),[((mm * ll) * z),((nn * kk) * i)]) by VECTSP_1:def 16 ;
hence (x * y) * v = x * (y * v) by ; :: thesis: verum
end;
P4: for v being Element of IT holds () * v = v
proof
let v be Element of IT; :: thesis: () * 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 ((),[z,i]) ) by ;
X2: 1. F_Rat = 1
.= ii1 / ii1 ;
thus () * v = Class ((),[(() * z),(() * i)]) by
.= v by ; :: thesis: verum
end;
P5: for v being Element of IT holds v is right_complementable
proof
let v be Element of IT; :: thesis:
consider i being Element of INT.Ring, z being Element of V such that
X1: ( i <> 0 & v = Class ((),[z,i]) ) by ;
X21: not - i in by ;
- i in INT \ by ;
then [z,(- i)] in [: the carrier of V,():] by ZFMISC_1:87;
then reconsider w = Class ((),[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 ((),[(((- i) * z) + (i * z)),(i * (- i))]) by
.= 0. IT by ;
hence v is right_complementable by ALGSTR_0:def 11; :: thesis: verum
end;
P6: for v, w being Element of IT holds v + w = w + v
proof
let v, w be Element of IT; :: thesis: v + w = w + v
consider i being Element of INT.Ring, z being Element of V such that
X1: ( i <> 0 & v = Class ((),[z,i]) ) by ;
consider j being Element of INT.Ring, y being Element of V such that
X2: ( j <> 0 & w = Class ((),[y,j]) ) by ;
v + w = Class ((),[((j * z) + (i * y)),(i * j)]) by ;
hence v + w = w + v by ; :: thesis: 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; :: thesis: (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 ((),[s,k]) ) by ;
consider i being Element of INT.Ring, z being Element of V such that
X1: ( i <> 0 & v = Class ((),[z,i]) ) by ;
consider j being Element of INT.Ring, y being Element of V such that
X2: ( j <> 0 & w = Class ((),[y,j]) ) by ;
X3: u + v = Class ((),[((i * s) + (k * z)),(k * i)]) by ;
X4: (u + v) + w = Class ((),[((j * ((i * s) + (k * z))) + ((k * i) * y)),((k * i) * j)]) by ;
X5: v + w = Class ((),[((j * z) + (i * y)),(i * j)]) by ;
X6: u + (v + w) = Class ((),[(((i * j) * s) + (k * ((j * z) + (i * y)))),(k * (i * j))]) by ;
(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; :: thesis: verum
end;
for v being Element of IT holds v + (0. IT) = v
proof
let u be Element of IT; :: thesis: u + (0. IT) = u
consider i being Element of INT.Ring, z being Element of V such that
X1: ( i <> 0 & u = Class ((),[z,i]) ) by ;
reconsider i1 = 1. INT.Ring as Element of INT.Ring ;
X3: 0. IT = Class ((),[(0. V),i1]) by ;
X5: u + (0. IT) = Class ((),[((i1 * z) + (i * (0. V))),(i1 * i)]) by ;
(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; :: thesis: verum
end;
hence ModuleStr(# (Class ()),(),(),() #) is VectSp of F_Rat by ; :: thesis: verum