:: $\mathbb Z$-modules
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received September 5, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, FUNCT_1,
ZFMISC_1, XBOOLE_0, RELAT_1, ARYTM_3, PARTFUN1, SUPINF_2, FUNCT_5,
MCART_1, ARYTM_1, CARD_1, FINSEQ_1, CARD_3, TARSKI, XXREAL_0, RLVECT_1,
REALSET1, RLSUB_1, ZMODUL01, INT_1, FINSEQ_4, LATTICES, EQREL_1, PBOOLE,
RLSUB_2, RMOD_2, RMOD_3, BINOM, NAT_1, INT_3, VECTSP_1, MESFUNC1,
BINOP_2, MOD_2, VECTSP_2, FUNCSDOM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCT_5, NUMBERS,
XCMPLX_0, XXREAL_0, INT_1, NAT_1, REALSET1, FINSEQ_1, BINOP_2, XREAL_0,
FINSEQ_4, STRUCT_0, ALGSTR_0, LATTICES, RLVECT_1, VECTSP_1, BINOM,
GROUP_1, VECTSP_2, INT_3, VECTSP_4, VECTSP_5, MOD_2;
constructors BINOP_1, NAT_1, FUNCT_3, FUNCT_5, REALSET1, RELSET_1, GROUP_1,
LATTICES, RLSUB_1, ALGSTR_1, BINOM, FINSEQ_4, VECTSP_1, INT_3, VECTSP_2,
VECTSP_4, BINOP_2, MOD_2, VECTSP_5, MEMBERED;
registrations ORDINAL1, XREAL_0, NAT_1, STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1,
SUBSET_1, INT_1, LATTICES, RELAT_1, ALGSTR_1, INT_3, VECTSP_1, VECTSP_5,
MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, ALGSTR_0, RLVECT_1, XBOOLE_0, VECTSP_1, VECTSP_4;
equalities STRUCT_0, ALGSTR_0, LATTICES, REALSET1, BINOP_1, BINOM, VECTSP_4,
INT_3, VECTSP_1;
expansions TARSKI, STRUCT_0, ALGSTR_0, LATTICES, XBOOLE_0, BINOP_1, VECTSP_4,
VECTSP_5;
theorems FUNCT_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, FINSEQ_1, ALGSTR_0,
BINOM, FINSEQ_3, INT_1, RLVECT_1, LATTICES, PARTFUN1, RELSET_1, XREAL_1,
VECTSP_1, VECTSP_4, VECTSP_5, INT_3, BINOP_2, GR_CY_1, MOD_2;
schemes NAT_1, BINOP_1;
begin :: 1. Definition of Z-module
definition
::$CD 6
mode Z_Module is LeftMod of INT.Ring;
end;
registration
cluster TrivialLMod INT.Ring -> trivial non empty strict;
coherence
proof
TrivialLMod INT.Ring =
ModuleStr (#{0},op2,op0,pr2(the carrier of INT.Ring,{0})#)
by MOD_2:def 1; then
the carrier of TrivialLMod INT.Ring = {0};
hence thesis;
end;
end;
registration
cluster strict for Z_Module;
existence
proof
take TrivialLMod(INT.Ring);
thus thesis;
end;
end;
definition
let R be Ring;
let V be LeftMod of R;
mode VECTOR of V is Element of V;
end;
reserve R for Ring;
reserve x, y, y1 for set;
reserve a, b for Element of R;
reserve V for LeftMod of R;
reserve v, w for Vector of V;
definition
let R be Ring;
let IT be LeftMod of R;
attr IT is Mult-cancelable means
for a being Element of R
for v being Vector of IT st a * v = 0.IT holds
a = 0.R or v = 0.IT;
end;
theorem Th1:
for V being Z_Module
for a being Element of INT.Ring,
v being Vector of V holds
a = 0.INT.Ring or v = 0.V implies a * v = 0.V
proof
let V be Z_Module;
let a be Element of INT.Ring,
v be Vector of V;
set R = INT.Ring;
set N1=1.INT.Ring, N0=0.INT.Ring;
assume
A1: a = 0.R or v = 0.V;
now
per cases by A1;
suppose
A2: a = 0.R;
v + N0 * v = N1 * v + N0 * v
.= (N1 + N0) * v by VECTSP_1:def 15
.= v
.= v + 0.V by RLVECT_1:4;
hence thesis by A2,RLVECT_1:8;
end;
suppose
A3: v = 0.V;
a * 0.V + a * 0.V = a * (0.V + 0.V) by VECTSP_1:def 14
.= a * 0.V by RLVECT_1:4
.= a * 0.V + 0.V by RLVECT_1:4;
hence thesis by A3,RLVECT_1:8;
end;
end;
hence thesis;
end;
theorem Th2:
- v = (- 1.R) * v by VECTSP_1:14;
theorem Th3:
for V being Z_Module,
v being Vector of V holds
V is Mult-cancelable & v = - v implies v = 0.V
proof
let V be Z_Module,
v be Vector of V;
assume A1:V is Mult-cancelable;
set a = 1.INT.Ring;
assume v = - v; then
0.V = v + v by RLVECT_1:def 10
.= a * v + v
.= a * v + a * v
.= (a + a) * v by VECTSP_1:def 15;
hence thesis by A1;
end;
theorem
for V being Z_Module,
v being Vector of V holds
V is Mult-cancelable & v + v = 0.V implies v = 0.V
proof
let V be Z_Module,
v be Vector of V;
assume A1: V is Mult-cancelable;
assume v + v = 0.V;
then v = - v by RLVECT_1:def 10;
hence thesis by A1,Th3;
end;
theorem Th5:
for V being Z_Module,
a being Element of INT.Ring,
v being Vector of V holds
a * (- v) = (- a) * v
proof
let V be Z_Module,
a be Element of INT.Ring,
v be Vector of V;
thus a * (- v) = a * ((- 1.INT.Ring) * v) by VECTSP_1:14
.= (a * (- 1.INT.Ring)) * v by VECTSP_1:def 16
.= (- a) * v;
end;
theorem Th6:
for V being Z_Module,
a being Element of INT.Ring,
v being Vector of V holds
a * (- v) = - (a * v)
proof
let V be Z_Module,
a be Element of INT.Ring,
v be Vector of V;
set i = 1.INT.Ring;
thus a * (- v) = (- a) * v by Th5
.= ((- i) * a) * v
.= (- i) * (a * v) by VECTSP_1:def 16
.= - (a * v) by Th2;
end;
theorem
for V being Z_Module,
a being Element of INT.Ring,
v being Vector of V holds
(- a) * (- v) = a * v
proof
let V be Z_Module,
a be Element of INT.Ring,
v be Vector of V;
thus (- a) * (- v) = (--a) * v by Th5
.= a * v;
end;
theorem Th8:
for V being Z_Module,
a being Element of INT.Ring,
v,w being Vector of V holds
a * (v - w) = a * v - a * w
proof
let V be Z_Module,
a be Element of INT.Ring,
v,w be Vector of V;
thus a * (v - w) = a * v + a * (- w) by VECTSP_1:def 14
.= a * v - a * w by Th6;
end;
theorem Th9:
for V being Z_Module,
a,b being Element of INT.Ring,
v being Vector of V holds
(a - b) * v = a * v - b * v
proof
let V be Z_Module,
a,b be Element of INT.Ring,
v be Vector of V;
thus (a - b) * v = a * v + (- b) * v by VECTSP_1:def 15
.= a * v + b * (- v) by Th5
.= a * v - b * v by Th6;
end;
theorem
for V being Z_Module,
a being Element of INT.Ring,
v,w being Vector of V holds
V is Mult-cancelable & a <> 0.INT.Ring & a * v = a * w implies v = w
proof
let V be Z_Module,
a be Element of INT.Ring,
v,w be Vector of V;
assume A1:V is Mult-cancelable;
set R = INT.Ring;
assume that
A2: a <> 0.R and
A3: a * v = a * w;
0.V = a * v - a * w by A3,RLVECT_1:15
.= a * (v - w) by Th8;
then v - w = 0.V by A2,A1;
hence thesis by RLVECT_1:21;
end;
theorem
for V being Z_Module,
a,b being Element of INT.Ring,
v being Vector of V holds
V is Mult-cancelable & v <> 0.V & a * v = b * v implies a = b
proof
let V be Z_Module,
a,b be Element of INT.Ring,
v be Vector of V;
assume A1: V is Mult-cancelable;
assume that
A2: v <> 0.V and
A3: a * v = b * v;
0.V = a * v - b * v by A3,RLVECT_1:15
.= (a - b) * v by Th9;
then (- b) + a = 0 by A2,A1 .= 0.INT.Ring;
hence thesis;
end;
reserve u,v,w for Vector of V;
reserve F,G,H,I for FinSequence of V;
reserve j,k,n for Nat;
reserve f,f9,g for sequence of V;
Lm1: Sum(<*>(the carrier of V)) = 0.V
proof
set S = <*>(the carrier of V);
ex f st Sum(S) = f.(len S) & f.0 = 0.V & for j,v st j < len S &
v = S.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
hence thesis;
end;
Lm2: len F = 0 implies Sum(F) = 0.V
proof
assume len F = 0;
then F = <*>(the carrier of V);
hence thesis by Lm1;
end;
theorem Th12:
len F = len G & (for k,v st k in dom F & v = G.k holds F.k = a * v)
implies Sum(F) = a * Sum(G)
proof
defpred P[set] means for H,I st len H = len I & len H = $1 & (for k, v
st k in Seg len H & v = I.k holds H.k = a * v) holds Sum(H) = a * Sum(I);
A1: dom F = Seg len F by FINSEQ_1:def 3;
now
let n;
assume
A2: for H, I st len H = len I & len H = n & for k, v st k in Seg len H &
v = I.k holds H.k = a * v holds Sum(H) = a * Sum(I);
let H, I;
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k, v st k in Seg len H & v = I.k holds H.k = a * v;
reconsider p = H | (Seg n),q = I | (Seg n) as FinSequence of the carrier
of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12; then
A7: len q = n by A3,A4,FINSEQ_1:17;
A8: len p = n by A4,A6,FINSEQ_1:17;
A9:
now
len p <= len H by A4,A6,FINSEQ_1:17; then
A10: Seg len p c= Seg len H by FINSEQ_1:5;
A11: dom p = Seg n by A4,A6,FINSEQ_1:17;
let k, v;
assume that
A12: k in Seg len p and
A13: v = q.k;
dom q = Seg n by A3,A4,A6,FINSEQ_1:17;
then I.k = q.k by A8,A12,FUNCT_1:47;
then H.k = a * v by A5,A12,A13,A10;
hence p.k = a * v by A8,A12,A11,FUNCT_1:47;
end;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom H & n + 1 in dom I by A3,A4,FINSEQ_3:25;
then reconsider v1 = H.(n + 1),v2 = I.(n + 1) as Vector of V
by FUNCT_1:102;
A14: v1 = a * v2 by A4,A5,FINSEQ_1:4;
A15: dom q = Seg len q by FINSEQ_1:def 3;
dom p = Seg len p by FINSEQ_1:def 3;
hence Sum(H) = Sum(p) + v1 by A4,A8,RLVECT_1:38
.= a * Sum(q) + a * v2 by A2,A8,A7,A9,A14
.= a * (Sum(q) + v2) by VECTSP_1:def 14
.= a * Sum(I) by A3,A4,A7,A15,RLVECT_1:38;
end;
then
A16: for n st P[n] holds P[n+1];
now
let H, I;
assume that
A17: len H = len I and
A18: len H = 0 and
for k, v st k in Seg len H & v = I.k holds H.k = a * v;
AA: Sum(H) = 0.V by A18,Lm2;
Sum I = 0.V by A17,A18,Lm2;
hence Sum(H) = a * Sum(I) by VECTSP_1:14,AA;
end;
then
A19: P[0];
for n holds P[n] from NAT_1:sch 2(A19,A16);
hence thesis by A1;
end;
theorem
for V being Z_Module, a being Element of INT.Ring holds
a * Sum(<*>(the carrier of V)) = 0.V by Lm1,Th1;
theorem
for R being Ring,
V being LeftMod of R, a being Element of R,
v, u being Vector of V holds
a * Sum<* v,u *> = a * v + a * u
proof
let R be Ring;
let V be LeftMod of R, a be Element of R, v, u be Vector of V;
thus a * Sum<* v,u *> = a * (v + u) by RLVECT_1:45
.= a * v + a * u by VECTSP_1:def 14;
end;
theorem
for R being Ring
for V being LeftMod of R, a being Element of R, v, u, w being Vector of V
holds a * Sum<* v,u,w *> = a * v + a * u + a * w
proof
let R be Ring;
let V be LeftMod of R, a be Element of R, v, u, w be Vector of V;
thus a * Sum<* v,u,w *> = a * (v + u + w) by RLVECT_1:46
.= a * (v + u) + a * w by VECTSP_1:def 14
.= a * v + a * u + a * w by VECTSP_1:def 14;
end;
theorem
for V being LeftMod of INT.Ring, a being Element of INT.Ring,
v being Vector of V holds
(- a) * v = - a * v
proof
let V be LeftMod of INT.Ring,
a be Element of INT.Ring,
v be Vector of V;
thus (- a) * v = a * (- v) by Th5
.= - a * v by Th6;
end;
theorem
len F = len G & (for k st k in dom F holds G.k = a * F/.k )
implies Sum(G) = a * Sum(F)
proof
assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = a * F/.k;
A3: dom F = Seg len F & dom G = Seg len G by FINSEQ_1:def 3;
now
let k, v;
assume that
A4: k in dom G and
A5: v = F.k;
v = F/.k by A1,A3,A4,A5,PARTFUN1:def 6;
hence G.k = a * v by A1,A2,A3,A4;
end;
hence thesis by A1,Th12;
end;
begin :: 2. Submodules and cosets of submodules in Z-module
reserve R for Ring;
reserve V, X, Y for LeftMod of R;
reserve u, u1, u2, v, v1, v2 for Vector of V;
reserve a for Element of R;
reserve V1, V2, V3 for Subset of V;
reserve x for set;
theorem
V1 <> {} & V1 is linearly-closed implies 0.V in V1 by VECTSP_4:1;
theorem
V1 is linearly-closed implies for v st v in V1 holds - v in V1
by VECTSP_4:2;
theorem
V1 is linearly-closed implies for v, u st v in V1 & u in V1 holds v - u in V1
by VECTSP_4:3;
theorem
the carrier of V = V1 implies V1 is linearly-closed;
theorem
V1 is linearly-closed & V2 is linearly-closed &
V3 = {v + u : v in V1 & u in V2} implies
V3 is linearly-closed
proof
assume that
A1: V1 is linearly-closed & V2 is linearly-closed and
A2: V3 = {v + u : v in V1 & u in V2};
thus for v, u st v in V3 & u in V3 holds v + u in V3
proof
let v, u;
assume that
A3: v in V3 and
A4: u in V3;
consider v2, v1 such that
A5: v = v1 + v2 and
A6: v1 in V1 & v2 in V2 by A2,A3;
consider u2, u1 such that
A7: u = u1 + u2 and
A8: u1 in V1 & u2 in V2 by A2,A4;
A9: v + u = ((v1 + v2) + u1) + u2 by A5,A7,RLVECT_1:def 3
.= ((v1 + u1) + v2) + u2 by RLVECT_1:def 3
.= (v1 + u1) + (v2 + u2) by RLVECT_1:def 3;
v1 + u1 in V1 & v2 + u2 in V2 by A1,A6,A8;
hence thesis by A2,A9;
end;
let a, v;
assume v in V3;
then consider v2, v1 such that
A10: v = v1 + v2 and
A11: v1 in V1 & v2 in V2 by A2;
A12: a * v = a * v1 + a * v2 by A10,VECTSP_1:def 14;
a * v1 in V1 & a * v2 in V2 by A1,A11;
hence thesis by A2,A12;
end;
registration let R; let V;
cluster {0.V} -> linearly-closed for Subset of V;
coherence by VECTSP_4:4;
end;
registration let R; let V;
cluster linearly-closed for Subset of V;
existence
proof
take {0.V};
thus thesis;
end;
end;
registration let R; let V;
let V1,V2 be linearly-closed Subset of V;
cluster V1 /\ V2 -> linearly-closed for Subset of V;
coherence by VECTSP_4:7;
end;
definition
::$CD 2
end;
definition
let R be Ring;
let V be LeftMod of R;
mode Submodule of V is Subspace of V;
end;
reserve W, W1, W2 for Submodule of V;
reserve w, w1, w2 for Vector of W;
theorem
x in W1 & W1 is Submodule of W2 implies x in W2 by VECTSP_4:8;
theorem Th24:
for x being object holds x in W implies x in V by VECTSP_4:9;
theorem Th25:
w is Vector of V by VECTSP_4:10;
theorem
0.W = 0.V by VECTSP_4:def 2;
theorem
0.W1 = 0.W2 by VECTSP_4:12;
theorem
w1 = v & w2 = u implies w1 + w2 = v + u by VECTSP_4:13;
theorem
w = v implies a * w = a * v by VECTSP_4:14;
theorem
w = v implies - v = - w by VECTSP_4:15;
theorem
w1 = v & w2 = u implies w1 - w2 = v - u by VECTSP_4:16;
theorem Th32:
V is Submodule of V by VECTSP_4:24;
theorem Th33:
0.V in W by VECTSP_4:17;
theorem
0.W1 in W2 by VECTSP_4:18;
theorem
0.W in V by VECTSP_4:19;
theorem Th36:
u in W & v in W implies u + v in W by VECTSP_4:20;
theorem
v in W implies a * v in W by VECTSP_4:21;
theorem
v in W implies - v in W by VECTSP_4:22;
theorem Th39:
u in W & v in W implies u - v in W by VECTSP_4:23;
reserve D for non empty set;
reserve d1 for Element of D;
reserve A for BinOp of D;
reserve M for Function of [:the carrier of R,D:],D;
theorem Th40:
V1 = D & d1 = 0.V & A = (the addF of V) || V1 &
M = (the lmult of V) | [:the carrier of R,V1:] implies
ModuleStr (# D,A,d1,M #) is Submodule of V
proof
assume that
A1: V1 = D and
A2: d1 = 0.V and
A3: A = (the addF of V) || V1 and
A4: M = (the lmult of V) | [:the carrier of R,V1:];
reconsider W = ModuleStr (# D,A,d1,M #) as non empty
ModuleStr over R;
A5: for a being Element of R
for x being Vector of W holds a * x = (the lmult of V).(a,x)
proof
let a be Element of R;
let x be Vector of W;
thus a * x = (the lmult of V).[a,x] by A1,A4,FUNCT_1:49
.= (the lmult of V).(a,x);
end;
A6: for x, y being Vector of W holds x + y = (the addF of V).(x,y)
proof
let x, y be Vector of W;
thus x + y = (the addF of V) . [x,y] by A1,A3,FUNCT_1:49
.= (the addF of V).(x,y);
end;
A7: W is Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
proof
set MV = the lmult of V;
set AV = the addF of V;
thus W is Abelian
proof
let x, y be Vector of W;
reconsider x1 = x, y1 = y as Vector of V by A1,TARSKI:def 3;
thus x + y = x1 + y1 by A6
.= y1 + x1
.= y + x by A6;
end;
thus W is add-associative
proof
let x, y, z be Vector of W;
reconsider x1 = x, y1 = y, z1 = z as Vector of V by A1,TARSKI:def 3;
thus (x + y) + z = AV.(x + y,z1) by A6
.= (x1 + y1) + z1 by A6
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= AV.(x1,y + z) by A6
.= x + (y + z) by A6;
end;
thus W is right_zeroed
proof
let x be Vector of W;
reconsider y = x as Vector of V by A1,TARSKI:def 3;
thus x + 0.W = y + 0.V by A2,A6
.= x by RLVECT_1:4;
end;
thus W is right_complementable
proof
let x be Vector of W;
reconsider x1 = x as Vector of V by A1,TARSKI:def 3;
consider v such that
A8: x1 + v = 0.V by ALGSTR_0:def 11;
v = - x1 by A8,RLVECT_1:def 10
.= (- (1.R)) * x1 by Th2
.= (the lmult of V).((- (1.R)),x1)
.= (- (1.R)) * x by A5;
then reconsider y = v as Vector of W;
take y;
thus thesis by A2,A6,A8;
end;
thus for a being Element of R for x, y being Vector of W
holds a * (x + y) = a * x + a * y
proof
let a be Element of R;
let x, y be Vector of W;
reconsider x1 = x, y1 = y as Vector of V by A1,TARSKI:def 3;
a * (x + y) = MV.(a,x + y) by A5
.= a * (x1 + y1) by A6
.= a * x1 + a * y1 by VECTSP_1:def 14
.= AV.(MV.(a,x1),a * y) by A5
.= AV.(a * x, a * y) by A5
.= a * x + a * y by A6;
hence thesis;
end;
thus for a, b being Element of R
for x being Vector of W holds (a + b) * x = a * x + b * x
proof
let a, b be Element of R;
let x be Vector of W;
reconsider y = x as Vector of V by A1,TARSKI:def 3;
(a + b) * x = (a + b) * y by A5
.= a * y + b * y by VECTSP_1:def 15
.= AV.(MV.(a,y),b * x) by A5
.= AV.(a * x,b * x) by A5
.= a * x + b * x by A6;
hence thesis;
end;
thus for a, b being Element of R
for x being Vector of W holds (a * b) * x = a * (b * x)
proof
let a, b be Element of R;
let x be Vector of W;
reconsider y = x as Vector of V by A1,TARSKI:def 3;
reconsider a, b as Element of R;
(a * b) * x = (a * b) * y by A5
.= a * (b * y) by VECTSP_1:def 16
.= MV.(a,b * x) by A5
.= a * (b * x) by A5;
hence thesis;
end;
let x be Vector of W;
reconsider y = x as Vector of V by A1,TARSKI:def 3;
thus (1.R) * x = (the lmult of V).(1.R,y) by A5
.= (1.R) * y
.= x;
end;
0.W = 0.V by A2;
hence thesis by A1,A3,A4,A7,VECTSP_4:def 2;
end;
theorem
for R being Ring
for V,X being strict LeftMod of R st V is Submodule of X &
X is Submodule of V holds V = X by VECTSP_4:25;
theorem Th42:
V is Submodule of X & X is Submodule of Y implies V is Submodule of Y
by VECTSP_4:26;
theorem Th43:
the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2
by VECTSP_4:27;
theorem
(for v st v in W1 holds v in W2) implies W1 is Submodule of W2
by VECTSP_4:28;
registration
let R be Ring;
let V be LeftMod of R;
cluster strict for Submodule of V;
existence
proof
the carrier of V is Subset of V iff the carrier of V c= the carrier of V;
then reconsider V1 = the carrier of V as Subset of V;
the addF of V = (the addF of V) ||V1 & the lmult of V = (the lmult of V)
| [: the carrier of R,V1:] by RELSET_1:19;
then ModuleStr(#the carrier of V,the addF of V,0.V,the lmult of V #)
is Submodule of V by Th40;
hence thesis;
end;
end;
theorem Th45:
for W1, W2 being strict Submodule of V holds
the carrier of W1 = the carrier of W2 implies W1 = W2 by VECTSP_4:29;
theorem Th46:
for W1, W2 being strict Submodule of V holds
(for v holds v in W1 iff v in W2) implies W1 = W2 by VECTSP_4:30;
theorem
for V being strict LeftMod of R, W being strict Submodule of V holds
the carrier of W = the carrier of V implies W = V by VECTSP_4:31;
theorem
for V being strict LeftMod of R, W being strict Submodule of V holds
(for v being Vector of V holds v in W iff v in V) implies W = V
proof
let V be strict LeftMod of R, W be strict Submodule of V;
assume
A1: for v being Vector of V holds v in W iff v in V;
V is Submodule of V by Th32;
hence thesis by A1,Th46;
end;
theorem
the carrier of W = V1 implies V1 is linearly-closed by VECTSP_4:33;
theorem
V1 <> {} & V1 is linearly-closed implies
ex W being strict Submodule of V st V1 = the carrier of W by VECTSP_4:34;
theorem
(0).W = (0).V by VECTSP_4:36;
theorem
(0).W1 = (0).W2 by VECTSP_4:37;
theorem
(0).W is Submodule of V by Th42;
theorem Th54:
(0).V is Submodule of W by VECTSP_4:39;
theorem
(0).W1 is Submodule of W2 by VECTSP_4:40;
theorem
for V being LeftMod of R holds V is Submodule of (Omega).V by VECTSP_4:41;
definition
::$CD 4
end;
reserve B,C for Coset of W;
theorem
0.V in v + W iff v in W by VECTSP_4:43;
theorem Th58:
v in v + W by VECTSP_4:44;
theorem
0.V + W = the carrier of W by VECTSP_4:45;
theorem
v + (0).V = {v} by VECTSP_4:46;
theorem
v + (Omega).V = the carrier of V by VECTSP_4:47;
theorem
0.V in v + W iff v + W = the carrier of W by VECTSP_4:48;
theorem
v in W iff v + W = the carrier of W by VECTSP_4:49;
theorem
v in W implies (a * v) + W = the carrier of W by VECTSP_4:50;
theorem
u in W iff v + W = (v + u) + W by VECTSP_4:53;
theorem
u in W iff v + W = (v - u) + W by VECTSP_4:54;
theorem
v in u + W iff u + W = v + W by VECTSP_4:55;
theorem
u in v1 + W & u in v2 + W implies v1 + W = v2 + W by VECTSP_4:56;
theorem
v in W implies a * v in v + W by VECTSP_4:58;
theorem
u + v in v + W iff u in W by VECTSP_4:60;
theorem
v - u in v + W iff u in W by VECTSP_4:61;
theorem
u in v + W iff ex v1 st v1 in W & u = v + v1
proof
thus u in v + W implies ex v1 st v1 in W & u = v + v1
proof
assume u in v + W;
then ex v1 st u = v + v1 & v1 in W;
hence thesis;
end;
given v1 such that
A1: v1 in W & u = v + v1;
thus thesis by A1;
end;
theorem
u in v + W iff ex v1 st v1 in W & u = v - v1 by VECTSP_4:62;
theorem
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W by VECTSP_4:63;
theorem
v + W = u + W implies ex v1 st v1 in W & v + v1 = u by VECTSP_4:64;
theorem
v + W = u + W implies ex v1 st v1 in W & v - v1 = u by VECTSP_4:65;
theorem
for W1, W2 being strict Submodule of V st v + W1 = v + W2 holds W1 = W2
by VECTSP_4:66;
theorem
for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds W1 = W2
by VECTSP_4:67;
theorem
C is linearly-closed iff C = the carrier of W by VECTSP_4:69;
theorem
for W1, W2 being strict Submodule of V, C1 being Coset of W1,
C2 being Coset of W2 st C1 = C2 holds W1 = W2 by VECTSP_4:70;
theorem
{v} is Coset of (0).V by VECTSP_4:71;
theorem
V1 is Coset of (0).V implies ex v st V1 = {v} by VECTSP_4:72;
theorem
the carrier of W is Coset of W by VECTSP_4:73;
theorem
the carrier of V is Coset of (Omega).V by VECTSP_4:74;
theorem
V1 is Coset of (Omega).V implies V1 = the carrier of V by VECTSP_4:75;
theorem
0.V in C iff C = the carrier of W by VECTSP_4:76;
theorem
u in C iff C = u + W by VECTSP_4:77;
theorem
u in C & v in C implies ex v1 st v1 in W & u + v1 = v by VECTSP_4:78;
theorem
u in C & v in C implies ex v1 st v1 in W & u - v1 = v by VECTSP_4:79;
theorem
(ex C st v1 in C & v2 in C) iff v1 - v2 in W by VECTSP_4:80;
theorem
u in B & u in C implies B = C by VECTSP_4:81;
begin :: 3. Operations on submodules in Z-module
reserve V for LeftMod of R;
reserve W, W1, W2, W3 for Submodule of V;
reserve u, u1, u2, v, v1, v2 for Vector of V;
reserve a, a1, a2 for Element of R;
reserve X, Y, y, y1, y2 for set;
definition let GF be Ring;
let M be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF;
let W1, W2 be Subspace of M;
redefine func W1 + W2; :: redefines + (VECTSP_5, definition)
commutativity by VECTSP_5:5;
end;
theorem Th92:
x in W1 + W2 iff ex v1, v2 st v1 in W1 & v2 in W2 & x = v1 + v2
by VECTSP_5:1;
theorem
v in W1 or v in W2 implies v in W1 + W2 by VECTSP_5:2;
theorem Th94:
for x being object holds x in W1 /\ W2 iff x in W1 & x in W2 by VECTSP_5:3;
Lm6: the carrier of W1 c= the carrier of W1 + W2
proof
let x be object;
set A = {v + u : v in W1 & u in W2};
assume x in the carrier of W1;
then reconsider v = x as Element of W1;
reconsider v as Vector of V by Th25;
A1: v = v + 0.V by RLVECT_1:4;
v in W1 & 0.V in W2 by Th33;
then x in A by A1;
hence thesis by VECTSP_5:def 1;
end;
theorem
for W being strict Submodule of V holds W + W = W by VECTSP_5:4;
theorem
W1 + (W2 + W3) = (W1 + W2) + W3 by VECTSP_5:6;
theorem
W1 is Submodule of W1 + W2 by VECTSP_5:7;
theorem Th98:
for W2 being strict Submodule of V holds
W1 is Submodule of W2 iff W1 + W2 = W2 by VECTSP_5:8;
theorem Th99:
for W being strict Submodule of V holds (0).V + W = W by VECTSP_5:9;
theorem
(0).V + (Omega).V = the ModuleStr of V by VECTSP_5:10;
theorem Th101:
(Omega).V + W = the ModuleStr of V by VECTSP_5:11;
theorem
for V being strict LeftMod of R holds (Omega).V + (Omega).V = V by Th101;
theorem
for W being strict Submodule of V holds W /\ W = W by VECTSP_5:13;
theorem
W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 by VECTSP_5:14;
Lm8: the carrier of W1 /\ W2 c= the carrier of W1
proof
the carrier of W1 /\ W2
= (the carrier of W1) /\ (the carrier of W2) by VECTSP_5:def 2;
hence thesis by XBOOLE_1:17;
end;
theorem
W1 /\ W2 is Submodule of W1 by VECTSP_5:15;
theorem Th106:
for W1 being strict Submodule of V holds W1 is Submodule of W2 iff
W1 /\ W2 = W1 by VECTSP_5:16;
theorem Th107:
(0).V /\ W = (0).V by VECTSP_5:20;
theorem
(0).V /\ (Omega).V = (0).V by Th107;
theorem Th109:
for W being strict Submodule of V holds (Omega).V /\ W = W by VECTSP_5:21;
theorem
for V being strict LeftMod of R holds (Omega).V /\ (Omega).V = V by Th109;
Lm9: the carrier of W1 /\ W2 c= the carrier of W1 + W2
proof
the carrier of W1 /\ W2 c= the carrier of W1 &
the carrier of W1 c= the carrier of W1 + W2 by Lm6,Lm8;
hence thesis;
end;
theorem
W1 /\ W2 is Submodule of W1 + W2 by Lm9,Th43;
Lm10: the carrier of (W1 /\ W2) + W2 = the carrier of W2
proof
thus the carrier of (W1 /\ W2) + W2 c= the carrier of W2
proof
let x be object;
assume x in the carrier of (W1 /\ W2) + W2;
then x in {u + v where v,u: u in W1 /\ W2 & v in W2} by VECTSP_5:def 1;
then consider v,u such that
A1: x = u + v and
A2: u in W1 /\ W2 and
A3: v in W2;
u in W2 by A2,Th94;
then u + v in W2 by A3,Th36;
hence thesis by A1;
end;
let x be object;
the carrier of W2 c= the carrier of (W1 /\ W2) + W2 by Lm6;
hence thesis;
end;
theorem
for W2 being strict Submodule of V
holds (W1 /\ W2) + W2 = W2 by Lm10,Th45;
Lm11: the carrier of W1 /\ (W1 + W2) = the carrier of W1
proof
thus the carrier of W1 /\ (W1 + W2) c= the carrier of W1
proof
let x be object;
assume
A1: x in the carrier of W1 /\ (W1 + W2);
the carrier of W1 /\ (W1 + W2)
= (the carrier of W1) /\ (the carrier of W1 + W2) by VECTSP_5:def 2;
hence thesis by A1,XBOOLE_0:def 4;
end;
let x be object;
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider x1 = x as Element of V by A2;
A3: x1 + 0.V = x1 & 0.V in W2 by Th33,RLVECT_1:4;
x in W1 by A2;
then x in {u + v where v,u: u in W1 & v in W2} by A3;
then x in the carrier of W1 + W2 by VECTSP_5:def 1;
then x in (the carrier of W1) /\ (the carrier of W1 + W2)
by A2,XBOOLE_0:def 4;
hence thesis by VECTSP_5:def 2;
end;
theorem
for W1 being strict Submodule of V holds
W1 /\ (W1 + W2) = W1 by Lm11,Th45;
Lm12: the carrier of (W1 /\ W2) + (W2 /\ W3) c=
the carrier of W2 /\ (W1 + W3)
proof
let x be object;
assume x in the carrier of (W1 /\ W2) + (W2 /\ W3);
then x in {u + v where v,u: u in W1 /\ W2 & v in W2 /\ W3} by VECTSP_5:def 1;
then consider v,u such that
A1: x = u + v and
A2: u in W1 /\ W2 & v in W2 /\ W3;
u in W2 & v in W2 by A2,Th94;
then
A3: x in W2 by A1,Th36;
u in W1 & v in W3 by A2,Th94;
then x in W1 + W3 by A1,Th92;
then x in W2 /\ (W1 + W3) by A3,Th94;
hence thesis;
end;
theorem
(W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3) by Lm12,Th43;
Lm13: W1 is Submodule of W2 implies
the carrier of W2 /\ (W1 + W3) = the carrier of (W1 /\ W2) + (W2 /\ W3)
by VECTSP_5:27;
theorem
W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
by Lm13,Th45;
Lm14: the carrier of W2 + (W1 /\ W3) c=
the carrier of (W1 + W2) /\ (W2 + W3)
proof
let x be object;
assume x in the carrier of W2 + (W1 /\ W3);
then x in {u + v where v,u: u in W2 & v in W1 /\ W3} by VECTSP_5:def 1;
then consider v,u such that
A1: x = u + v & u in W2 and
A2: v in W1 /\ W3;
v in W3 by A2,Th94;
then x in {u1 + u2 where u2,u1: u1 in W2 & u2 in W3} by A1;
then
A3: x in the carrier of W2 + W3 by VECTSP_5:def 1;
v in W1 by A2,Th94;
then x in {v1 + v2 where v2,v1: v1 in W1 & v2 in W2} by A1;
then x in the carrier of W1 + W2 by VECTSP_5:def 1;
then x in (the carrier of W1 + W2) /\ (the carrier of W2 + W3) by A3,
XBOOLE_0:def 4;
hence thesis by VECTSP_5:def 2;
end;
theorem
W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3) by Lm14,Th43;
Lm15: W1 is Submodule of W2 implies
the carrier of W2 + (W1 /\ W3) = the carrier of (W1 + W2) /\ (W2 + W3)
proof
reconsider V2 = the carrier of W2 as Subset of V by VECTSP_4:def 2;
A1: V2 is linearly-closed by VECTSP_4:33;
assume W1 is Submodule of W2; then
A2: the carrier of W1 c= the carrier of W2 by VECTSP_4:def 2;
thus the carrier of W2 + (W1 /\ W3) c= the carrier of (W1 + W2) /\ (W2 + W3)
by Lm14;
let x be object;
assume x in the carrier of (W1 + W2) /\ (W2 + W3);
then x in (the carrier of W1 + W2) /\ (the carrier of W2 + W3)
by VECTSP_5:def 2;
then x in the carrier of W1 + W2 by XBOOLE_0:def 4;
then x in {u1 + u2 where u2,u1: u1 in W1 & u2 in W2} by VECTSP_5:def 1;
then consider u2, u1 such that
A3: x = u1 + u2 and
A4: u1 in W1 & u2 in W2;
u1 + u2 in V2 by A2,A1,A4;
then
A5: u1 + u2 in W2;
0.V in W1 /\ W3 & (u1 + u2) + 0.V = u1 + u2 by Th33,RLVECT_1:4;
then x in {u + v where v,u: u in W2 & v in W1 /\ W3} by A3,A5;
hence thesis by VECTSP_5:def 1;
end;
theorem
W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
by Lm15,Th45;
theorem
W1 is strict Submodule of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3
by VECTSP_5:30;
theorem
for W1,W2 being strict Submodule of V holds W1 + W2 = W2 iff W1 /\ W2 = W1
proof
let W1,W2 be strict Submodule of V;
W1 + W2 = W2 iff W1 is Submodule of W2 by Th98;
hence thesis by Th106;
end;
theorem
for W2,W3 being strict Submodule of V holds W1 is Submodule of W2
implies W1 + W3 is Submodule of W2 + W3 by VECTSP_5:32;
theorem
(ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2))
iff W1 is Submodule of W2 or W2 is Submodule of W1 by VECTSP_5:35;
notation let GF be Ring;
let V be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
scalar-unital non empty ModuleStr over GF;
synonym Submodules V for Subspaces(V);
end;
registration let R,V;
cluster Submodules(V) -> non empty;
coherence;
end;
theorem
for V being strict LeftMod of R holds V in Submodules(V)
proof
let V be strict LeftMod of R;
(Omega).V in Submodules(V) by VECTSP_5:def 3;
hence thesis;
end;
Lm16: for V being LeftMod of R, W being strict Submodule of V holds
(for v being Vector of V holds v in W) implies W = the ModuleStr of V
proof
let V be LeftMod of R, W be strict Submodule of V;
assume for v being Vector of V holds v in W;
then for v be Vector of V holds (v in W iff v in (Omega).V);
hence thesis by Th46;
end;
Lm17: for V being LeftMod of R, W1,W2 being Submodule of V holds
W1 + W2 = the ModuleStr of V
iff for v being Vector of V ex v1,v2 being Vector of V
st v1 in W1 & v2 in W2 & v = v1 + v2
proof
let V be LeftMod of R, W1,W2 be Submodule of V;
thus W1 + W2 = the ModuleStr of V implies
for v being Vector of V
ex v1, v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2
by RLVECT_1:1,Th92;
assume
A1: for v being Vector of V ex v1, v2 being Vector of V
st v1 in W1 & v2 in W2 & v = v1 + v2;
now
let u be Vector of V;
ex v1, v2 being Vector of V st v1 in W1 & v2 in W2 & u = v1 + v2 by A1;
hence u in W1 + W2 by Th92;
end;
hence thesis by Lm16;
end;
definition
::$CD 3
let R;
let V be LeftMod of R;
let W be Submodule of V;
attr W is with_Linear_Compl means
ex C being Submodule of V st V is_the_direct_sum_of C,W;
end;
registration
let R;
let V be LeftMod of R;
cluster with_Linear_Compl for Submodule of V;
correctness
proof
V is_the_direct_sum_of (0).V,(Omega).V by Th99,Th107;
then (Omega).V is with_Linear_Compl;
hence thesis;
end;
end;
definition
let R;
let V be LeftMod of R;
let W be Submodule of V;
assume A1: W is with_Linear_Compl;
mode Linear_Compl of W -> Submodule of V means :Def19:
V is_the_direct_sum_of it,W;
existence by A1;
end;
theorem
for W1, W2 being Submodule of V holds V
is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1
proof
let W1, W2 be Submodule of V;
assume V is_the_direct_sum_of W1,W2;
then A1:V is_the_direct_sum_of W2,W1 by VECTSP_5:41;
then W1 is with_Linear_Compl;
hence thesis by Def19,A1;
end;
theorem Th124:
for W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W holds
V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L
proof
let W be with_Linear_Compl Submodule of V,
L be Linear_Compl of W;
thus V is_the_direct_sum_of L,W by Def19;
hence thesis by VECTSP_5:41;
end;
theorem
for W being with_Linear_Compl Submodule of V, L being
Linear_Compl of W holds W + L = the ModuleStr of V
proof
let W be with_Linear_Compl Submodule of V,
L be Linear_Compl of W;
V is_the_direct_sum_of W,L by Th124;
hence W + L = the ModuleStr of V;
end;
theorem
for W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W holds W /\ L = (0).V
proof
let W be with_Linear_Compl Submodule of V,
L be Linear_Compl of W;
V is_the_direct_sum_of W,L by Th124;
hence W /\ L = (0).V;
end;
theorem
V is_the_direct_sum_of W1,W2
implies V is_the_direct_sum_of W2,W1 by VECTSP_5:41;
theorem
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W holds W is Linear_Compl of L
proof
let V be Z_Module, W be with_Linear_Compl Submodule of V,
L be Linear_Compl of W;
V is_the_direct_sum_of L,W by Def19; then
A1: V is_the_direct_sum_of W,L by VECTSP_5:41;
then L is with_Linear_Compl;
hence thesis by Def19,A1;
end;
theorem Th129:
for V being Z_Module holds V is_the_direct_sum_of (0).V, (Omega).V &
V is_the_direct_sum_of (Omega).V,(0).V
proof
let V be Z_Module;
V is_the_direct_sum_of (0).V, (Omega).V by Th99,Th107;
hence thesis by VECTSP_5:41;
end;
theorem
for V being Z_Module holds (0).V is Linear_Compl of (Omega).V &
(Omega).V is Linear_Compl of (0).V
proof
let V be Z_Module;
A1: V is_the_direct_sum_of (0).V,(Omega).V &
V is_the_direct_sum_of (Omega).V, (0).V by Th129;
then
A2: (Omega).V is with_Linear_Compl;
(0).V is with_Linear_Compl by A1;
hence thesis by Def19,A1,A2;
end;
reserve C for Coset of W;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;
theorem
C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2 by VECTSP_5:45;
Lm18: ex C st v in C
proof
reconsider C = v + W as Coset of W by VECTSP_4:def 6;
take C;
thus thesis by Th58;
end;
theorem
for V being Z_Module, W1, W2 being Submodule of V holds V
is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1, C2 being Coset of W2
ex v being Vector of V st C1 /\ C2 = {v} by VECTSP_5:46;
theorem
for V being LeftMod of R, W1,W2 being Submodule of V holds
W1 + W2 = the ModuleStr of V
iff for v being Vector of V ex v1, v2 being Vector of V
st v1 in W1 & v2 in W2 & v = v1 + v2 by Lm17;
theorem
V is_the_direct_sum_of W1,W2 & v1 + v2 = u1 + u2 & v1 in
W1 & u1 in W1 & v2 in W2 & u2 in W2 implies v1 = u1 & v2 = u2
by VECTSP_5:48;
theorem
V = W1 + W2 & (ex v st for v1,v2,u1,u2 st v1 + v2 = u1 + u2 &
v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2) implies
V is_the_direct_sum_of W1,W2
proof
assume
A1: V = W1 + W2;
the carrier of (0).V = {0.V} & (0).V is Submodule of W1 /\ W2
by Th54,VECTSP_4:def 3; then
A2: {0.V} c= the carrier of W1 /\ W2 by VECTSP_4:def 2;
given v such that
A3: for v1, v2, u1, u2 st v1 + v2 = u1 + u2 & v1 in W1 & u1 in W1 &
v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2;
assume not thesis;
then the carrier of W1 /\ W2 <> {0.V} by VECTSP_4:def 3,A1;
then {0.V} c< the carrier of W1 /\ W2 by A2;
then consider x being object such that
A4: x in the carrier of W1 /\ W2 and
A5: not x in {0.V} by XBOOLE_0:6;
A6: x <> 0.V by A5,TARSKI:def 1;
A7: x in W1 /\ W2 by A4;
then x in V by Th24;
then reconsider u = x as Vector of V;
consider v1, v2 such that
A8: v1 in W1 and
A9: v2 in W2 and
A10: v = v1 + v2 by A1,Lm17;
A11: v = v1 + v2 + 0.V by A10,RLVECT_1:4
.= (v1 + v2) + (u - u) by RLVECT_1:15
.= ((v1 + v2) + u) - u by RLVECT_1:def 3
.= ((v1 + u) + v2) - u by RLVECT_1:def 3
.= (v1 + u) + (v2 - u) by RLVECT_1:def 3;
x in W2 by A7,Th94;
then
A12: v2 - u in W2 by A9,Th39;
x in W1 by A7,Th94;
then v1 + u in W1 by A8,Th36;
then v2 - u = v2 by A3,A8,A9,A10,A11,A12
.= v2 - 0.V by RLVECT_1:13;
hence thesis by A6,RLVECT_1:23;
end;
definition
::$CD
end;
theorem Th136:
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2
by VECTSP_5:50;
theorem Th137:
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1
by VECTSP_5:51;
theorem
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V,
t being Element of [:the carrier of V, the carrier of V:]
holds t`1 + t`2 = v & t`1 in W & t`2 in L implies t = v |-- (W,L)
proof
let V be Z_Module, W be with_Linear_Compl Submodule of V,
L be Linear_Compl of W;
V is_the_direct_sum_of W,L by Th124;
hence thesis by VECTSP_5:def 6;
end;
theorem
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V holds
(v |-- (W,L))`1 + (v |-- (W,L))`2 = v
proof
let V be Z_Module, W be with_Linear_Compl Submodule of V,
L be Linear_Compl of W;
V is_the_direct_sum_of W,L by Th124;
hence thesis by VECTSP_5:def 6;
end;
theorem
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V holds
(v |-- (W,L))`1 in W & (v |-- (W,L))`2 in L
proof
let V be Z_Module, W be with_Linear_Compl Submodule of V,
L be Linear_Compl of W;
V is_the_direct_sum_of W,L by Th124;
hence thesis by VECTSP_5:def 6;
end;
theorem
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V holds
(v |-- (W,L))`1 = (v |-- (L,W))`2 by Th124,Th136;
theorem
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W, v being Vector of V holds
(v |-- (W,L))`2 = (v |-- (L,W))`1 by Th124,Th137;
reserve A1,A2,B for Element of Submodules(V);
theorem Th143:
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice
by VECTSP_5:57;
registration let R; let V;
cluster LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #)
-> Lattice-like;
coherence by Th143;
end;
theorem Th144:
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is lower-bounded by VECTSP_5:58;
theorem Th145:
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is upper-bounded by VECTSP_5:59;
theorem
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is 01_Lattice
proof
let V be Z_Module;
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is lower-bounded
upper-bounded Lattice by Th144,Th145;
hence thesis;
end;
theorem
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is modular by VECTSP_5:61;
theorem
for V being Z_Module, W1,W2,W3 being strict Submodule of V holds
W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3
proof
let V be Z_Module, W1,W2,W3 be strict Submodule of V;
set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
reconsider A = W1, B = W2, C = W3, AC = W1 /\ W3, BC = W2 /\ W3
as Element of S by VECTSP_5:def 3;
assume
A1: W1 is Submodule of W2;
A "\/" B = W1 + W2 by VECTSP_5:def 7
.= B by A1,Th98;
then A [= B;
then A "/\" C [= B "/\" C by LATTICES:9;
then
A2: (A "/\" C) "\/" (B "/\" C) = (B "/\" C);
A3: B "/\" C = W2 /\ W3 by VECTSP_5:def 8;
(A "/\" C) "\/" (B "/\" C) = SubJoin(V).(SubMeet(V).(A,C),BC)
by VECTSP_5:def 8
.= SubJoin(V).(AC,BC) by VECTSP_5:def 8
.= (W1 /\ W3) + (W2 /\ W3) by VECTSP_5:def 7;
hence thesis by A2,A3,Th98;
end;
theorem
for V being Z_Module, W being strict Submodule of V holds
(for v being Vector of V holds v in W) implies
W = the ModuleStr of V by Lm16;
theorem
ex C st v in C by Lm18;
begin :: 4.Transformation of Abelian group to Z-module
definition
let AG be non empty addLoopStr;
func Int-mult-left(AG) -> Function of
[:the carrier of INT.Ring,
the carrier of AG:], the carrier of AG means :Def23:
for i being Element of INT.Ring, a being Element of AG holds
(i >= 0 implies it.(i,a) = (Nat-mult-left(AG)).(i,a)) &
(i < 0 implies it.(i,a) = (Nat-mult-left(AG)).(-i,-a));
existence
proof
defpred P[Element of the carrier of INT.Ring,
Element of AG,Element of AG] means
($1 >= 0 implies $3 = (Nat-mult-left(AG)).($1,$2)) &
($1 < 0 implies $3 = (Nat-mult-left(AG)).(-$1,-$2));
A1: for x being Element of the carrier of INT.Ring
for y being Element of AG
ex z being Element of AG st P[x,y,z]
proof
let x be Element of the carrier of INT.Ring, y be Element of AG;
reconsider xx = x as Element of INT;
per cases;
suppose x >= 0; then
reconsider x0=x as Element of NAT by INT_1:3;
reconsider z = (Nat-mult-left(AG)).(x0,y) as Element of AG;
P[x,y,z];
hence thesis;
end;
suppose a2: x < 0; then
reconsider x0=-xx as Element of NAT by INT_1:3;
reconsider z = (Nat-mult-left(AG)).(x0,-y) as Element of AG;
T1: (x >= 0 implies z = (Nat-mult-left(AG)).(x,y)) by a2;
P[x,y,z] by T1;
hence thesis;
end;
end;
consider f being Function of [:the carrier of INT.Ring,
the carrier of AG:],the carrier of AG such that
A3: for x being Element of the carrier of INT.Ring
for y being Element of the carrier of AG
holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
take f;
thus thesis by A3;
end;
uniqueness
proof
let f1, f2 be Function of [:the carrier of INT.Ring,the carrier of AG:],
the carrier of AG;
assume
A4: for i being Element of INT.Ring,a being Element of AG holds
(i >= 0 implies f1.(i,a) = (Nat-mult-left(AG)).(i,a)) &
(i < 0 implies f1.(i,a) = (Nat-mult-left(AG)).(-i,-a));
assume
A5: for i being Element of INT.Ring,a being Element of AG holds
(i >= 0 implies f2.(i,a) = (Nat-mult-left(AG)).(i,a)) &
(i < 0 implies f2.(i,a) = (Nat-mult-left(AG)).(-i,-a));
for x, y being set st x in INT & y in the carrier of AG
holds f1.(x,y)= f2.(x,y)
proof let x, y be set;
assume A6: x in INT & y in the carrier of AG; then
reconsider x0=x as Element of INT;
reconsider x1=x as Element of INT.Ring by A6;
reconsider y0=y as Element of AG by A6;
per cases;
suppose A7: 0 <= x0;
hence f1.(x,y) = (Nat-mult-left(AG)).(x0,y0) by A4
.= f2.(x,y) by A5,A7;
end;
suppose A8: 0 > x0;
hence f1.(x,y) = (Nat-mult-left(AG)).(-x1,-y0) by A4
.= f2.(x,y) by A5,A8;
end;
end;
hence f1=f2;
end;
end;
theorem
for R being non empty addLoopStr, a being Element of R,
i be Element of INT.Ring, i1 be Element of NAT st i=i1 holds
(Int-mult-left(R)).(i,a) = i1 * a by Def23;
theorem Th152:
for R being non empty addLoopStr, a being Element of R,
i be Integer st i=0 holds
(Int-mult-left(R)).(i,a) = 0.R
proof
let R be non empty addLoopStr,
a be Element of R, i be Integer;
assume i=0;
hence (Int-mult-left(R)).(i,a) = 0 * a by Def23
.=0.R by BINOM:12;
end;
theorem Th153:
for R being add-associative right_zeroed right_complementable
non empty addLoopStr,
i be Element of NAT holds
(Nat-mult-left(R)).(i,0.R) = 0.R
proof
let R be add-associative right_zeroed right_complementable
non empty addLoopStr,
i be Element of NAT;
defpred P[Nat] means (Nat-mult-left(R)).($1,0.R) = 0.R;
A1: P[0] by BINOM:def 3;
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A3:P[n];
(Nat-mult-left(R)).(n+1,0.R) = 0.R + 0.R by A3,BINOM:def 3
.= 0.R by RLVECT_1:4;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th154:
for R being add-associative right_zeroed right_complementable
non empty addLoopStr,
i be Element of INT.Ring holds
(Int-mult-left(R)).(i,0.R) = 0.R
proof
let R be add-associative right_zeroed right_complementable
non empty addLoopStr,
i be Element of INT.Ring;
reconsider ii = i as Element of INT;
per cases;
suppose 0 <= i; then
reconsider i1=i as Element of NAT by INT_1:3;
thus (Int-mult-left(R)).(i,0.R) = (Nat-mult-left(R)).(i1,0.R) by Def23
.=0.R by Th153;
end;
suppose A1: 0 > i; then
reconsider i1=-ii as Element of NAT by INT_1:3;
thus (Int-mult-left(R)).(i,0.R) = (Nat-mult-left(R)).(-i,-(0.R))
by Def23,A1
.= (Nat-mult-left(R)).(i1,0.R) by RLVECT_1:12
.=0.R by Th153;
end;
end;
theorem Th155:
for R being right_zeroed non empty addLoopStr, a being Element of R,
i be Integer st i = 1
holds (Int-mult-left(R)).(i,a) = a
proof
let R be right_zeroed non empty addLoopStr,
a be Element of R,
i be Integer;
assume i=1;
hence (Int-mult-left(R)).(i,a) = 1 * a by Def23
.= a by BINOM:13;
end;
theorem Th156:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j, k being Element of NAT
st i <= j & k = j-i holds
(Nat-mult-left(R)).(k,a)
= (Nat-mult-left(R)).(j,a) - (Nat-mult-left(R)).(i,a)
proof
let R be Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a being Element of R, i, j, k being Element of NAT;
assume A1: i <= j & k = j-i;
A2:j*a = (k+i)*a by A1
.= k*a + i*a by BINOM:15;
thus (Nat-mult-left(R)).(j,a)-(Nat-mult-left(R)).(i,a)
= (k*a) +((i*a) -(i*a)) by A2,RLVECT_1:28
.= (k*a) + 0.R by RLVECT_1:15
.= (Nat-mult-left(R)).(k,a) by RLVECT_1:4;
end;
theorem Th157:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i being Element of NAT
holds -(Nat-mult-left(R)).(i,a) = (Nat-mult-left(R)).(i,-a)
proof
let R be Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i being Element of NAT;
defpred P[Nat] means
(Nat-mult-left(R)).($1,a) + (Nat-mult-left(R)).($1,-a) =0.R;
A1: P[0]
proof
(Nat-mult-left(R)).(0,a) + (Nat-mult-left(R)).(0,-a)
= 0.R + (Nat-mult-left(R)).(0,-a) by BINOM:def 3
.= 0.R + 0.R by BINOM:def 3
.= 0.R by RLVECT_1:4;
hence thesis;
end;
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A3:P[n];
(Nat-mult-left(R)).(n+1,a) + (Nat-mult-left(R)).(n+1,-a)
=a + (Nat-mult-left(R)).(n,a) + (Nat-mult-left(R)).(n+1,-a)
by BINOM:def 3
.= a + (Nat-mult-left(R)).(n,a) + (-a + (Nat-mult-left(R)).(n,-a))
by BINOM:def 3
.= a + (Nat-mult-left(R)).(n,a) + (Nat-mult-left(R)).(n,-a) + -a
by RLVECT_1:def 3
.= a + ((Nat-mult-left(R)).(n,a) + (Nat-mult-left(R)).(n,-a)) + -a
by RLVECT_1:def 3
.= a + -a by A3,RLVECT_1:4
.= 0.R by RLVECT_1:5;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2); then
(Nat-mult-left(R)).(i,a) + (Nat-mult-left(R)).(i,-a) =0.R;
hence thesis by RLVECT_1:6;
end;
theorem Th158:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT.Ring
st i in NAT & not j in NAT
holds (Int-mult-left(R)).(i+j,a)
= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a)
proof
let R be Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a be Element of R, i, j be Element of INT.Ring;
reconsider jj = j, ii = i, ij = i+j as Element of INT;
assume A1: i in NAT & not j in NAT; then
reconsider i1=i as Element of NAT;
A2: jj < 0 by A1,INT_1:3; then
reconsider j1=-jj as Element of NAT by INT_1:3;
per cases;
suppose A4: j1 <= i1;
reconsider k1=i1-j1 as Element of NAT by A4,INT_1:5;
set IT = Int-mult-left(R);
W1: (Int-mult-left(R)).(jj,a) = (Nat-mult-left(R)).(-j,-a) by A2,Def23;
thus (Int-mult-left(R)).(i+j,a) = (Nat-mult-left(R)).(k1,a) by Def23
.= (Nat-mult-left(R)).(i1,a) - (Nat-mult-left(R)).(j1,a) by Th156,A4
.=(Nat-mult-left(R)).(i1,a) + (Nat-mult-left(R)).(j1,-a) by Th157
.=(Int-mult-left(R)).(i,a) + (Nat-mult-left(R)).(j1,-a) by Def23
.=(Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a) by W1;
end;
suppose A5: j1 > i1; then
reconsider k1=j1-i1 as Element of NAT by INT_1:5;
A6: i1-j1 < 0 by A5,XREAL_1:49;
Z1: (Int-mult-left(R)).(j,a) = (Nat-mult-left(R)).(-j,-a) by Def23,A2;
thus (Int-mult-left(R)).(i+j,a)
= (Nat-mult-left(R)).(-(i+j),-a) by A6,Def23
.= (Nat-mult-left(R)).(k1,-a)
.= (Nat-mult-left(R)).(j1,-a) - (Nat-mult-left(R)).(i1,-a)
by Th156,A5
.=(Nat-mult-left(R)).(j1,-a) + (Nat-mult-left(R)).(i1,-(-a))
by Th157
.=(Nat-mult-left(R)).(j1,-a) + (Nat-mult-left(R)).(i1,a)
by RLVECT_1:17
.=(Int-mult-left(R)).(j,a) + (Int-mult-left(R)).(i,a)
by Def23,Z1
.=(Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a);
end;
end;
theorem Th159:
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a being Element of R, i, j being Element of INT.Ring
holds (Int-mult-left(R)).(i+j,a)
= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a)
proof
let R be Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a be Element of R, i, j be Element of INT.Ring;
reconsider ii = i, jj = j as Element of INT;
per cases;
suppose A1: i in NAT & j in NAT; then
reconsider i1=i as Element of NAT;
reconsider j1=j as Element of NAT by A1;
thus (Int-mult-left(R)).(i+j,a)
= (Nat-mult-left(R)).(i1+j1,a) by Def23
.= (i1+j1)*a
.= i1*a + j1*a by BINOM:15
.= (Int-mult-left(R)).(i,a) + (Nat-mult-left(R)).(j1,a) by Def23
.= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a) by Def23;
end;
suppose i in NAT & not j in NAT;
hence (Int-mult-left(R)).(i+j,a) = (Int-mult-left(R)).(i,a)
+(Int-mult-left(R)).(j,a) by Th158;
end;
suppose not i in NAT & j in NAT;
hence (Int-mult-left(R)).(i+j,a)
=(Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a) by Th158;
end;
suppose not i in NAT & not j in NAT; then
A3: i < 0 & j < 0 by INT_1:3; then
reconsider i1=-ii as Element of NAT by INT_1:3;
reconsider j1=-jj as Element of NAT by A3,INT_1:3;
S1: (Int-mult-left(R)).(i,a) = (Nat-mult-left(R)).(-i,-a) by A3,Def23
.= i1*(-a);
S2: (Nat-mult-left(R)).(-j,-a) = j1*(-a);
thus (Int-mult-left(R)).(i+j,a) = (Nat-mult-left(R)).(-(i+j),-a)
by Def23,A3
.= (i1+j1)*(-a)
.= i1*(-a) + j1*(-a) by BINOM:15
.= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a)
by A3,Def23,S1,S2;
end;
end;
theorem Th160:
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a, b being Element of R, i being Element of NAT
holds (Nat-mult-left(R)).(i,a+b)
= (Nat-mult-left(R)).(i,a) + (Nat-mult-left(R)).(i,b)
proof
let R be Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a, b be Element of R, i being Element of NAT;
defpred P[Nat] means (Nat-mult-left(R)).($1,a+b)
= (Nat-mult-left(R)).($1,a) + (Nat-mult-left(R)).($1,b);
A1: P[0]
proof
(Nat-mult-left(R)).(0,a+b) = 0.R by BINOM:def 3
.= 0.R + 0.R by RLVECT_1:4
.= (Nat-mult-left(R)).(0,a) + 0.R by BINOM:def 3
.= (Nat-mult-left(R)).(0,a) + (Nat-mult-left(R)).(0,b) by BINOM:def 3;
hence thesis;
end;
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A3:P[n];
(Nat-mult-left(R)).(n+1,a+b)
=(a+b) + (Nat-mult-left(R)).(n,a+b) by BINOM:def 3
.= (a+b) + (Nat-mult-left(R)).(n,a) + (Nat-mult-left(R)).(n,b)
by A3,RLVECT_1:def 3
.= a+ (Nat-mult-left(R)).(n,a) + b + (Nat-mult-left(R)).(n,b)
by RLVECT_1:def 3
.= (Nat-mult-left(R)).(n+1,a) + b + (Nat-mult-left(R)).(n,b)
by BINOM:def 3
.= (Nat-mult-left(R)).(n+1,a) + (b + (Nat-mult-left(R)).(n,b))
by RLVECT_1:def 3
.= (Nat-mult-left(R)).(n+1,a) + (Nat-mult-left(R)).(n+1,b)
by BINOM:def 3;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th161:
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a, b being Element of R, i being Element of INT.Ring
holds (Int-mult-left(R)).(i,a+b)
= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(i,b)
proof
let R be Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a, b be Element of R, i be Element of INT.Ring;
reconsider ii = i as Element of INT;
per cases;
suppose 0 <= i; then
reconsider i1=i as Element of NAT by INT_1:3;
thus (Int-mult-left(R)).(i,a+b)
= (Nat-mult-left(R)).(i1,a+b) by Def23
.= i1*a + i1*b by Th160
.= (Int-mult-left(R)).(i,a) + (Nat-mult-left(R)).(i1,b) by Def23
.= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(i,b) by Def23;
end;
suppose A1: 0 > i; then
reconsider i1=-ii as Element of NAT by INT_1:3;
(a+b) + ( (-a) + (-b)) = b + a + (-a) + (-b) by RLVECT_1:def 3
.= b + (a + (-a)) + (-b) by RLVECT_1:def 3
.= b + 0.R + (-b) by RLVECT_1:5
.= b + (-b) by RLVECT_1:4
.= 0.R by RLVECT_1:5; then
A2: -(a+b) = (-a) + (-b) by RLVECT_1:6;
S1: (i1)*(-a) = (Nat-mult-left(R)).(-i,-a)
.= (Int-mult-left(R)).(i,a) by A1,Def23;
S2: i1*(-b) = (Nat-mult-left(R)).(-i,-b);
thus (Int-mult-left(R)).(i,a+b) = (Nat-mult-left(R)).(-i,-(a+b))
by Def23,A1
.= i1*(-a) + i1*(-b) by A2,Th160
.= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(i,b)
by A1,Def23,S1,S2;
end;
end;
theorem Th162:
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a being Element of R, i, j being Element of NAT holds
(Nat-mult-left(R)).(i*j,a) = (Nat-mult-left(R)).(i,(Nat-mult-left(R)).(j,a))
proof
let R be Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a be Element of R, i, j be Element of NAT;
defpred P[Nat] means (Nat-mult-left(R)).($1*j,a)
=(Nat-mult-left(R)).($1,(Nat-mult-left(R)).(j,a));
A1: P[0]
proof
(Nat-mult-left(R)).(0*j,a) = 0.R by BINOM:def 3
.= (Nat-mult-left(R)).(0,(Nat-mult-left(R)).(j,a)) by BINOM:def 3;
hence thesis;
end;
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A3:P[n];
(Nat-mult-left(R)).((n+1)*j,a) = (j+(n*j))*a
.= j*a+(n*j)*a by BINOM:15
.= (Nat-mult-left(R)).(n+1,j*a) by A3,BINOM:def 3;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lm19:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT.Ring st
i <> 0 & j <> 0 holds
(Int-mult-left(R)).(i*j,a) = (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a))
proof
let R be Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a be Element of R, i, j be Element of INT.Ring;
reconsider ii = i, jj = j as Element of INT;
assume A1: i <> 0 & j <> 0;
per cases;
suppose A2: i in NAT & j in NAT; then
reconsider i1=i as Element of NAT;
reconsider j1=j as Element of NAT by A2;
thus (Int-mult-left(R)).(i*j,a)
= (Nat-mult-left(R)).(i1*j1,a) by Def23
.= (Nat-mult-left(R)).(i1,(Nat-mult-left(R)).(j1,a)) by Th162
.= (Nat-mult-left(R)).(i1,(Int-mult-left(R)).(j,a)) by Def23
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by Def23;
end;
suppose A4: i in NAT & not j in NAT; then
A5: 0 < i & jj < 0 by A1,INT_1:3;
reconsider i1= i as Element of NAT by A4;
reconsider j1=-jj as Element of NAT by A5,INT_1:3;
a7: ii*jj < 0 by XREAL_1:132,A5;
thus (Int-mult-left(R)).(i*j,a)
=(Nat-mult-left(R)).(-(i*j),-a) by a7,Def23
.=(Nat-mult-left(R)).(i1*j1,-a)
.= (Nat-mult-left(R)).(i1,(Nat-mult-left(R)).(-j,-a)) by Th162
.= (Nat-mult-left(R)).(i1,(Int-mult-left(R)).(j,a)) by Def23,A5
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by Def23;
end;
suppose A8: not i in NAT & j in NAT; then
A9: 0 < j & i < 0 by A1,INT_1:3; then
reconsider i1= -ii as Element of NAT by INT_1:3;
reconsider j1= j as Element of NAT by A8;
A11: ii*jj < 0 by A9,XREAL_1:132;
thus (Int-mult-left(R)).(i*j,a)
=(Nat-mult-left(R)).(-(i*j),-a) by A11,Def23
.=(Nat-mult-left(R)).(i1*j1,-a)
.= (Nat-mult-left(R)).(-i,(Nat-mult-left(R)).(j1,-a)) by Th162
.= (Nat-mult-left(R)).(-i,-((Nat-mult-left(R)).(j1,a))) by Th157
.= (Nat-mult-left(R)).(-i,-(Int-mult-left(R)).(j,a)) by Def23
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by A9,Def23;
end;
suppose not i in NAT & not j in NAT; then
A13: i < 0 & j < 0 by INT_1:3; then
reconsider i1=-ii as Element of NAT by INT_1:3;
reconsider j1=-jj as Element of NAT by A13,INT_1:3;
-(Nat-mult-left(R)).(j1,a) = (Nat-mult-left(R)).(j1,-a) by Th157; then
(Nat-mult-left(R)).(j1,-a) + (Nat-mult-left(R)).(j1,a) = 0.R
by RLVECT_1:def 10; then
A15: (Nat-mult-left(R)).(j1,a) = - (Nat-mult-left(R)).(j1,-a)
by RLVECT_1:def 10;
thus (Int-mult-left(R)).(i*j,a) =(Nat-mult-left(R)).(i1*j1,a)
by Def23
.= (Nat-mult-left(R)).(-i,(Nat-mult-left(R)).(-j,a)) by Th162
.= (Nat-mult-left(R)).(-i,-((Int-mult-left(R)).(j,a)))
by A13,A15,Def23
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by A13,Def23;
end;
end;
Lm20:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT.Ring st i = 0 or j = 0 holds
(Int-mult-left(R)).(i*j,a) = (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a))
proof
let R be Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a be Element of R, i, j be Element of INT.Ring;
assume A1: i = 0 or j = 0;
per cases by A1;
suppose A2: i = 0;
hence (Int-mult-left(R)).(i*j,a) = 0.R by Th152
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by A2,Th152;
end;
suppose A3: j = 0;
hence (Int-mult-left(R)).(i*j,a) = 0.R by Th152
.= (Int-mult-left(R)).(i,0.R) by Th154
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by Th152,A3;
end;
end;
theorem Th163:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT.Ring holds
(Int-mult-left(R)).(i*j,a) = (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a))
proof
let R be Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a be Element of R, i, j be Element of INT.Ring;
per cases;
suppose i = 0 or j = 0;
hence (Int-mult-left(R)).(i*j,a)
=(Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by Lm20;
end;
suppose not (i = 0 or j = 0);
hence (Int-mult-left(R)).(i*j,a)
=(Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by Lm19;
end;
end;
theorem
for AG be non empty Abelian add-associative right_zeroed
right_complementable addLoopStr holds
ModuleStr (# the carrier of AG, the addF of AG, the ZeroF of AG,
Int-mult-left(AG) #) is Z_Module
proof
let AG be non empty Abelian add-associative right_zeroed
right_complementable addLoopStr;
reconsider ZS = ModuleStr (# the carrier of AG,
the addF of AG, the ZeroF of AG,
Int-mult-left(AG) #) as non empty ModuleStr over INT.Ring;
set ML= the lmult of ZS;
set AD= the addF of ZS;
set CA= the carrier of ZS;
set Z0= the ZeroF of ZS;
set MLI = Int-mult-left(AG);
A1: for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS;
reconsider v1=v,w1=w as Element of AG;
thus v + w = v1+w1
.= w1+v1
.= w+v;
end;
A2: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of ZS;
reconsider u1=u,v1=v,w1=w as Element of AG;
thus (u + v) + w = u1+v1+w1
.= u1+(v1+w1) by RLVECT_1:def 3
.= u+(v+w);
end;
A3: for v being Element of ZS holds v + 0.ZS = v
proof
let v be Vector of ZS;
reconsider v1=v as Element of AG;
thus v + 0.ZS = v1+0.AG
.= v by RLVECT_1:def 4;
end;
A4: now
let v be Vector of ZS;
reconsider v1=v as Element of AG;
consider w1 being Element of AG such that
A5: v1+w1 = 0.AG by ALGSTR_0:def 11;
reconsider w=w1 as Element of ZS;
v+w = 0.ZS by A5;
hence v is right_complementable;
end;
A6: for a, b be Element of INT.Ring, v being Vector of ZS
holds (a + b) * v = a * v + b * v
proof
let a, b be Element of INT.Ring, v being Vector of ZS;
reconsider a1=a,b1=b as Element of INT;
reconsider v1=v as Element of AG;
thus (a+b) * v = MLI.(a,v1) + MLI.(b,v1) by Th159
.= a * v + b * v;
end;
A7: for a be Element of INT.Ring, v, w being Vector of ZS
holds a * (v + w) = a * v + a * w
proof
let a be Element of INT.Ring, v, w being Vector of ZS;
reconsider a1=a as Element of INT.Ring;
reconsider v1=v,w1=w as Element of AG;
thus a * (v + w) = MLI.(a1,v1+w1)
.= MLI.(a1,v1) + MLI.(a1,w1) by Th161
.= a * v + a * w;
end;
A8: for a, b be Element of INT.Ring for v being Vector of
ZS holds (a * b) * v = a * (b * v) by Th163;
for v being Vector of ZS holds (1.(INT.Ring)) * v = v by Th155;
hence thesis by A1,A2,A3,A4,A6,A7,A8,
VECTSP_1:def 14,VECTSP_1:def 15,VECTSP_1:def 16,VECTSP_1:def 17,
ALGSTR_0:def 16,RLVECT_1:def 2,def 3,def 4;
end;