:: $\mathbb Z$-modules
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received September 5, 2011
:: Copyright (c) 2011 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, ORDINAL1, 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;
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, NAT_1, INT_1, REALSET1, FINSEQ_1, FINSEQ_4, STRUCT_0,
ALGSTR_0, LATTICES, RLVECT_1, BINOM;
constructors BINOP_1, XXREAL_0, NAT_1, FUNCT_3, FUNCT_5, REALSET1, RELSET_1,
LATTICES, RLSUB_1, ALGSTR_1, BINOM, FINSEQ_4;
registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, ALGSTR_0,
FINSEQ_1, CARD_1, SUBSET_1, INT_1, REALSET1, LATTICES, RELAT_1, ALGSTR_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, STRUCT_0, ALGSTR_0, RLVECT_1, LATTICES, XBOOLE_0,
REALSET1, BINOP_1, BINOM;
theorems FUNCT_1, NAT_1, TARSKI, RELAT_1, STRUCT_0, XBOOLE_0, XBOOLE_1,
FINSEQ_1, ALGSTR_0, BINOM, CARD_1, FINSEQ_3, INT_1, RLVECT_1, BINOP_1,
LATTICES, MCART_1, ZFMISC_1, PARTFUN1, FUNCT_2, RELSET_1, XREAL_1,
RLSUB_2;
schemes NAT_1, BINOP_1, FUNCT_1, XBOOLE_0;
begin :: 1. Definition of Z-module
definition
struct (addLoopStr) Z_ModuleStruct
(# carrier -> set,
ZeroF -> Element of the carrier,
addF -> BinOp of the carrier,
Mult -> Function of [:INT, the carrier :], the carrier #);
end;
registration
cluster non empty for Z_ModuleStruct;
existence
proof
set ZS = the non empty set,
O = the Element of ZS,
F = the BinOp of ZS,
G = the Function of [:INT,ZS:],ZS;
take Z_ModuleStruct(#ZS,O,F,G#);
thus the carrier of Z_ModuleStruct(#ZS,O,F,G#) is non empty;
end;
end;
definition
let V be Z_ModuleStruct;
mode VECTOR of V is Element of V;
end;
reserve V for non empty Z_ModuleStruct;
reserve x, y, y1 for set;
reserve a, b for integer number;
reserve v for VECTOR of V;
definition
let V,v;
let a be integer number;
func a * v -> Element of V equals
(the Mult of V).(a,v);
coherence
proof
reconsider a as Element of INT by INT_1:def 2;
(the Mult of V).(a,v) is Element of V;
hence thesis;
end;
end;
registration
let ZS be non empty set, O be Element of ZS, F be BinOp of ZS,
G be Function of [:INT,ZS:],ZS;
cluster Z_ModuleStruct (# ZS,O,F,G #) -> non empty;
coherence;
end;
definition
let IT be non empty Z_ModuleStruct;
attr IT is vector-distributive means :RL1Def8:
for a for v,w being VECTOR of IT holds a * (v + w) = a * v + a * w;
attr IT is scalar-distributive means :RL1Def9:
for a,b for v being VECTOR of IT holds (a + b) * v = a * v + b * v;
attr IT is scalar-associative means :RL1Def10:
for a,b for v being VECTOR of IT holds (a * b) * v = a * (b * v);
attr IT is scalar-unital means :RL1Def11:
for v being VECTOR of IT holds 1 * v = v;
end;
definition
func Trivial-Z_ModuleStruct -> strict Z_ModuleStruct equals
Z_ModuleStruct(#1,op0,op2,pr2(INT,1)#);
coherence;
end;
registration
cluster Trivial-Z_ModuleStruct -> trivial non empty;
coherence by CARD_1:49;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
scalar-distributive vector-distributive scalar-associative scalar-unital
for non empty Z_ModuleStruct;
existence
proof
take S = Trivial-Z_ModuleStruct;
thus S is strict;
thus S is Abelian;
thus S is add-associative;
thus S is right_zeroed;
thus S is right_complementable;
thus for a,b for v being VECTOR of S holds (a + b) * v = a * v + b * v
by STRUCT_0:def 10;
thus for a for v,w being VECTOR of S holds a * (v + w) = a * v + a * w
by STRUCT_0:def 10;
thus for a,b for v being VECTOR of S holds (a * b) * v = a * (b * v)
by STRUCT_0:def 10;
thus for v being VECTOR of S holds 1 * v = v by STRUCT_0:def 10;
end;
end;
definition
mode Z_Module is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty Z_ModuleStruct;
end;
reserve V for Z_Module;
reserve v, w for VECTOR of V;
definition
let IT be non empty Z_ModuleStruct;
attr IT is Mult-cancelable means :RL1Def12:
for a for v being VECTOR of IT st a * v = 0.IT
holds a = 0 or v = 0.IT;
end;
theorem RL1Th23:
a = 0 or v = 0.V implies a * v = 0.V
proof
reconsider N1=1,N0=0 as Integer;
assume
A1: a = 0 or v = 0.V;
now
per cases by A1;
suppose
A2: a = 0;
v + N0 * v = N1 * v + N0 * v by RL1Def11
.= (N1 + N0) * v by RL1Def9
.= v by RL1Def11
.= 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 RL1Def8
.= 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 RL1Th29:
- v = (- 1) * v
proof
reconsider N1=1,N0=0,M1 = -1 as Integer;
v + (- 1) * v = 1 * v + (- 1) * v by RL1Def11
.= (1 + (- 1)) * v by RL1Def9
.= 0.V by RL1Th23;
hence (- v) = (- v) + (v + (- 1) * v) by RLVECT_1:4
.= ((- v) + v) + (- 1) * v by RLVECT_1:def 3
.= 0.V + (- 1) * v by RLVECT_1:def 10
.= (- 1) * v by RLVECT_1:4;
end;
theorem RL1Th33:
V is Mult-cancelable & v = - v implies v = 0.V
proof
assume AS:V is Mult-cancelable;
assume v = - v;
then 0.V = v + v by RLVECT_1:def 10
.= 1 * v + v by RL1Def11
.= 1 * v + 1 * v by RL1Def11
.= (1 + 1) * v by RL1Def9
.= 2 * v;
hence thesis by AS,RL1Def12;
end;
theorem
V is Mult-cancelable & v + v = 0.V implies v = 0.V
proof
assume AS: V is Mult-cancelable;
assume v + v = 0.V;
then v = - v by RLVECT_1:def 10;
hence thesis by AS,RL1Th33;
end;
theorem RL1Th38:
a * (- v) = (- a) * v
proof
thus a * (- v) = a * ((- 1) * v) by RL1Th29
.= (a *(- 1)) * v by RL1Def10
.= (- a) * v;
end;
theorem RL1Th39:
a * (- v) = - (a * v)
proof
thus a * (- v) = (- (1 * a)) * v by RL1Th38
.= ((- 1) * a) * v
.= (- 1) * (a * v) by RL1Def10
.= - (a * v) by RL1Th29;
end;
theorem
(- a) * (- v) = a * v
proof
thus (- a) * (- v) = (- (- a)) * v by RL1Th38
.= a * v;
end;
theorem RL1Th48:
a * (v - w) = a * v - a * w
proof
thus a * (v - w) = a * v + a * (- w) by RL1Def8
.= a * v - a * w by RL1Th39;
end;
theorem RL1Th49:
(a - b) * v = a * v - b * v
proof
thus (a - b) * v = (a + (- b)) * v .= a * v + (- b) * v by RL1Def9
.= a * v + b * (- v) by RL1Th38
.= a * v - b * v by RL1Th39;
end;
theorem
V is Mult-cancelable &
a <> 0 & a * v = a * w implies v = w
proof
assume AS:V is Mult-cancelable;
assume that
A1: a <> 0 and
A2: a * v = a * w;
0.V = a * v - a * w by A2,RLVECT_1:15
.= a * (v - w) by RL1Th48;
then v - w = 0.V by A1,AS,RL1Def12;
hence thesis by RLVECT_1:21;
end;
theorem
V is Mult-cancelable & v <> 0.V & a * v = b * v implies a = b
proof
assume AS: V is Mult-cancelable;
assume that
A1: v <> 0.V and
A2: a * v = b * v;
0.V = a * v - b * v by A2,RLVECT_1:15
.= (a - b) * v by RL1Th49;
then (- b) + a = 0 by A1,AS,RL1Def12;
hence thesis;
end;
reserve V for Z_Module;
reserve u,v,w for VECTOR of V;
reserve F,G,H,I for FinSequence of V;
reserve j,k,n for Element of NAT;
reserve f,f9,g for Function of NAT, the carrier of V;
RL1Lm4: 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;
RL1Lm5: len F = 0 implies Sum(F) = 0.V
proof
assume len F = 0;
then F = <*>(the carrier of V);
hence thesis by RL1Lm4;
end;
theorem RL1Th56:
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 RL1Def8
.= 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;
Sum(H) = 0.V by A18,RL1Lm5;
hence Sum(H) = a * Sum(I) by A17,A18,RL1Lm5,RL1Th23;
end;
then
A19: P[0];
for n holds P[n] from NAT_1:sch 1(A19,A16);
hence thesis by A1;
end;
theorem
for V being Z_Module, a being Integer holds
a * Sum(<*>(the carrier of V)) = 0.V by RL1Lm4,RL1Th23;
theorem
for V being Z_Module, a being Integer, v, u being VECTOR of V holds
a * Sum<* v,u *> = a * v + a * u
proof
let V be Z_Module, a be Integer, v, u be VECTOR of V;
thus a * Sum<* v,u *> = a * (v + u) by RLVECT_1:45
.= a * v + a * u by RL1Def8;
end;
theorem
for V being Z_Module, a being Integer, v, u, w being VECTOR of V
holds a * Sum<* v,u,w *> = a * v + a * u + a * w
proof
let V be Z_Module, a be Integer, 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 RL1Def8
.= a * v + a * u + a * w by RL1Def8;
end;
theorem
(- a) * v = - a * v
proof
thus (- a) * v = a * (- v) by RL1Th38
.= - a * v by RL1Th39;
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,RL1Th56;
end;
begin :: 2. Submodules and cosets of submodules in Z-module
reserve V, X, Y for Z_Module;
reserve u, u1, u2, v, v1, v2 for VECTOR of V;
reserve a for integer number;
reserve V1, V2, V3 for Subset of V;
reserve x for set;
definition
let V,V1;
attr V1 is linearly-closed means :SUB1Def1:
(for v, u st v in V1 & u in V1 holds v + u in V1) &
for a, v st v in V1 holds a * v in V1;
end;
theorem SUB1Th4:
V1 <> {} & V1 is linearly-closed implies 0.V in V1
proof
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed;
set x = the Element of V1;
reconsider x as Element of V by A1,TARSKI:def 3;
0 * x in V1 by A1,A2,SUB1Def1;
hence thesis by RL1Th23;
end;
theorem SUB1Th5:
V1 is linearly-closed implies for v st v in V1 holds - v in V1
proof
assume
A1: V1 is linearly-closed;
let v;
assume v in V1;
then (- 1) * v in V1 by A1,SUB1Def1;
hence thesis by RL1Th29;
end;
theorem SUB1Th6:
V1 is linearly-closed implies for v, u st v in V1 & u in V1 holds v - u in V1
proof
assume
A1: V1 is linearly-closed;
let v, u;
assume that
A2: v in V1 and
A3: u in V1;
- u in V1 by A1,A3,SUB1Th5;
hence thesis by A1,A2,SUB1Def1;
end;
theorem
the carrier of V = V1 implies V1 is linearly-closed
proof
assume
A1: the carrier of V = V1;
hence for v, u st v in V1 & u in V1 holds v + u in V1;
let a, v;
thus thesis by A1;
end;
theorem SUB1Th9:
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 v1, v2 such that
A5: v = v1 + v2 and
A6: v1 in V1 & v2 in V2 by A2,A3;
consider u1, u2 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,SUB1Def1;
hence thesis by A2,A9;
end;
let a, v;
assume v in V3;
then consider v1, v2 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,RL1Def8;
a * v1 in V1 & a * v2 in V2 by A1,A11,SUB1Def1;
hence thesis by A2,A12;
end;
registration let V;
cluster {0.V} -> linearly-closed for Subset of V;
coherence
proof let S be Subset of V such that
Z: S = {0.V};
thus for v, u st v in S & u in S holds v + u in S
proof
let v, u;
assume v in S & u in S;
then v = 0.V & u = 0.V by TARSKI:def 1,Z;
then v + u = 0.V by RLVECT_1:4;
hence thesis by TARSKI:def 1,Z;
end;
let a, v;
assume
A1: v in S;
then v = 0.V by TARSKI:def 1,Z;
hence thesis by A1,RL1Th23;
end;
end;
registration let V;
cluster linearly-closed for Subset of V;
existence
proof
take {0.V};
thus thesis;
end;
end;
registration let V;
let V1,V2 be linearly-closed Subset of V;
cluster V1 /\ V2 -> linearly-closed for Subset of V;
coherence
proof let S be Subset of V such that
Z: S = V1 /\ V2;
thus for v, u st v in S & u in S holds v + u in S
proof
let v, u;
assume
A3: v in S & u in S;
then v in V2 & u in V2 by XBOOLE_0:def 4,Z;
then
A4: v + u in V2 by SUB1Def1;
v in V1 & u in V1 by A3,XBOOLE_0:def 4,Z;
then v + u in V1 by SUB1Def1;
hence thesis by A4,XBOOLE_0:def 4,Z;
end;
let a, v;
assume
A5: v in S;
then v in V2 by XBOOLE_0:def 4,Z;
then
A6: a * v in V2 by SUB1Def1;
v in V1 by A5,XBOOLE_0:def 4,Z;
then a * v in V1 by SUB1Def1;
hence thesis by A6,XBOOLE_0:def 4,Z;
end;
end;
definition
let V;
mode Submodule of V -> Z_Module means :SUB1Def2:
the carrier of it c= the carrier of V & 0.it = 0.V
& the addF of it = (the addF of V) ||the carrier of it
& the Mult of it = (the Mult of V) | [:INT, the carrier of it:];
existence
proof
the addF of V = (the addF of V) ||the carrier of V &
the Mult of V = (the Mult of V) | [:INT, the carrier of V:] by RELSET_1:19;
hence thesis;
end;
end;
reserve W, W1, W2 for Submodule of V;
reserve w, w1, w2 for VECTOR of W;
theorem SUB1Th16:
x in W1 & W1 is Submodule of W2 implies x in W2
proof
assume x in W1 & W1 is Submodule of W2;
then x in the carrier of W1
& the carrier of W1 c= the carrier of W2 by SUB1Def2,STRUCT_0:def 5;
hence thesis by STRUCT_0:def 5;
end;
theorem SUB1Th17:
x in W implies x in V
proof
assume x in W;
then
A1: x in the carrier of W by STRUCT_0:def 5;
the carrier of W c= the carrier of V by SUB1Def2;
hence thesis by A1,STRUCT_0:def 5;
end;
theorem SUB1Th18:
w is VECTOR of V
proof
w in V by SUB1Th17,RLVECT_1:1;
hence thesis by STRUCT_0:def 5;
end;
theorem
0.W = 0.V by SUB1Def2;
theorem
0.W1 = 0.W2
proof
thus 0.W1 = 0.V by SUB1Def2
.= 0.W2 by SUB1Def2;
end;
theorem SUB1Th21:
w1 = v & w2 = u implies w1 + w2 = v + u
proof
assume
A1: v = w1 & u = w2;
w1 + w2 = ((the addF of V) ||the carrier of W).[w1,w2] by SUB1Def2;
hence thesis by A1,FUNCT_1:49;
end;
theorem SUB1Th22:
w = v implies a * w = a * v
proof
reconsider a as Element of INT by INT_1:def 2;
assume
A1: w = v;
a * w = ((the Mult of V) |
[:INT, the carrier of W:]).[a,w] by SUB1Def2;
hence thesis by A1,FUNCT_1:49;
end;
theorem SUB1Th23:
w = v implies - v = - w
proof
A1: - v = (- 1) * v & - w = (- 1) * w by RL1Th29;
assume w = v;
hence thesis by A1,SUB1Th22;
end;
theorem SUB1Th24:
w1 = v & w2 = u implies w1 - w2 = v - u
proof
assume that
A1: w1 = v and
A2: w2 = u;
- w2 = - u by A2,SUB1Th23;
hence thesis by A1,SUB1Th21;
end;
SUB1Lm1: the carrier of W = V1 implies V1 is linearly-closed
proof
set VW = the carrier of W;
reconsider WW = W as Z_Module;
assume
A1: the carrier of W = V1;
thus for v, u st v in V1 & u in V1 holds v + u in V1
proof
let v, u;
assume v in V1 & u in V1;
then reconsider vv = v, uu = u as VECTOR of WW by A1;
reconsider vw = vv + uu as Element of VW;
vw in V1 by A1;
hence thesis by SUB1Th21;
end;
let a, v;
assume v in V1;
then reconsider vv = v as VECTOR of WW by A1;
reconsider vw = a * vv as Element of VW;
vw in V1 by A1;
hence thesis by SUB1Th22;
end;
theorem SUB1Th33:
V is Submodule of V
proof
thus the carrier of V c= the carrier of V & 0.V = 0.V;
thus thesis by RELSET_1:19;
end;
theorem SUB1Th25:
0.V in W
proof
0.W in W by RLVECT_1:1;
hence thesis by SUB1Def2;
end;
theorem
0.W1 in W2
proof
0.W1 = 0.V by SUB1Def2;
hence thesis by SUB1Th25;
end;
theorem
0.W in V by SUB1Th17,RLVECT_1:1;
theorem SUB1Th28:
u in W & v in W implies u + v in W
proof
reconsider VW = the carrier of W as Subset of V by SUB1Def2;
assume u in W & v in W;
then
A1: u in the carrier of W & v in the carrier of W by STRUCT_0:def 5;
VW is linearly-closed by SUB1Lm1;
then u + v in the carrier of W by A1,SUB1Def1;
hence thesis by STRUCT_0:def 5;
end;
theorem SUB1Th29:
v in W implies a * v in W
proof
reconsider VW = the carrier of W as Subset of V by SUB1Def2;
assume v in W;
then
A1: v in the carrier of W by STRUCT_0:def 5;
VW is linearly-closed by SUB1Lm1;
then a * v in the carrier of W by A1,SUB1Def1;
hence thesis by STRUCT_0:def 5;
end;
theorem SUB1Th30:
v in W implies - v in W
proof
assume v in W;
then (- 1) * v in W by SUB1Th29;
hence thesis by RL1Th29;
end;
theorem SUB1Th31:
u in W & v in W implies u - v in W
proof
assume that
A1: u in W and
A2: v in W;
- v in W by A2,SUB1Th30;
hence thesis by A1,SUB1Th28;
end;
reserve D for non empty set;
reserve d1 for Element of D;
reserve A for BinOp of D;
reserve M for Function of [:INT,D:],D;
theorem SUB1Th32:
V1 = D & d1 = 0.V & A = (the addF of V) ||V1 &
M = (the Mult of V) | [:INT,V1:] implies Z_ModuleStruct (# D,d1,A,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 Mult of V) | [:INT,V1:];
set W = Z_ModuleStruct (# D,d1,A,M #);
A5: for a for x being VECTOR of W holds a * x = (the Mult of V).(a,x)
proof
let a;
let x be VECTOR of W;
reconsider a1=a as Element of INT by INT_1:def 2;
thus a * x = (the Mult of V) . [a1,x] by A1,A4,FUNCT_1:49
.= (the Mult 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 Mult 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) * x1 by RL1Th29
.= (- 1) * x by A5;
then reconsider y = v as VECTOR of W;
take y;
thus thesis by A2,A6,A8;
end;
thus for a being integer number for x, y being VECTOR of W
holds a * (x + y) = a * x + a * y
proof
let a be integer number;
let x, y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3;
reconsider a as Integer;
a * (x + y) = MV.(a,x + y) by A5
.= a * (x1 + y1) by A6
.= a * x1 + a * y1 by RL1Def8
.= 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 integer number for
x being VECTOR of W holds (a + b) * x = a * x + b * x
proof
let a, b be integer number;
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
reconsider a, b as Integer;
(a + b) * x = (a + b) * y by A5
.= a * y + b * y by RL1Def9
.= 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 integer number
for x being VECTOR of W holds (a * b) * x = a * (b * x)
proof
let a, b be integer number;
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
reconsider a, b as Integer;
(a * b) * x = (a * b) * y by A5
.= a * (b * y) by RL1Def10
.= 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 * x = 1 * y by A5
.= x by RL1Def11;
end;
0.W = 0.V by A2;
hence thesis by A1,A3,A4,A7,SUB1Def2;
end;
theorem SUB1Th34:
for V,X being strict Z_Module st V is Submodule of X &
X is Submodule of V holds V = X
proof
let V,X be strict Z_Module;
assume that
A1: V is Submodule of X and
A2: X is Submodule of V;
set VX = the carrier of X;
set VV = the carrier of V;
VV c= VX & VX c= VV by A1,A2,SUB1Def2;
then
A3: VV = VX by XBOOLE_0:def 10;
set AX = the addF of X;
set AV = the addF of V;
AV = AX||VV & AX = AV||VX by A1,A2,SUB1Def2;
then
A4: AV = AX by A3,RELAT_1:72;
set MX = the Mult of X;
set MV = the Mult of V;
A5: MX = MV | [:INT,VX:] by A2,SUB1Def2;
0.V = 0.X & MV = MX | [:INT,VV:] by A1,SUB1Def2;
hence thesis by A3,A4,A5,RELAT_1:72;
end;
theorem SUB1Th35:
V is Submodule of X & X is Submodule of Y implies V is Submodule of Y
proof
assume that
A1: V is Submodule of X and
A2: X is Submodule of Y;
the carrier of V c= the carrier of X & the carrier of X c= the carrier
of Y by A1,A2,SUB1Def2;
hence the carrier of V c= the carrier of Y by XBOOLE_1:1;
0.V = 0.X by A1,SUB1Def2;
hence 0.V = 0.Y by A2,SUB1Def2;
thus the addF of V = (the addF of Y) ||the carrier of V
proof
set AY = the addF of Y;
set VX = the carrier of X;
set AX = the addF of X;
set VV = the carrier of V;
set AV = the addF of V;
VV c= VX by A1,SUB1Def2;
then
A3: [:VV,VV:] c= [:VX,VX:] by ZFMISC_1:96;
AV = AX||VV by A1,SUB1Def2;
then AV = AY||VX||VV by A2,SUB1Def2;
hence thesis by A3,FUNCT_1:51;
end;
set MY = the Mult of Y;
set MX = the Mult of X;
set MV = the Mult of V;
set VX = the carrier of X;
set VV = the carrier of V;
VV c= VX by A1,SUB1Def2;
then
A4: [:INT,VV:] c= [:INT,VX:] by ZFMISC_1:95;
MV = MX | [:INT,VV:] by A1,SUB1Def2;
then MV = (MY | [:INT,VX:]) | [:INT,VV:] by A2,SUB1Def2;
hence thesis by A4,FUNCT_1:51;
end;
theorem SUB1Th36:
the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2
proof
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
set AV = the addF of V;
set MV = the Mult of V;
assume
A1: the carrier of W1 c= the carrier of W2;
then
A2: [:VW1,VW1:] c= [:VW2,VW2:] by ZFMISC_1:96;
0.W1 = 0.V by SUB1Def2;
hence the carrier of W1 c= the carrier of W2 & 0.W1 = 0.W2 by A1,SUB1Def2;
the addF of W1 = AV||VW1 & the addF of W2 = AV||VW2 by SUB1Def2;
hence the addF of W1 = (the addF of W2) ||
the carrier of W1 by A2,FUNCT_1:51;
A3: [:INT,VW1:] c= [:INT,VW2:] by A1,ZFMISC_1:95;
the Mult of W1 = MV | [:INT,VW1:] & the Mult of W2 = MV | [:INT,VW2 :]
by SUB1Def2;
hence thesis by A3,FUNCT_1:51;
end;
theorem
(for v st v in W1 holds v in W2) implies W1 is Submodule of W2
proof
assume
A1: for v st v in W1 holds v in W2;
the carrier of W1 c= the carrier of W2
proof
let x be set;
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by SUB1Def2;
then reconsider v = x as VECTOR of V by A2;
v in W1 by A2,STRUCT_0:def 5;
then v in W2 by A1;
hence thesis by STRUCT_0:def 5;
end;
hence thesis by SUB1Th36;
end;
registration
let V;
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 Mult of V = (the Mult of V)
| [: INT,V1:] by RELSET_1:19;
then Z_ModuleStruct(#the carrier of V,0.V,the addF of V,the Mult of V #)
is Submodule of V by SUB1Th32;
hence thesis;
end;
end;
theorem SUB1Th38:
for W1, W2 being strict Submodule of V holds
the carrier of W1 = the carrier of W2 implies W1 = W2
proof
let W1, W2 be strict Submodule of V;
assume the carrier of W1 = the carrier of W2;
then W1 is Submodule of W2 & W2 is Submodule of W1 by SUB1Th36;
hence thesis by SUB1Th34;
end;
theorem SUB1Th39:
for W1, W2 being strict Submodule of V holds
(for v holds v in W1 iff v in W2) implies W1 = W2
proof
let W1, W2 be strict Submodule of V;
assume
A1: for v holds v in W1 iff v in W2;
x in the carrier of W1 iff x in the carrier of W2
proof
thus x in the carrier of W1 implies x in the carrier of W2
proof
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by SUB1Def2;
then reconsider v = x as VECTOR of V by A2;
v in W1 by A2,STRUCT_0:def 5;
then v in W2 by A1;
hence thesis by STRUCT_0:def 5;
end;
assume
A3: x in the carrier of W2;
the carrier of W2 c= the carrier of V by SUB1Def2;
then reconsider v = x as VECTOR of V by A3;
v in W2 by A3,STRUCT_0:def 5;
then v in W1 by A1;
hence thesis by STRUCT_0:def 5;
end;
then the carrier of W1 = the carrier of W2 by TARSKI:1;
hence thesis by SUB1Th38;
end;
theorem
for V being strict Z_Module, W being strict Submodule of V holds
the carrier of W = the carrier of V implies W = V
proof
let V be strict Z_Module, W be strict Submodule of V;
assume
A1: the carrier of W = the carrier of V;
V is Submodule of V by SUB1Th33;
hence thesis by A1,SUB1Th38;
end;
theorem
for V being strict Z_Module, 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 Z_Module, 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 SUB1Th33;
hence thesis by A1,SUB1Th39;
end;
theorem
the carrier of W = V1 implies V1 is linearly-closed by SUB1Lm1;
theorem SUB1Th43:
V1 <> {} & V1 is linearly-closed implies ex W being strict
Submodule of V st V1 = the carrier of W
proof
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed;
reconsider D = V1 as non empty set by A1;
set M = (the Mult of V) | [:INT,V1:];
set VV = the carrier of V;
dom(the Mult of V) = [:INT,VV:] by FUNCT_2:def 1;
then
A3: dom M = [:INT,VV:] /\ [:INT,V1:] by RELAT_1:61;
[:INT,V1:] c= [:INT,VV:] by ZFMISC_1:95;
then
A4: dom M = [:INT,D:] by A3,XBOOLE_1:28;
now
let y be set;
thus y in D implies ex x being set st x in dom M & y = M.x
proof
assume
A5: y in D;
then reconsider v1 = y as Element of VV;
reconsider N1=1 as Element of INT by INT_1:def 2;
A6: [N1,y] in [:INT,D:] by A5,ZFMISC_1:87;
then M. [1,y] = 1 * v1 by FUNCT_1:49
.= y by RL1Def11;
hence thesis by A4,A6;
end;
given x being set such that
A7: x in dom M and
A8: y = M.x;
consider x1,x2 being set such that
A9: x1 in INT and
A10: x2 in D and
A11: x = [x1,x2] by A4,A7,ZFMISC_1:def 2;
reconsider xx1 = x1 as Integer by A9;
reconsider v2 = x2 as Element of VV by A10;
[x1,x2] in [:INT,V1:] by A9,A10,ZFMISC_1:87;
then y = xx1 * v2 by A8,A11,FUNCT_1:49;
hence y in D by A2,A10,SUB1Def1;
end;
then D = rng M by FUNCT_1:def 3;
then reconsider M as Function of [:INT,D:],D
by A4,FUNCT_2:def 1,RELSET_1:4;
set A = (the addF of V) ||V1;
reconsider d1 = 0.V as Element of D by A2,SUB1Th4;
dom(the addF of V) = [:VV,VV:] by FUNCT_2:def 1;
then dom A = [:VV,VV:] /\ [:V1,V1:] by RELAT_1:61;
then
A12: dom A = [:D,D:] by XBOOLE_1:28;
now
let y be set;
thus y in D implies ex x being set st x in dom A & y = A.x
proof
assume
A13: y in D;
then reconsider v1 = y, v0 = d1 as Element of VV;
A14: [d1,y] in [:D,D:] by A13,ZFMISC_1:87;
then A. [d1,y] = v0 + v1 by FUNCT_1:49
.= y by RLVECT_1:4;
hence thesis by A12,A14;
end;
given x being set such that
A15: x in dom A and
A16: y = A.x;
consider x1,x2 being set such that
A17: x1 in D & x2 in D and
A18: x = [x1,x2] by A12,A15,ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Element of VV by A17;
[x1,x2] in [:V1,V1:] by A17,ZFMISC_1:87;
then y = v1 + v2 by A16,A18,FUNCT_1:49;
hence y in D by A2,A17,SUB1Def1;
end;
then D = rng A by FUNCT_1:def 3;
then reconsider A as Function of [:D,D:],D
by A12,FUNCT_2:def 1,RELSET_1:4;
set W = Z_ModuleStruct (# D,d1,A,M #);
W is Submodule of V by SUB1Th32;
hence thesis;
end;
definition
let V;
func (0).V -> strict Submodule of V means :SUB1Def3:
the carrier of it = {0.V};
correctness by SUB1Th38,SUB1Th43;
end;
definition
let V;
func (Omega).V -> strict Submodule of V equals
the Z_ModuleStruct of V;
coherence
proof
set W = the Z_ModuleStruct of V;
A1: for u, v, w being VECTOR of W holds (u + v) + w = u + (v + w)
proof
let u, v, w be VECTOR of W;
reconsider u9=u,v9=v,w9=w as VECTOR of V;
thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w);
end;
A2: for v being VECTOR of W holds v + 0.W = v
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus v + 0.W = v9 + 0.V .= v by RLVECT_1:4;
end;
A3: W is right_complementable
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
consider w9 being VECTOR of V such that
A4: v9 + w9 = 0.V by ALGSTR_0:def 11;
reconsider w=w9 as VECTOR of W;
take w;
thus thesis by A4;
end;
A5: for a being integer number for v,w being VECTOR of W holds
a * (v + w) = a * v + a * w
proof
let a be integer number;
let v, w be VECTOR of W;
reconsider v9=v, w9=w as VECTOR of V;
thus a * (v + w) = a * (v9 + w9)
.= a * v9 + a * w9 by RL1Def8
.= a * v + a * w;
end;
A6: for a, b being integer number for v being VECTOR of W holds
(a * b) * v = a * (b * v)
proof
let a, b be integer number;
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by RL1Def10
.= a * (b * v);
end;
A7: for a, b being integer number for v being VECTOR of W holds
(a + b) * v = a * v + b * v
proof
let a, b be integer number;
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus (a + b) * v = (a + b) * v9 .= a * v9 + b * v9 by RL1Def9
.= a * v + b * v;
end;
A8: for a for v, w be VECTOR of W, v9,w9 be VECTOR of V st v=v9 & w=w9
holds v+w = v9+w9 & a*v = a*v9;
A9: for v, w being VECTOR of W holds v + w = w + v
proof
let v, w be VECTOR of W;
reconsider v9=v, w9=w as VECTOR of V;
thus v + w = w9 + v9 by A8
.= w + v;
end;
for v being VECTOR of W holds 1 * v = v
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus 1 * v = 1 * v9 .= v by RL1Def11;
end;
then reconsider W as Z_Module
by A9,A1,A2,A3,A5,A7,A6,RL1Def8,RL1Def9,RL1Def10,RL1Def11,RLVECT_1:def 2
,def 3,def 4;
A10: the Mult of W = (the Mult of V) | [:INT, the carrier of W:]
by RELSET_1:19;
0.W = 0.V & the addF of W = (the addF of V) ||the carrier of W
by RELSET_1:19;
hence thesis by A10,SUB1Def2;
end;
end;
theorem SUB1Th48:
(0).W = (0).V
proof
the carrier of (0).W = {0.W} & the carrier of (0).V = {0.V} by SUB1Def3;
then
A1: the carrier of (0).W = the carrier of (0).V by SUB1Def2;
(0).W is Submodule of V by SUB1Th35;
hence thesis by A1,SUB1Th38;
end;
theorem SUB1Th49:
(0).W1 = (0).W2
proof
(0).W1 = (0).V by SUB1Th48;
hence thesis by SUB1Th48;
end;
theorem
(0).W is Submodule of V by SUB1Th35;
theorem SUB1Th51:
(0).V is Submodule of W
proof
the carrier of (0).V = {0.V} by SUB1Def3
.= {0.W} by SUB1Def2;
hence thesis by SUB1Th36;
end;
theorem
(0).W1 is Submodule of W2
proof
(0).W1 = (0).W2 by SUB1Th49;
hence thesis;
end;
theorem
for V being strict Z_Module holds V is Submodule of (Omega).V;
definition
let V,v,W;
func v + W -> Subset of V equals
{v + u : u in W};
coherence
proof
set Y = {v + u : u in W};
defpred P[set] means ex u st $1 = v + u & u in W;
consider X being set such that
A1: for x being set holds x in X iff x in the carrier of V & P[x]
from XBOOLE_0:sch 1;
X c= the carrier of V
proof
let x be set;
assume x in X;
hence thesis by A1;
end;
then reconsider X as Subset of V;
A2: Y c= X
proof
let x be set;
assume x in Y;
then ex u st x = v + u & u in W;
hence thesis by A1;
end;
X c= Y
proof
let x be set;
assume x in X;
then ex u st x = v + u & u in W by A1;
hence thesis;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
end;
SUB1Lm2: 0.V + W = the carrier of W
proof
set A = {0.V + u : u in W};
A1: the carrier of W c= A
proof
let x be set;
assume x in the carrier of W;
then
A2: x in W by STRUCT_0:def 5;
then x in V by SUB1Th17;
then reconsider y = x as Element of V by STRUCT_0:def 5;
0.V + y = x by RLVECT_1:4;
hence thesis by A2;
end;
A c= the carrier of W
proof
let x be set;
assume x in A;
then consider u such that
A3: x = 0.V + u and
A4: u in W;
x = u by A3,RLVECT_1:4;
hence thesis by A4,STRUCT_0:def 5;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
definition
let V,W;
mode Coset of W -> Subset of V means :SUB1Def6:
ex v st it = v + W;
existence
proof
reconsider VW = the carrier of W as Subset of V by SUB1Def2;
take VW;
take 0.V;
thus thesis by SUB1Lm2;
end;
end;
reserve B,C for Coset of W;
theorem SUB1Th58:
0.V in v + W iff v in W
proof
thus 0.V in v + W implies v in W
proof
assume 0.V in v + W;
then consider u such that
A1: 0.V = v + u and
A2: u in W;
v = - u by A1,RLVECT_1:def 10;
hence thesis by A2,SUB1Th30;
end;
assume v in W;
then
A3: - v in W by SUB1Th30;
0.V = v - v by RLVECT_1:15
.= v + (- v);
hence thesis by A3;
end;
theorem SUB1Th59:
v in v + W
proof
v + 0.V = v & 0.V in W by SUB1Th25,RLVECT_1:4;
hence thesis;
end;
theorem
0.V + W = the carrier of W by SUB1Lm2;
theorem SUB1Th61:
v + (0).V = {v}
proof
thus v + (0).V c= {v}
proof
let x be set;
assume x in v + (0).V;
then consider u such that
A1: x = v + u and
A2: u in (0).V;
A3: the carrier of (0).V = {0.V} by SUB1Def3;
u in the carrier of (0).V by A2,STRUCT_0:def 5;
then u = 0.V by A3,TARSKI:def 1;
then x = v by A1,RLVECT_1:4;
hence thesis by TARSKI:def 1;
end;
let x be set;
assume x in {v};
then
A4: x = v by TARSKI:def 1;
0.V in (0).V & v = v + 0.V by SUB1Th25,RLVECT_1:4;
hence thesis by A4;
end;
SUB1Lm3: v in W iff v + W = the carrier of W
proof
0.V in W & v + 0.V = v by SUB1Th25,RLVECT_1:4;
then
A1: v in {v + u : u in W};
thus v in W implies v + W = the carrier of W
proof
assume
A2: v in W;
thus v + W c= the carrier of W
proof
let x be set;
assume x in v + W;
then consider u such that
A3: x = v + u and
A4: u in W;
v + u in W by A2,A4,SUB1Th28;
hence thesis by A3,STRUCT_0:def 5;
end;
let x be set;
assume x in the carrier of W;
then reconsider y = x, z = v as Element of W by A2,STRUCT_0:def 5;
reconsider y1 = y, z1 = z as VECTOR of V by SUB1Th18;
A5: z + (y - z) = (y + z) - z by RLVECT_1:def 3
.= y + (z - z) by RLVECT_1:def 3
.= y + 0.W by RLVECT_1:15
.= x by RLVECT_1:4;
y - z in W by STRUCT_0:def 5;
then
A6: y1 - z1 in W by SUB1Th24;
y - z = y1 - z1 by SUB1Th24;
then z1 + (y1 - z1) = x by A5,SUB1Th21;
hence thesis by A6;
end;
thus thesis by A1,STRUCT_0:def 5;
end;
theorem SUB1Th62:
v + (Omega).V = the carrier of V
proof
v in (Omega).V by STRUCT_0:def 5;
hence thesis by SUB1Lm3;
end;
theorem SUB1Th63:
0.V in v + W iff v + W = the carrier of W
proof
0.V in v + W iff v in W by SUB1Th58;
hence thesis by SUB1Lm3;
end;
theorem
v in W iff v + W = the carrier of W by SUB1Lm3;
theorem
v in W implies (a * v) + W = the carrier of W
proof
assume
A1: v in W;
thus (a * v) + W c= the carrier of W
proof
let x be set;
assume x in (a * v) + W;
then consider u such that
A2: x = a * v + u and
A3: u in W;
a * v in W by A1,SUB1Th29;
then a * v + u in W by A3,SUB1Th28;
hence thesis by A2,STRUCT_0:def 5;
end;
let x be set;
assume
A4: x in the carrier of W;
then
A5: x in W by STRUCT_0:def 5;
the carrier of W c= the carrier of V by SUB1Def2;
then reconsider y = x as Element of V by A4;
A6: a * v + (y - a * v) = (y + a * v) - a * v by RLVECT_1:def 3
.= y + (a * v - a * v) by RLVECT_1:def 3
.= y + 0.V by RLVECT_1:15
.= x by RLVECT_1:4;
a * v in W by A1,SUB1Th29;
then y - a * v in W by A5,SUB1Th31;
hence thesis by A6;
end;
theorem SUB1Th68:
u in W iff v + W = (v + u) + W
proof
thus u in W implies v + W = (v + u) + W
proof
assume
A1: u in W;
thus v + W c= (v + u) + W
proof
let x be set;
assume x in v + W;
then consider v1 such that
A2: x = v + v1 and
A3: v1 in W;
A4: (v + u) + (v1 - u) = v + (u + (v1 - u)) by RLVECT_1:def 3
.= v + ((v1 + u) - u) by RLVECT_1:def 3
.= v + (v1 + (u - u)) by RLVECT_1:def 3
.= v + (v1 + 0.V) by RLVECT_1:15
.= x by A2,RLVECT_1:4;
v1 - u in W by A1,A3,SUB1Th31;
hence thesis by A4;
end;
let x be set;
assume x in (v + u) + W;
then consider v2 such that
A5: x = (v + u) + v2 and
A6: v2 in W;
A7: x = v + (u + v2) by A5,RLVECT_1:def 3;
u + v2 in W by A1,A6,SUB1Th28;
hence thesis by A7;
end;
assume
A8: v + W = (v + u) + W;
0.V in W & v + 0.V = v by SUB1Th25,RLVECT_1:4;
then v in (v + u) + W by A8;
then consider u1 such that
A9: v = (v + u) + u1 and
A10: u1 in W;
v = v + 0.V & v = v + (u + u1) by A9,RLVECT_1:4,def 3;
then u + u1 = 0.V by RLVECT_1:8;
then u = - u1 by RLVECT_1:def 10;
hence thesis by A10,SUB1Th30;
end;
theorem
u in W iff v + W = (v - u) + W
proof
A1: - u in W implies u in W
proof
assume - u in W;
then - (- u) in W by SUB1Th30;
hence thesis by RLVECT_1:17;
end;
- u in W iff v + W = (v + (- u)) + W by SUB1Th68;
hence thesis by A1,SUB1Th30;
end;
theorem SUB1Th70:
v in u + W iff u + W = v + W
proof
thus v in u + W implies u + W = v + W
proof
assume v in u + W;
then consider z being VECTOR of V such that
A1: v = u + z and
A2: z in W;
thus u + W c= v + W
proof
let x be set;
assume x in u + W;
then consider v1 such that
A3: x = u + v1 and
A4: v1 in W;
v - z = u + (z - z) by A1,RLVECT_1:def 3
.= u + 0.V by RLVECT_1:15
.= u by RLVECT_1:4;
then
A5: x = v + (v1 + (- z)) by A3,RLVECT_1:def 3
.= v + (v1 - z);
v1 - z in W by A2,A4,SUB1Th31;
hence thesis by A5;
end;
let x be set;
assume x in v + W;
then consider v2 such that
A6: x = v + v2 & v2 in W;
z + v2 in W & x = u + (z + v2) by A1,A2,A6,SUB1Th28,RLVECT_1:def 3;
hence thesis;
end;
thus thesis by SUB1Th59;
end;
theorem SUB1Th72:
u in v1 + W & u in v2 + W implies v1 + W = v2 + W
proof
assume that
A1: u in v1 + W and
A2: u in v2 + W;
consider x1 being VECTOR of V such that
A3: u = v1 + x1 and
A4: x1 in W by A1;
consider x2 being VECTOR of V such that
A5: u = v2 + x2 and
A6: x2 in W by A2;
thus v1 + W c= v2 + W
proof
let x be set;
assume x in v1 + W;
then consider u1 such that
A7: x = v1 + u1 and
A8: u1 in W;
x2 - x1 in W by A4,A6,SUB1Th31;
then
A9: (x2 - x1) + u1 in W by A8,SUB1Th28;
u - x1 = v1 + (x1 - x1) by A3,RLVECT_1:def 3
.= v1 + 0.V by RLVECT_1:15
.= v1 by RLVECT_1:4;
then x = (v2 + (x2 - x1)) + u1 by A5,A7,RLVECT_1:def 3
.= v2 + ((x2 - x1) + u1) by RLVECT_1:def 3;
hence thesis by A9;
end;
let x be set;
assume x in v2 + W;
then consider u1 such that
A10: x = v2 + u1 and
A11: u1 in W;
x1 - x2 in W by A4,A6,SUB1Th31;
then
A12: (x1 - x2) + u1 in W by A11,SUB1Th28;
u - x2 = v2 + (x2 - x2) by A5,RLVECT_1:def 3
.= v2 + 0.V by RLVECT_1:15
.= v2 by RLVECT_1:4;
then x = (v1 + (x1 - x2)) + u1 by A3,A10,RLVECT_1:def 3
.= v1 + ((x1 - x2) + u1) by RLVECT_1:def 3;
hence thesis by A12;
end;
theorem
v in W implies a * v in v + W
proof
assume v in W;
then
A1: (a - 1) * v in W by SUB1Th29;
a * v = ((a - 1) + 1) * v .= (a - 1) * v + 1 * v by RL1Def9
.= v + (a - 1) * v by RL1Def11;
hence thesis by A1;
end;
theorem SUB1Th77:
u + v in v + W iff u in W
proof
thus u + v in v + W implies u in W
proof
assume u + v in v + W;
then ex v1 st u + v = v + v1 & v1 in W;
hence thesis by RLVECT_1:8;
end;
assume u in W;
hence thesis;
end;
theorem
v - u in v + W iff u in W
proof
A1: v - u = (- u) + v;
A2: - u in W implies - (- u) in W by SUB1Th30;
u in W implies - u in W by SUB1Th30;
hence thesis by A1,A2,SUB1Th77,RLVECT_1:17;
end;
theorem SUB1Th79:
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 SUB1Th80:
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 consider v1 such that
A1: u = v + v1 and
A2: v1 in W;
take x = - v1;
thus x in W by A2,SUB1Th30;
thus thesis by A1,RLVECT_1:17;
end;
given v1 such that
A3: v1 in W and
A4: u = v - v1;
- v1 in W by A3,SUB1Th30;
hence thesis by A4;
end;
theorem SUB1Th81:
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W
proof
thus (ex v st v1 in v + W & v2 in v + W) implies v1 - v2 in W
proof
given v such that
A1: v1 in v + W and
A2: v2 in v + W;
consider u2 such that
A3: u2 in W and
A4: v2 = v + u2 by A2,SUB1Th79;
consider u1 such that
A5: u1 in W and
A6: v1 = v + u1 by A1,SUB1Th79;
v1 - v2 = (u1 + v) + ((- v) - u2) by A6,A4,RLVECT_1:30
.= ((u1 + v) + (- v)) - u2 by RLVECT_1:def 3
.= (u1 + (v + (- v))) - u2 by RLVECT_1:def 3
.= (u1 + 0.V) - u2 by RLVECT_1:5
.= u1 - u2 by RLVECT_1:4;
hence thesis by A5,A3,SUB1Th31;
end;
assume v1 - v2 in W;
then
A7: - (v1 - v2) in W by SUB1Th30;
take v1;
thus v1 in v1 + W by SUB1Th59;
v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by RLVECT_1:33
.= (v1 + (- v1)) + v2 by RLVECT_1:def 3
.= 0.V + v2 by RLVECT_1:5
.= v2 by RLVECT_1:4;
hence thesis by A7;
end;
theorem SUB1Th82:
v + W = u + W implies ex v1 st v1 in W & v + v1 = u
proof
assume v + W = u + W;
then v in u + W by SUB1Th59;
then consider u1 such that
A1: v = u + u1 and
A2: u1 in W;
take v1 = u - v;
0.V = (u + u1) - v by A1,RLVECT_1:15
.= u1 + (u - v) by RLVECT_1:def 3;
then v1 = - u1 by RLVECT_1:def 10;
hence v1 in W by A2,SUB1Th30;
thus v + v1 = (u + v) - v by RLVECT_1:def 3
.= u + (v - v) by RLVECT_1:def 3
.= u + 0.V by RLVECT_1:15
.= u by RLVECT_1:4;
end;
theorem SUB1Th83:
v + W = u + W implies ex v1 st v1 in W & v - v1 = u
proof
assume v + W = u + W;
then u in v + W by SUB1Th59;
then consider u1 such that
A1: u = v + u1 and
A2: u1 in W;
take v1 = v - u;
0.V = (v + u1) - u by A1,RLVECT_1:15
.= u1 + (v - u) by RLVECT_1:def 3;
then v1 = - u1 by RLVECT_1:def 10;
hence v1 in W by A2,SUB1Th30;
thus v - v1 = (v - v) + u by RLVECT_1:29
.= 0.V + u by RLVECT_1:15
.= u by RLVECT_1:4;
end;
theorem SUB1Th84:
for W1, W2 being strict Submodule of V st v + W1 = v + W2 holds W1 = W2
proof
let W1, W2 be strict Submodule of V;
assume
A1: v + W1 = v + W2;
the carrier of W1 = the carrier of W2
proof
A2: the carrier of W1 c= the carrier of V by SUB1Def2;
thus the carrier of W1 c= the carrier of W2
proof
let x be set;
assume
A3: x in the carrier of W1;
then reconsider y = x as Element of V by A2;
set z = v + y;
x in W1 by A3,STRUCT_0:def 5;
then z in v + W2 by A1;
then consider u such that
A4: z = v + u and
A5: u in W2;
y = u by A4,RLVECT_1:8;
hence thesis by A5,STRUCT_0:def 5;
end;
let x be set;
assume
A6: x in the carrier of W2;
the carrier of W2 c= the carrier of V by SUB1Def2;
then reconsider y = x as Element of V by A6;
set z = v + y;
x in W2 by A6,STRUCT_0:def 5;
then z in v + W1 by A1;
then consider u such that
A7: z = v + u and
A8: u in W1;
y = u by A7,RLVECT_1:8;
hence thesis by A8,STRUCT_0:def 5;
end;
hence thesis by SUB1Th38;
end;
theorem SUB1Th85:
for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds W1 = W2
proof
let W1, W2 be strict Submodule of V;
assume
A1: v + W1 = u + W2;
set V2 = the carrier of W2;
set V1 = the carrier of W1;
assume
A2: W1 <> W2;
A3:
now
set x = the Element of V1 \ V2;
assume V1 \ V2 <> {};
then x in V1 by XBOOLE_0:def 5;
then
A4: x in W1 by STRUCT_0:def 5;
then x in V by SUB1Th17;
then reconsider x as Element of V by STRUCT_0:def 5;
set z = v + x;
z in u + W2 by A1,A4;
then consider u1 such that
A5: z = u + u1 and
A6: u1 in W2;
x = 0.V + x by RLVECT_1:4
.= v - v + x by RLVECT_1:15
.= - v + (u + u1) by A5,RLVECT_1:def 3;
then
A7: (v + (- v + (u + u1))) + W1 = v + W1 by A4,SUB1Th68;
v + (- v + (u + u1)) = (v - v) + (u + u1) by RLVECT_1:def 3
.= 0.V + (u + u1) by RLVECT_1:15
.= u + u1 by RLVECT_1:4;
then (u + u1) + W2 = (u + u1) + W1 by A1,A6,A7,SUB1Th68;
hence thesis by A2,SUB1Th84;
end;
A8:
now
set x = the Element of V2 \ V1;
assume V2 \ V1 <> {};
then x in V2 by XBOOLE_0:def 5;
then
A9: x in W2 by STRUCT_0:def 5;
then x in V by SUB1Th17;
then reconsider x as Element of V by STRUCT_0:def 5;
set z = u + x;
z in v + W1 by A1,A9;
then consider u1 such that
A10: z = v + u1 and
A11: u1 in W1;
x = 0.V + x by RLVECT_1:4
.= u - u + x by RLVECT_1:15
.= - u + (v + u1) by A10,RLVECT_1:def 3;
then
A12: (u + (- u + (v + u1))) + W2 = u + W2 by A9,SUB1Th68;
u + (- u + (v + u1)) = (u - u) + (v + u1) by RLVECT_1:def 3
.= 0.V + (v + u1) by RLVECT_1:15
.= v + u1 by RLVECT_1:4;
then (v + u1) + W1 = (v + u1) + W2 by A1,A11,A12,SUB1Th68;
hence thesis by A2,SUB1Th84;
end;
V1 <> V2 by A2,SUB1Th38;
then not V1 c= V2 or not V2 c= V1 by XBOOLE_0:def 10;
hence thesis by A3,A8,XBOOLE_1:37;
end;
theorem
C is linearly-closed iff C = the carrier of W
proof
thus C is linearly-closed implies C = the carrier of W
proof
assume
A1: C is linearly-closed;
consider v such that
A2: C = v + W by SUB1Def6;
C <> {} by A2,SUB1Th59;
then 0.V in v + W by A1,A2,SUB1Th4;
hence thesis by A2,SUB1Th63;
end;
thus thesis by SUB1Lm1;
end;
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
proof
let W1, W2 be strict Submodule of V, C1 be Coset of W1, C2 be Coset of W2;
(ex v1 st C1 = v1 + W1) & ex v2 st C2 = v2 + W2 by SUB1Def6;
hence thesis by SUB1Th85;
end;
theorem
{v} is Coset of (0).V
proof
v + (0).V = {v} by SUB1Th61;
hence thesis by SUB1Def6;
end;
theorem SUB1Th89:
V1 is Coset of (0).V implies ex v st V1 = {v}
proof
assume V1 is Coset of (0).V;
then consider v such that
A1: V1 = v + (0).V by SUB1Def6;
take v;
thus thesis by A1,SUB1Th61;
end;
theorem SUB1Th90:
the carrier of W is Coset of W
proof
the carrier of W = 0.V + W by SUB1Lm2;
hence thesis by SUB1Def6;
end;
theorem
the carrier of V is Coset of (Omega).V
proof
set v = the VECTOR of V;
the carrier of V is Subset of V iff the carrier of V c= the carrier of V;
then reconsider A = the carrier of V as Subset of V;
A = v + (Omega).V by SUB1Th62;
hence thesis by SUB1Def6;
end;
theorem
V1 is Coset of (Omega).V implies V1 = the carrier of V
proof
assume V1 is Coset of (Omega).V;
then ex v st V1 = v + (Omega).V by SUB1Def6;
hence thesis by SUB1Th62;
end;
theorem
0.V in C iff C = the carrier of W
proof
ex v st C = v + W by SUB1Def6;
hence thesis by SUB1Th63;
end;
theorem SUB1Th94:
u in C iff C = u + W
proof
thus u in C implies C = u + W
proof
assume
A1: u in C;
ex v st C = v + W by SUB1Def6;
hence thesis by A1,SUB1Th70;
end;
thus thesis by SUB1Th59;
end;
theorem
u in C & v in C implies ex v1 st v1 in W & u + v1 = v
proof
assume u in C & v in C;
then C = u + W & C = v + W by SUB1Th94;
hence thesis by SUB1Th82;
end;
theorem SUB1Th96:
u in C & v in C implies ex v1 st v1 in W & u - v1 = v
proof
assume u in C & v in C;
then C = u + W & C = v + W by SUB1Th94;
hence thesis by SUB1Th83;
end;
theorem
(ex C st v1 in C & v2 in C) iff v1 - v2 in W
proof
thus (ex C st v1 in C & v2 in C) implies v1 - v2 in W
proof
given C such that
A1: v1 in C & v2 in C;
ex v st C = v + W by SUB1Def6;
hence thesis by A1,SUB1Th81;
end;
assume v1 - v2 in W;
then consider v such that
A2: v1 in v + W & v2 in v + W by SUB1Th81;
reconsider C = v + W as Coset of W by SUB1Def6;
take C;
thus thesis by A2;
end;
theorem
u in B & u in C implies B = C
proof
assume
A1: u in B & u in C;
(ex v1 st B = v1 + W) & ex v2 st C = v2 + W by SUB1Def6;
hence thesis by A1,SUB1Th72;
end;
begin :: 3. Operations on submodules in Z-module
reserve V for Z_Module;
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 integer number;
reserve X, Y, y, y1, y2 for set;
definition
let V,W1,W2;
func W1 + W2 -> strict Submodule of V means :SUB2Def1:
the carrier of it = {v + u : v in W1 & u in W2};
existence
proof
reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V
by SUB1Def2;
set VS = {v + u : v in W1 & u in W2};
VS c= the carrier of V
proof
let x be set;
assume x in VS;
then ex v1, v2 st x = v1 + v2 & v1 in W1 & v2 in W2;
hence thesis;
end;
then reconsider VS as Subset of V;
A1: 0.V = 0.V + 0.V by RLVECT_1:4;
0.V in W1 & 0.V in W2 by SUB1Th25;
then
A2: 0.V in VS by A1;
A3: VS = {v + u : v in V1 & u in V2}
proof
thus VS c= {v + u : v in V1 & u in V2}
proof
let x be set;
assume x in VS;
then consider v,u such that
A4: x = v + u and
A5: v in W1 & u in W2;
v in V1 & u in V2 by A5,STRUCT_0:def 5;
hence thesis by A4;
end;
let x be set;
assume x in {v + u : v in V1 & u in V2};
then consider v,u such that
A6: x = v + u and
A7: v in V1 & u in V2;
v in W1 & u in W2 by A7,STRUCT_0:def 5;
hence thesis by A6;
end;
V1 is linearly-closed & V2 is linearly-closed by SUB1Lm1;
hence thesis by A2,A3,SUB1Th9,SUB1Th43;
end;
uniqueness by SUB1Th38;
commutativity
proof let W be strict Submodule of V;
let W1,W2;
set A = {v + u : v in W1 & u in W2};
set B = {v + u : v in W2 & u in W1};
A1: B c= A
proof
let x be set;
assume x in B;
then ex v, u st x = v + u & v in W2 & u in W1;
hence thesis;
end;
A c= B
proof
let x be set;
assume x in A;
then ex v, u st x = v + u & v in W1 & u in W2;
hence thesis;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
end;
definition
let V,W1,W2;
func W1 /\ W2 -> strict Submodule of V means :SUB2Def2:
the carrier of it = (the carrier of W1) /\ (the carrier of W2);
existence
proof
set VW2 = the carrier of W2;
set VW1 = the carrier of W1;
set VV = the carrier of V;
0.V in W2 by SUB1Th25;
then
A1: 0.V in VW2 by STRUCT_0:def 5;
VW1 c= VV & VW2 c= VV by SUB1Def2;
then VW1 /\ VW2 c= VV /\ VV by XBOOLE_1:27;
then reconsider
V1 = VW1, V2 = VW2, V3 = VW1 /\ VW2 as Subset of V by SUB1Def2;
V1 is linearly-closed & V2 is linearly-closed by SUB1Lm1;
then
A2: V3 is linearly-closed;
0.V in W1 by SUB1Th25;
then 0.V in VW1 by STRUCT_0:def 5;
then VW1 /\ VW2 <> {} by A1,XBOOLE_0:def 4;
hence thesis by A2,SUB1Th43;
end;
uniqueness by SUB1Th38;
commutativity;
end;
theorem SUB2Th5:
x in W1 + W2 iff ex v1, v2 st v1 in W1 & v2 in W2 & x = v1 + v2
proof
thus x in W1 + W2 implies ex v1, v2 st v1 in W1 & v2 in W2 & x = v1 + v2
proof
assume x in W1 + W2;
then x in the carrier of W1 + W2 by STRUCT_0:def 5;
then x in {v + u : v in W1 & u in W2} by SUB2Def1;
then consider v1, v2 such that
A1: x = v1 + v2 & v1 in W1 & v2 in W2;
take v1, v2;
thus thesis by A1;
end;
given v1, v2 such that
A2: v1 in W1 & v2 in W2 & x = v1 + v2;
x in {v + u : v in W1 & u in W2} by A2;
then x in the carrier of W1 + W2 by SUB2Def1;
hence thesis by STRUCT_0:def 5;
end;
theorem
v in W1 or v in W2 implies v in W1 + W2
proof
assume
A1: v in W1 or v in W2;
now
per cases by A1;
suppose
A2: v in W1;
v = v + 0.V & 0.V in W2 by SUB1Th25,RLVECT_1:4;
hence thesis by A2,SUB2Th5;
end;
suppose
A3: v in W2;
v = 0.V + v & 0.V in W1 by SUB1Th25,RLVECT_1:4;
hence thesis by A3,SUB2Th5;
end;
end;
hence thesis;
end;
theorem SUB2Th7:
x in W1 /\ W2 iff x in W1 & x in W2
proof
x in W1 /\ W2 iff x in the carrier of W1 /\ W2 by STRUCT_0:def 5;
then x in W1 /\ W2 iff x in (the carrier of W1) /\ (the carrier of W2)
by SUB2Def2;
then x in W1 /\ W2 iff x in the carrier of W1 & x in the carrier of W2
by XBOOLE_0:def 4;
hence thesis by STRUCT_0:def 5;
end;
SUB2Lm2: the carrier of W1 c= the carrier of W1 + W2
proof
let x be set;
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 SUB1Th18;
A1: v = v + 0.V by RLVECT_1:4;
v in W1 & 0.V in W2 by SUB1Th25,STRUCT_0:def 5;
then x in A by A1;
hence thesis by SUB2Def1;
end;
SUB2Lm3: for W2 being strict Submodule of V holds
the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2
proof
let W2 be strict Submodule of V;
assume
A1: the carrier of W1 c= the carrier of W2;
A2: the carrier of W1 + W2 c= the carrier of W2
proof
let x be set;
assume x in the carrier of W1 + W2;
then x in {v + u : v in W1 & u in W2} by SUB2Def1;
then consider v,u such that
A3: x = v + u and
A4: v in W1 and
A5: u in W2;
W1 is Submodule of W2 by A1,SUB1Th36;
then v in W2 by A4,SUB1Th16;
then v + u in W2 by A5,SUB1Th28;
hence thesis by A3,STRUCT_0:def 5;
end;
the carrier of W2 c= the carrier of W1+W2 by SUB2Lm2;
then the carrier of W1 + W2 = the carrier of W2 by A2,XBOOLE_0:def 10;
hence thesis by SUB1Th38;
end;
theorem
for W being strict Submodule of V holds W + W = W by SUB2Lm3;
theorem SUB2Th10:
W1 + (W2 + W3) = (W1 + W2) + W3
proof
set A = {v + u : v in W1 & u in W2};
set B = {v + u : v in W2 & u in W3};
set C = {v + u : v in W1 + W2 & u in W3};
set D = {v + u : v in W1 & u in W2 + W3};
A1: the carrier of W1 + (W2 + W3) = D by SUB2Def1;
A2: C c= D
proof
let x be set;
assume x in C;
then consider v,u such that
A3: x = v + u and
A4: v in W1 + W2 and
A5: u in W3;
v in the carrier of W1 + W2 by A4,STRUCT_0:def 5;
then v in A by SUB2Def1;
then consider u1,u2 such that
A6: v = u1 + u2 and
A7: u1 in W1 and
A8: u2 in W2;
u2 + u in B by A5,A8;
then u2 + u in the carrier of W2 + W3 by SUB2Def1;
then
A9: u2 + u in W2 + W3 by STRUCT_0:def 5;
v + u =u1 + (u2 + u) by A6,RLVECT_1:def 3;
hence thesis by A3,A7,A9;
end;
D c= C
proof
let x be set;
assume x in D;
then consider v, u such that
A10: x = v + u and
A11: v in W1 and
A12: u in W2 + W3;
u in the carrier of W2 + W3 by A12,STRUCT_0:def 5;
then u in B by SUB2Def1;
then consider u1,u2 such that
A13: u = u1 + u2 and
A14: u1 in W2 and
A15: u2 in W3;
v + u1 in A by A11,A14;
then v + u1 in the carrier of W1 + W2 by SUB2Def1;
then
A16: v + u1 in W1 + W2 by STRUCT_0:def 5;
v + u = (v + u1) + u2 by A13,RLVECT_1:def 3;
hence thesis by A10,A15,A16;
end;
then D = C by A2,XBOOLE_0:def 10;
hence thesis by A1,SUB2Def1;
end;
theorem SUB2Th11:
W1 is Submodule of W1 + W2
proof
the carrier of W1 c= the carrier of W1 + W2 by SUB2Lm2;
hence W1 is Submodule of W1 + W2 by SUB1Th36;
end;
theorem SUB2Th12:
for W2 being strict Submodule of V holds
W1 is Submodule of W2 iff W1 + W2 = W2
proof
let W2 be strict Submodule of V;
thus W1 is Submodule of W2 implies W1 + W2 = W2
proof
assume W1 is Submodule of W2;
then the carrier of W1 c= the carrier of W2 by SUB1Def2;
hence thesis by SUB2Lm3;
end;
thus thesis by SUB2Th11;
end;
theorem SUB2Th13:
for W being strict Submodule of V holds (0).V + W = W
proof
let W be strict Submodule of V;
(0).V is Submodule of W by SUB1Th51;
then the carrier of (0).V c= the carrier of W by SUB1Def2;
hence thesis by SUB2Lm3;
end;
theorem
(0).V + (Omega).V = the Z_ModuleStruct of V by SUB2Th13;
theorem SUB2Th15:
(Omega).V + W = the Z_ModuleStruct of V
proof
the carrier of W c= the carrier of V by SUB1Def2;
hence thesis by SUB2Lm3;
end;
theorem
for V being strict Z_Module holds (Omega).V + (Omega).V = V by SUB2Th15;
theorem
for W being strict Submodule of V holds W /\ W = W
proof
let W be strict Submodule of V;
the carrier of W = (the carrier of W) /\ (the carrier of W);
hence thesis by SUB2Def2;
end;
theorem SUB2Th19:
W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
proof
set V1 = the carrier of W1;
set V2 = the carrier of W2;
set V3 = the carrier of W3;
the carrier of W1 /\ (W2 /\ W3)
= V1 /\ (the carrier of W2 /\ W3) by SUB2Def2
.= V1 /\ (V2 /\ V3) by SUB2Def2
.= (V1 /\ V2) /\ V3 by XBOOLE_1:16
.= (the carrier of W1 /\ W2) /\ V3 by SUB2Def2;
hence thesis by SUB2Def2;
end;
SUB2Lm4: 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 SUB2Def2;
hence thesis by XBOOLE_1:17;
end;
theorem SUB2Th20:
W1 /\ W2 is Submodule of W1
proof
the carrier of W1 /\ W2 c= the carrier of W1 by SUB2Lm4;
hence W1 /\ W2 is Submodule of W1 by SUB1Th36;
end;
theorem SUB2Th21:
for W1 being strict Submodule of V holds W1 is Submodule of W2 iff
W1 /\ W2 = W1
proof
let W1 be strict Submodule of V;
thus W1 is Submodule of W2 implies W1 /\ W2 = W1
proof
assume W1 is Submodule of W2;
then
A1: the carrier of W1 c= the carrier of W2 by SUB1Def2;
the carrier of W1 /\ W2 = (the carrier of W1) /\ (the carrier of W2 )
by SUB2Def2;
hence thesis by A1,SUB1Th38,XBOOLE_1:28;
end;
thus thesis by SUB2Th20;
end;
theorem SUB2Th22:
(0).V /\ W = (0).V
proof
0.V in W by SUB1Th25;
then 0.V in the carrier of W by STRUCT_0:def 5;
then {0.V} c= the carrier of W by ZFMISC_1:31;
then
A1: {0.V} /\ (the carrier of W) = {0.V} by XBOOLE_1:28;
the carrier of (0).V /\ W = (the carrier of (0).V) /\ (the carrier of W)
by SUB2Def2
.= {0.V} /\ (the carrier of W) by SUB1Def3;
hence thesis by A1,SUB1Def3;
end;
theorem
(0).V /\ (Omega).V = (0).V by SUB2Th22;
theorem SUB2Th24:
for W being strict Submodule of V holds (Omega).V /\ W = W
proof
let W be strict Submodule of V;
the carrier of (Omega). V /\ W = (the carrier of V) /\ (the carrier of W)
& the carrier of W c= the carrier of V by SUB2Def2,SUB1Def2;
hence thesis by SUB1Th38,XBOOLE_1:28;
end;
theorem
for V being strict Z_Module holds (Omega).V /\ (Omega).V = V by SUB2Th24;
SUB2Lm5: 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 SUB2Lm2,SUB2Lm4;
hence thesis by XBOOLE_1:1;
end;
theorem
W1 /\ W2 is Submodule of W1 + W2 by SUB2Lm5,SUB1Th36;
SUB2Lm6: 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 set;
assume x in the carrier of (W1 /\ W2) + W2;
then x in {u + v : u in W1 /\ W2 & v in W2} by SUB2Def1;
then consider u, v such that
A1: x = u + v and
A2: u in W1 /\ W2 and
A3: v in W2;
u in W2 by A2,SUB2Th7;
then u + v in W2 by A3,SUB1Th28;
hence thesis by A1,STRUCT_0:def 5;
end;
let x be set;
the carrier of W2 c= the carrier of (W1 /\ W2) + W2 by SUB2Lm2;
hence thesis;
end;
theorem
for W2 being strict Submodule of V
holds (W1 /\ W2) + W2 = W2 by SUB2Lm6,SUB1Th38;
SUB2Lm7: 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 set;
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 SUB2Def2;
hence thesis by A1,XBOOLE_0:def 4;
end;
let x be set;
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by SUB1Def2;
then reconsider x1 = x as Element of V by A2;
A3: x1 + 0.V = x1 & 0.V in W2 by SUB1Th25,RLVECT_1:4;
x in W1 by A2,STRUCT_0:def 5;
then x in {u + v : u in W1 & v in W2} by A3;
then x in the carrier of W1 + W2 by SUB2Def1;
then x in (the carrier of W1) /\ (the carrier of W1 + W2) by A2,
XBOOLE_0:def 4;
hence thesis by SUB2Def2;
end;
theorem
for W1 being strict Submodule of V
holds W1 /\ (W1 + W2) = W1 by SUB2Lm7,SUB1Th38;
SUB2Lm8: the carrier of (W1 /\ W2) + (W2 /\ W3) c=
the carrier of W2 /\ (W1 + W3)
proof
let x be set;
assume x in the carrier of (W1 /\ W2) + (W2 /\ W3);
then x in {u + v : u in W1 /\ W2 & v in W2 /\ W3} by SUB2Def1;
then consider u, v such that
A1: x = u + v and
A2: u in W1 /\ W2 & v in W2 /\ W3;
u in W2 & v in W2 by A2,SUB2Th7;
then
A3: x in W2 by A1,SUB1Th28;
u in W1 & v in W3 by A2,SUB2Th7;
then x in W1 + W3 by A1,SUB2Th5;
then x in W2 /\ (W1 + W3) by A3,SUB2Th7;
hence thesis by STRUCT_0:def 5;
end;
theorem
(W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3) by SUB2Lm8,SUB1Th36;
SUB2Lm9: W1 is Submodule of W2 implies
the carrier of W2 /\ (W1 + W3) = the carrier of (W1 /\ W2) + (W2 /\ W3)
proof
assume
A1: W1 is Submodule of W2;
thus the carrier of W2 /\ (W1 + W3) c= the carrier of (W1 /\ W2) + (W2 /\ W3)
proof
let x be set;
assume x in the carrier of W2 /\ (W1 + W3);
then
A2: x in (the carrier of W2) /\ (the carrier of W1 + W3) by SUB2Def2;
then x in the carrier of W1 + W3 by XBOOLE_0:def 4;
then x in {u + v : u in W1 & v in W3} by SUB2Def1;
then consider u1, v1 such that
A3: x = u1 + v1 and
A4: u1 in W1 and
A5: v1 in W3;
A6: u1 in W2 by A1,A4,SUB1Th16;
x in the carrier of W2 by A2,XBOOLE_0:def 4;
then u1 + v1 in W2 by A3,STRUCT_0:def 5;
then (v1 + u1) - u1 in W2 by A6,SUB1Th31;
then v1 + (u1 - u1) in W2 by RLVECT_1:def 3;
then v1 + 0.V in W2 by RLVECT_1:15;
then v1 in W2 by RLVECT_1:4;
then
A7: v1 in W2 /\ W3 by A5,SUB2Th7;
u1 in W1 /\ W2 by A4,A6,SUB2Th7;
then x in (W1 /\ W2) + (W2 /\ W3) by A3,A7,SUB2Th5;
hence thesis by STRUCT_0:def 5;
end;
thus thesis by SUB2Lm8;
end;
theorem
W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
by SUB2Lm9,SUB1Th38;
SUB2Lm10: the carrier of W2 + (W1 /\ W3) c=
the carrier of (W1 + W2) /\ (W2 + W3)
proof
let x be set;
assume x in the carrier of W2 + (W1 /\ W3);
then x in {u + v : u in W2 & v in W1 /\ W3} by SUB2Def1;
then consider u, v such that
A1: x = u + v & u in W2 and
A2: v in W1 /\ W3;
v in W3 by A2,SUB2Th7;
then x in {u1 + u2 : u1 in W2 & u2 in W3} by A1;
then
A3: x in the carrier of W2 + W3 by SUB2Def1;
v in W1 by A2,SUB2Th7;
then x in {v1 + v2 : v1 in W1 & v2 in W2} by A1;
then x in the carrier of W1 + W2 by SUB2Def1;
then x in (the carrier of W1 + W2) /\ (the carrier of W2 + W3) by A3,
XBOOLE_0:def 4;
hence thesis by SUB2Def2;
end;
theorem
W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3) by SUB2Lm10,SUB1Th36;
SUB2Lm11: 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 SUB1Def2;
A1: V2 is linearly-closed by SUB1Lm1;
assume W1 is Submodule of W2;
then
A2: the carrier of W1 c= the carrier of W2 by SUB1Def2;
thus the carrier of W2 + (W1 /\ W3) c= the carrier of (W1 + W2) /\ (W2 + W3)
by SUB2Lm10;
let x be set;
assume x in the carrier of (W1 + W2) /\ (W2 + W3);
then x in (the carrier of W1 + W2) /\ (the carrier of W2 + W3) by SUB2Def2;
then x in the carrier of W1 + W2 by XBOOLE_0:def 4;
then x in {u1 + u2 : u1 in W1 & u2 in W2} by SUB2Def1;
then consider u1, u2 such that
A3: x = u1 + u2 and
A4: u1 in W1 & u2 in W2;
u1 in the carrier of W1 & u2 in the carrier of W2 by A4,STRUCT_0:def 5;
then u1 + u2 in V2 by A2,A1,SUB1Def1;
then
A5: u1 + u2 in W2 by STRUCT_0:def 5;
0.V in W1 /\ W3 & (u1 + u2) + 0.V = u1 + u2 by SUB1Th25,RLVECT_1:4;
then x in {u + v : u in W2 & v in W1 /\ W3} by A3,A5;
hence thesis by SUB2Def1;
end;
theorem
W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
by SUB2Lm11,SUB1Th38;
theorem SUB2Th33:
W1 is strict Submodule of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3
proof
assume
A1: W1 is strict Submodule of W3;
thus (W1 + W2) /\ W3
= (W1 /\ W3) + (W3 /\ W2) by A1,SUB2Lm9,SUB1Th38
.= W1 + (W2 /\ W3) by A1,SUB2Th21;
end;
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 SUB2Th12;
hence thesis by SUB2Th21;
end;
theorem
for W2,W3 being strict Submodule of V holds W1 is Submodule of W2
implies W1 + W3 is Submodule of W2 + W3
proof
let W2,W3 be strict Submodule of V;
assume
A1: W1 is Submodule of W2;
(W1 + W3) + (W2 + W3)
= ((W1 + W3) + W3) + W2 by SUB2Th10
.= (W1 + (W3 + W3)) + W2 by SUB2Th10
.= (W1 + W3) + W2 by SUB2Lm3
.= (W1 + W2) + W3 by SUB2Th10
.= W2 + W3 by A1,SUB2Th12;
hence thesis by SUB2Th12;
end;
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
proof
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
thus
(ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2))
implies W1 is Submodule of W2 or W2 is Submodule of W1
proof
given W such that
A1: the carrier of W = (the carrier of W1) \/ (the carrier of W2);
set VW = the carrier of W;
assume that
A2: not W1 is Submodule of W2 and
A3: not W2 is Submodule of W1;
not VW2 c= VW1 by A3,SUB1Th36;
then consider y being set such that
A4: y in VW2 and
A5: not y in VW1 by TARSKI:def 3;
reconsider y as Element of VW2 by A4;
reconsider y as VECTOR of V by SUB1Th18;
reconsider A1 = VW as Subset of V by SUB1Def2;
A6: A1 is linearly-closed by SUB1Lm1;
not VW1 c= VW2 by A2,SUB1Th36;
then consider x being set such that
A7: x in VW1 and
A8: not x in VW2 by TARSKI:def 3;
reconsider x as Element of VW1 by A7;
reconsider x as VECTOR of V by SUB1Th18;
A9:
now
reconsider A2 = VW2 as Subset of V by SUB1Def2;
A10: A2 is linearly-closed by SUB1Lm1;
assume x + y in VW2;
then (x + y) - y in VW2 by A10,SUB1Th6;
then x + (y - y) in VW2 by RLVECT_1:def 3;
then x + 0.V in VW2 by RLVECT_1:15;
hence contradiction by A8,RLVECT_1:4;
end;
A11:
now
reconsider A2 = VW1 as Subset of V by SUB1Def2;
A12: A2 is linearly-closed by SUB1Lm1;
assume x + y in VW1;
then (y + x) - x in VW1 by A12,SUB1Th6;
then y + (x - x) in VW1 by RLVECT_1:def 3;
then y + 0.V in VW1 by RLVECT_1:15;
hence contradiction by A5,RLVECT_1:4;
end;
x in VW & y in VW by A1,XBOOLE_0:def 3;
then x + y in VW by A6,SUB1Def1;
hence thesis by A1,A11,A9,XBOOLE_0:def 3;
end;
A13:
now
assume W1 is Submodule of W2;
then VW1 c= VW2 by SUB1Def2;
then VW1 \/ VW2 = VW2 by XBOOLE_1:12;
hence thesis;
end;
A14:
now
assume W2 is Submodule of W1;
then VW2 c= VW1 by SUB1Def2;
then VW1 \/ VW2 = VW1 by XBOOLE_1:12;
hence thesis;
end;
assume W1 is Submodule of W2 or W2 is Submodule of W1;
hence thesis by A13,A14;
end;
definition
let V;
func Submodules(V) -> set means :SUB2Def3:
for x holds x in it iff x is strict Submodule of V;
existence
proof
defpred Q[set,set] means ex W being strict Submodule of V
st $2 = W & $1 = the carrier of W;
defpred P[set] means ex W being strict Submodule of V
st $1 = the carrier of W;
consider B being set such that
A1: for x holds x in B iff x in bool(the carrier of V) & P[x]
from XBOOLE_0:sch 1;
A2: for x, y1, y2 st Q[x,y1] & Q[x,y2] holds y1 = y2 by SUB1Th38;
consider f being Function such that
A3: for x, y holds [x,y] in f iff x in B & Q[x,y] from FUNCT_1:sch 1(A2);
for x holds x in B iff ex y st [x,y] in f
proof
let x;
thus x in B implies ex y st [x,y] in f
proof
assume
A4: x in B;
then consider W being strict Submodule of V such that
A5: x = the carrier of W by A1;
reconsider y = W as set;
take y;
thus thesis by A3,A4,A5;
end;
given y such that
A6: [x,y] in f;
thus thesis by A3,A6;
end;
then
A7: B = dom f by RELAT_1:def 4;
for y holds y in rng f iff y is strict Submodule of V
proof
let y;
thus y in rng f implies y is strict Submodule of V
proof
assume y in rng f;
then consider x such that
A8: x in dom f & y = f.x by FUNCT_1:def 3;
[x,y] in f by A8,FUNCT_1:def 2;
then ex W being strict Submodule of V st y = W & x = the carrier of W
by A3;
hence thesis;
end;
assume y is strict Submodule of V;
then reconsider W = y as strict Submodule of V;
reconsider x = the carrier of W as set;
the carrier of W c= the carrier of V by SUB1Def2;
then
A9: x in dom f by A1,A7;
then [x,y] in f by A3,A7;
then y = f.x by A9,FUNCT_1:def 2;
hence thesis by A9,FUNCT_1:def 3;
end;
hence thesis;
end;
uniqueness
proof
let D1, D2 be set;
assume
A10: for x holds x in D1 iff x is strict Submodule of V;
assume
A11: for x holds x in D2 iff x is strict Submodule of V;
now
let x;
thus x in D1 implies x in D2
proof
assume x in D1;
then x is strict Submodule of V by A10;
hence thesis by A11;
end;
assume x in D2;
then x is strict Submodule of V by A11;
hence x in D1 by A10;
end;
hence thesis by TARSKI:1;
end;
end;
registration
let V;
cluster Submodules(V) -> non empty;
coherence
proof
set x = the strict Submodule of V;
x in Submodules(V) by SUB2Def3;
hence thesis;
end;
end;
theorem
for V being strict Z_Module holds V in Submodules(V)
proof
let V be strict Z_Module;
(Omega).V in Submodules(V) by SUB2Def3;
hence thesis;
end;
definition
let V,W1,W2;
pred V is_the_direct_sum_of W1,W2 means :SUB2Def4:
the Z_ModuleStruct of V = W1 + W2 & W1 /\ W2 = (0).V;
end;
SUB2Lm12: 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 Z_ModuleStruct of V
proof
let V be Z_Module, 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) by RLVECT_1:1;
hence thesis by SUB1Th39;
end;
SUB2Lm13: for V being Z_Module, W1,W2 being Submodule of V holds
W1 + W2 = the Z_ModuleStruct 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 Z_Module, W1,W2 be Submodule of V;
thus W1 + W2 = the Z_ModuleStruct 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
proof
assume
A1: W1 + W2 = the Z_ModuleStruct of V;
let v be VECTOR of V;
v in the Z_ModuleStruct of V by RLVECT_1:1;
hence thesis by A1,SUB2Th5;
end;
assume
A2: 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 A2;
hence u in W1 + W2 by SUB2Th5;
end;
hence thesis by SUB2Lm12;
end;
definition
let V be Z_Module;
let W be Submodule of V;
attr W is with_Linear_Compl means :SUB2Def50:
ex C being Submodule of V st V is_the_direct_sum_of C,W;
end;
registration
let V be Z_Module;
cluster with_Linear_Compl for Submodule of V;
correctness
proof
(0).V + (Omega).V = the Z_ModuleStruct of V
& (0).V = (0).V /\ (Omega). V by SUB2Th13,SUB2Th22;
then
V is_the_direct_sum_of (0).V,(Omega).V by SUB2Def4;
then
(Omega).V is with_Linear_Compl by SUB2Def50;
hence thesis;
end;
end;
definition
let V be Z_Module;
let W be Submodule of V;
assume AS: W is with_Linear_Compl;
mode Linear_Compl of W -> Submodule of V means :SUB2Def5:
V is_the_direct_sum_of it,W;
existence by AS,SUB2Def50;
end;
SUB2Lm16: V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1
proof
assume
A1: V is_the_direct_sum_of W1,W2;
then
A2: W2 /\ W1 = (0).V by SUB2Def4;
the Z_ModuleStruct of V = W1 + W2 by A1,SUB2Def4;
hence thesis by A2,SUB2Def4;
end;
theorem
for V being Z_Module, W1, W2 being Submodule of V holds V
is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1
proof
let V be Z_Module, W1, W2 be Submodule of V;
assume V is_the_direct_sum_of W1,W2;
then X1:V is_the_direct_sum_of W2,W1 by SUB2Lm16;
then W1 is with_Linear_Compl by SUB2Def50;
hence thesis by SUB2Def5,X1;
end;
theorem SUB2Th43:
for V being Z_Module, 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 V be Z_Module, W be with_Linear_Compl Submodule of V,
L be Linear_Compl of W;
thus V is_the_direct_sum_of L,W by SUB2Def5;
hence thesis by SUB2Lm16;
end;
theorem
for V being Z_Module, W being with_Linear_Compl Submodule of V, L being
Linear_Compl of W holds W + L = the Z_ModuleStruct of 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 SUB2Th43;
hence W + L = the Z_ModuleStruct of V by SUB2Def4;
end;
theorem
for V being Z_Module, W being with_Linear_Compl Submodule of V,
L being Linear_Compl of W holds W /\ L = (0).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 SUB2Th43;
hence W /\ L = (0).V by SUB2Def4;
end;
theorem
V is_the_direct_sum_of W1,W2
implies V is_the_direct_sum_of W2,W1 by SUB2Lm16;
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 SUB2Def5;
then X1:V is_the_direct_sum_of W,L by SUB2Lm16;
then L is with_Linear_Compl by SUB2Def50;
hence thesis by SUB2Def5,X1;
end;
theorem SUB2Th47:
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;
A1: (0).V + (Omega).V = the Z_ModuleStruct of V
& (0).V = (0).V /\ (Omega). V by SUB2Th13,SUB2Th22;
hence V is_the_direct_sum_of (0).V,(Omega).V by SUB2Def4;
thus thesis by A1,SUB2Def4;
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;
X1: V is_the_direct_sum_of (0).V,(Omega).V &
V is_the_direct_sum_of (Omega).V, (0).V by SUB2Th47;
then
X2: (Omega).V is with_Linear_Compl by SUB2Def50;
(0).V is with_Linear_Compl by X1,SUB2Def50;
hence thesis by SUB2Def5,X1,X2;
end;
reserve C for Coset of W;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;
theorem SUB2Th50:
C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2
proof
set v = the Element of C1 /\ C2;
set C = C1 /\ C2;
assume
A1: C1 /\ C2 <> {};
then reconsider v as Element of V by TARSKI:def 3;
v in C2 by A1,XBOOLE_0:def 4;
then
A2: C2 = v + W2 by SUB1Th94;
v in C1 by A1,XBOOLE_0:def 4;
then
A3: C1 = v + W1 by SUB1Th94;
C is Coset of W1 /\ W2
proof
take v;
thus C c= v + W1 /\ W2
proof
let x;
assume
A4: x in C;
then x in C1 by XBOOLE_0:def 4;
then consider u1 such that
A5: u1 in W1 and
A6: x = v + u1 by A3,SUB1Th79;
x in C2 by A4,XBOOLE_0:def 4;
then consider u2 such that
A7: u2 in W2 and
A8: x = v + u2 by A2,SUB1Th79;
u1 = u2 by A6,A8,RLVECT_1:8;
then u1 in W1 /\ W2 by A5,A7,SUB2Th7;
hence thesis by A6;
end;
let x;
assume x in v + (W1 /\ W2);
then consider u such that
A9: u in W1 /\ W2 and
A10: x = v + u by SUB1Th79;
u in W2 by A9,SUB2Th7;
then
A11: x in {v + u2 : u2 in W2} by A10;
u in W1 by A9,SUB2Th7;
then x in {v + u1 : u1 in W1} by A10;
hence thesis by A3,A2,A11,XBOOLE_0:def 4;
end;
hence thesis;
end;
SUB2Lm17: ex C st v in C
proof
reconsider C = v + W as Coset of W by SUB1Def6;
take C;
thus thesis by SUB1Th59;
end;
theorem SUB2Th51:
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}
proof
let V be Z_Module, W1, W2 be Submodule of V;
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
0.V in W2 by SUB1Th25;
then
A1: 0.V in VW2 by STRUCT_0:def 5;
thus V is_the_direct_sum_of W1,W2 implies
for C1 being Coset of W1, C2 being Coset of W2
ex v being VECTOR of V st C1 /\ C2 = {v}
proof
assume
A2: V is_the_direct_sum_of W1,W2;
then
A3: the Z_ModuleStruct of V = W1 + W2 by SUB2Def4;
let C1 be Coset of W1, C2 be Coset of W2;
consider v1 being VECTOR of V such that
A4: C1 = v1 + W1 by SUB1Def6;
v1 in the Z_ModuleStruct of V by RLVECT_1:1;
then consider v11, v12 being VECTOR of V such that
A5: v11 in W1 and
A6: v12 in W2 and
A7: v1 = v11 + v12 by A3,SUB2Th5;
consider v2 being VECTOR of V such that
A8: C2 = v2 + W2 by SUB1Def6;
v2 in the Z_ModuleStruct of V by RLVECT_1:1;
then consider v21, v22 being VECTOR of V such that
A9: v21 in W1 and
A10: v22 in W2 and
A11: v2 = v21 + v22 by A3,SUB2Th5;
take v = v12 + v21;
{v} = C1 /\ C2
proof
thus
A12: {v} c= C1 /\ C2
proof
let x;
assume x in {v};
then
A13: x = v by TARSKI:def 1;
v21 = v2 - v22 by A11,RLSUB_2:61;
then v21 in C2 by A8,A10,SUB1Th80;
then C2 = v21 + W2 by SUB1Th94;
then
A14: x in C2 by A6,A13;
v12 = v1 - v11 by A7,RLSUB_2:61;
then v12 in C1 by A4,A5,SUB1Th80;
then C1 = v12 + W1 by SUB1Th94;
then x in C1 by A9,A13;
hence thesis by A14,XBOOLE_0:def 4;
end;
let x;
assume
A15: x in C1 /\ C2;
then C1 meets C2 by XBOOLE_0:4;
then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by SUB2Th50;
A16: v in {v} by TARSKI:def 1;
W1 /\ W2 = (0).V by A2,SUB2Def4;
then ex u being VECTOR of V st C = {u} by SUB1Th89;
hence thesis by A12,A15,A16,TARSKI:def 1;
end;
hence thesis;
end;
assume
A17: for C1 being Coset of W1, C2 being Coset of W2
ex v being VECTOR of V st C1 /\ C2 = {v};
A18: VW2 is Coset of W2 by SUB1Th90;
now
let u be VECTOR of V;
consider C1 being Coset of W1 such that
A19: u in C1 by SUB2Lm17;
consider v being VECTOR of V such that
A20: C1 /\ VW2 = {v} by A18,A17;
A21: v in {v} by TARSKI:def 1;
then v in C1 by A20,XBOOLE_0:def 4;
then consider v1 being VECTOR of V such that
A22: v1 in W1 and
A23: u - v1 = v by A19,SUB1Th96;
v in VW2 by A20,A21,XBOOLE_0:def 4;
then
A24: v in W2 by STRUCT_0:def 5;
u = v1 + v by A23,RLSUB_2:61;
hence u in W1 + W2 by A24,A22,SUB2Th5;
end;
hence the Z_ModuleStruct of V = W1 + W2 by SUB2Lm12;
VW1 is Coset of W1 by SUB1Th90;
then consider v being VECTOR of V such that
A25: VW1 /\ VW2 = {v} by A18,A17;
0.V in W1 by SUB1Th25;
then 0.V in VW1 by STRUCT_0:def 5;
then
A26: 0.V in {v} by A25,A1,XBOOLE_0:def 4;
the carrier of (0).V = {0.V} by SUB1Def3
.= VW1 /\ VW2 by A25,A26,TARSKI:def 1
.= the carrier of W1 /\ W2 by SUB2Def2;
hence thesis by SUB1Th38;
end;
theorem
for V being Z_Module, W1,W2 being Submodule of V holds
W1 + W2 = the Z_ModuleStruct 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 SUB2Lm13;
theorem SUB2Th53:
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
proof
reconsider C2 = v1 + W2 as Coset of W2 by SUB1Def6;
reconsider C1 = the carrier of W1 as Coset of W1 by SUB1Th90;
A1: v1 in C2 by SUB1Th59;
assume V is_the_direct_sum_of W1,W2;
then consider u being VECTOR of V such that
A2: C1 /\ C2 = {u} by SUB2Th51;
assume that
A3: v1 + v2 = u1 + u2 and
A4: v1 in W1 and
A5: u1 in W1 and
A6: v2 in W2 & u2 in W2;
A7: v2 - u2 in W2 by A6,SUB1Th31;
v1 in C1 by A4,STRUCT_0:def 5;
then v1 in C1 /\ C2 by A1,XBOOLE_0:def 4;
then
A8: v1 = u by A2,TARSKI:def 1;
u1 = (v1 + v2) - u2 by A3,RLSUB_2:61
.= v1 + (v2 - u2) by RLVECT_1:def 3;
then
A9: u1 in C2 by A7;
u1 in C1 by A5,STRUCT_0:def 5;
then
A10: u1 in C1 /\ C2 by A9,XBOOLE_0:def 4;
hence v1 = u1 by A2,A8,TARSKI:def 1;
u1 = u by A10,A2,TARSKI:def 1;
hence thesis by A3,A8,RLVECT_1:8;
end;
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 SUB1Th51,SUB1Def3;
then
A2: {0.V} c= the carrier of W1 /\ W2 by SUB1Def2;
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 W1 /\ W2 <> (0).V by A1,SUB2Def4;
then the carrier of W1 /\ W2 <> {0.V} by SUB1Def3;
then {0.V} c< the carrier of W1 /\ W2 by A2,XBOOLE_0:def 8;
then consider x 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,STRUCT_0:def 5;
then x in V by SUB1Th17;
then reconsider u = x as VECTOR of V by STRUCT_0:def 5;
consider v1, v2 such that
A8: v1 in W1 and
A9: v2 in W2 and
A10: v = v1 + v2 by A1,SUB2Lm13;
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,SUB2Th7;
then
A12: v2 - u in W2 by A9,SUB1Th31;
x in W1 by A7,SUB2Th7;
then v1 + u in W1 by A8,SUB1Th28;
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
let V,v,W1,W2;
assume
A1: V is_the_direct_sum_of W1,W2;
func v |-- (W1,W2) -> Element of [:the carrier of V, the carrier of V:]
means :SUB2Def6:
v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
existence
proof
W1 + W2 = the Z_ModuleStruct of V by A1,SUB2Def4;
then consider v1, v2 such that
A2: v1 in W1 & v2 in W2 & v = v1 + v2 by SUB2Lm13;
take [v1,v2];
[v1,v2]`1 = v1 by MCART_1:7;
hence thesis by A2,MCART_1:7;
end;
uniqueness
proof
let t1, t2 be
Element of [:the carrier of V, the carrier of V:];
assume v = t1`1 + t1`2 & t1`1 in W1 & t1`2 in W2 & v = t2`1 + t2`2 & t2`1
in W1 & t2`2 in W2;
then
A3: t1`1 = t2`1 & t1`2 = t2`2 by A1,SUB2Th53;
t1 = [t1`1,t1`2] by MCART_1:21;
hence thesis by A3,MCART_1:21;
end;
end;
theorem SUB2Th59:
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2
proof
assume
A1: V is_the_direct_sum_of W1,W2;
then
A2: (v |-- (W1,W2))`2 in W2 by SUB2Def6;
A3: V is_the_direct_sum_of W2,W1 by A1,SUB2Lm16;
then
A4: v = (v |-- (W2,W1))`2 + (v |-- (W2,W1))`1
& (v |-- (W2,W1))`1 in W2 by SUB2Def6;
A5: (v |-- (W2,W1))`2 in W1 by A3,SUB2Def6;
v = (v |-- (W1,W2))`1 + (v |-- (W1,W2))`2 & (v |-- (W1,W2))`1 in W1
by A1,SUB2Def6;
hence thesis by A1,A2,A4,A5,SUB2Th53;
end;
theorem SUB2Th60:
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1
proof
assume
A1: V is_the_direct_sum_of W1,W2;
then
A2: (v |-- (W1,W2))`2 in W2 by SUB2Def6;
A3: V is_the_direct_sum_of W2,W1 by A1,SUB2Lm16;
then
A4: v = (v |-- (W2,W1))`2 + (v |-- (W2,W1))`1
& (v |-- (W2,W1))`1 in W2 by SUB2Def6;
A5: (v |-- (W2,W1))`2 in W1 by A3,SUB2Def6;
v = (v |-- (W1,W2))`1 + (v |-- (W1,W2))`2 & (v |-- (W1,W2))`1 in W1
by A1,SUB2Def6;
hence thesis by A1,A2,A4,A5,SUB2Th53;
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,
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 SUB2Th43;
hence thesis by SUB2Def6;
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 SUB2Th43;
hence thesis by SUB2Def6;
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 SUB2Th43;
hence thesis by SUB2Def6;
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
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 SUB2Th43;
hence thesis by SUB2Th59;
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))`2 = (v |-- (L,W))`1
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 SUB2Th43;
hence thesis by SUB2Th60;
end;
reserve A1,A2,B for Element of Submodules(V);
definition
let V;
func SubJoin(V) -> BinOp of Submodules(V) means :SUB2Def7:
for A1, A2, W1, W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
existence
proof
defpred P[Element of Submodules(V),Element of Submodules(V), Element of
Submodules(V)] means for W1, W2 st $1 = W1 & $2 = W2 holds $3 = W1 + W2;
A1: for A1, A2 ex B st P[A1,A2,B]
proof
let A1, A2;
reconsider W1 = A1, W2 = A2 as Submodule of V by SUB2Def3;
reconsider C = W1 + W2 as Element of Submodules(V) by SUB2Def3;
take C;
thus thesis;
end;
ex o being BinOp of Submodules(V) st for a, b being Element of Submodules
(V) holds P[a,b,o.(a,b)] from BINOP_1:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let o1, o2 be BinOp of Submodules(V);
assume
A2: for A1, A2, W1, W2 st A1 = W1 & A2 = W2 holds o1.(A1,A2) = W1 + W2;
assume
A3: for A1, A2, W1, W2 st A1 = W1 & A2 = W2 holds o2.(A1,A2) = W1 + W2;
now
let x, y be set;
assume
A4: x in Submodules(V) & y in Submodules(V);
then reconsider A = x, B = y as Element of Submodules(V);
reconsider W1 = x, W2 = y as Submodule of V by A4,SUB2Def3;
o1.(A,B) = W1 + W2 by A2;
hence o1.(x,y) = o2.(x,y) by A3;
end;
hence thesis by BINOP_1:1;
end;
end;
definition
let V;
func SubMeet(V) -> BinOp of Submodules(V) means :SUB2Def8:
for A1, A2, W1, W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
existence
proof
defpred P[Element of Submodules(V),Element of Submodules(V), Element of
Submodules(V)] means for W1, W2 st $1 = W1 & $2 = W2 holds $3 = W1 /\ W2;
A1: for A1, A2 ex B st P[A1,A2,B]
proof
let A1, A2;
reconsider W1 = A1, W2 = A2 as Submodule of V by SUB2Def3;
reconsider C = W1 /\ W2 as Element of Submodules(V) by SUB2Def3;
take C;
thus thesis;
end;
ex o being BinOp of Submodules(V) st for a,b being Element of
Submodules(V) holds P[a,b,o.(a,b)] from BINOP_1:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let o1, o2 be BinOp of Submodules(V);
assume
A2: for A1, A2, W1, W2 st A1 = W1 & A2 = W2 holds o1.(A1,A2) = W1 /\ W2;
assume
A3: for A1, A2, W1, W2 st A1 = W1 & A2 = W2 holds o2.(A1,A2) = W1 /\ W2;
now
let x, y be set;
assume
A4: x in Submodules(V) & y in Submodules(V);
then reconsider A = x, B = y as Element of Submodules(V);
reconsider W1 = x, W2 = y as Submodule of V by A4,SUB2Def3;
o1.(A,B) = W1 /\ W2 by A2;
hence o1.(x,y) = o2.(x,y) by A3;
end;
hence thesis by BINOP_1:1;
end;
end;
theorem SUB2Th70:
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice
proof
set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
A1: for A, B being Element of S holds A "/\" B = B "/\" A
proof
let A, B be Element of S;
reconsider W1 = A, W2 = B as Submodule of V by SUB2Def3;
thus A "/\" B = W1 /\ W2 by SUB2Def8
.= B "/\" A by SUB2Def8;
end;
A2: for A, B being Element of S holds (A "/\" B) "\/" B = B
proof
let A, B be Element of S;
reconsider W1 = A, W2 = B as strict Submodule of V by SUB2Def3;
reconsider AB = W1 /\ W2 as Element of S by SUB2Def3;
thus (A "/\" B) "\/" B = SubJoin(V).(AB,B) by SUB2Def8
.= (W1 /\ W2) + W2 by SUB2Def7
.= B by SUB2Lm6,SUB1Th38;
end;
A3: for A, B, C being Element of S holds
A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A, B, C be Element of S;
reconsider W1 = A, W2 = B, W3 = C as Submodule of V by SUB2Def3;
reconsider AB = W1 + W2, BC = W2 + W3 as Element of S by SUB2Def3;
thus A "\/" (B "\/" C) = SubJoin(V).(A,BC) by SUB2Def7
.= W1 + (W2 + W3) by SUB2Def7
.= (W1 + W2) + W3 by SUB2Th10
.= SubJoin(V).(AB,C) by SUB2Def7
.= (A "\/" B) "\/" C by SUB2Def7;
end;
A4: for A, B being Element of S holds A "/\" (A "\/" B) = A
proof
let A, B be Element of S;
reconsider W1 = A, W2 = B as strict Submodule of V by SUB2Def3;
reconsider AB = W1 + W2 as Element of S by SUB2Def3;
thus A "/\" (A "\/" B) = SubMeet(V).(A,AB) by SUB2Def7
.= W1 /\ (W1 + W2) by SUB2Def8
.= A by SUB2Lm7,SUB1Th38;
end;
A5: for A, B, C being Element of S holds
A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A, B, C be Element of S;
reconsider W1 = A, W2 = B, W3 = C as Submodule of V by SUB2Def3;
reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of S by SUB2Def3;
thus A "/\" (B "/\" C) = SubMeet(V).(A,BC) by SUB2Def8
.= W1 /\ (W2 /\ W3) by SUB2Def8
.= (W1 /\ W2) /\ W3 by SUB2Th19
.= SubMeet(V).(AB,C) by SUB2Def8
.= (A "/\" B) "/\" C by SUB2Def8;
end;
for A, B being Element of S holds A "\/" B = B "\/" A
proof
let A, B be Element of S;
reconsider W1 = A, W2 = B as Submodule of V by SUB2Def3;
thus A "\/" B = W1 + W2 by SUB2Def7
.= B "\/" A by SUB2Def7;
end;
then S is join-commutative join-associative
meet-absorbing meet-commutative meet-associative join-absorbing
by A3,A2,A1,A5,A4,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
hence thesis;
end;
registration
let V;
cluster LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #)
-> Lattice-like;
coherence by SUB2Th70;
end;
theorem SUB2Th71:
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is lower-bounded
proof
let V be Z_Module;
set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
ex C being Element of S st for A being Element of S holds C "/\" A = C &
A "/\" C = C
proof
reconsider C = (0).V as Element of S by SUB2Def3;
take C;
let A be Element of S;
reconsider W = A as Submodule of V by SUB2Def3;
thus C "/\" A = (0).V /\ W by SUB2Def8
.= C by SUB2Th22;
hence thesis;
end;
hence thesis by LATTICES:def 13;
end;
theorem SUB2Th72:
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is upper-bounded
proof
let V be Z_Module;
set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
ex C being Element of S st for A being Element of S holds C "\/" A = C &
A "\/" C = C
proof
reconsider C = (Omega).V as Element of S by SUB2Def3;
take C;
let A be Element of S;
reconsider W = A as Submodule of V by SUB2Def3;
thus C "\/" A = (Omega).V + W by SUB2Def7
.= C by SUB2Th15;
hence thesis;
end;
hence thesis by LATTICES:def 14;
end;
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 SUB2Th71,SUB2Th72;
hence thesis;
end;
theorem
for V being Z_Module holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is modular
proof
let V be Z_Module;
set S = LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #);
for A, B, C being Element of S st A [= C holds A "\/" (B "/\" C) = (A "\/"
B) "/\" C
proof
let A, B, C be Element of S;
reconsider W1 = A, W2 = B, W3 = C as strict Submodule of V by SUB2Def3;
assume
A1: A [= C;
reconsider AB = W1 + W2 as Element of S by SUB2Def3;
reconsider BC = W2 /\ W3 as Element of S by SUB2Def3;
W1 + W3 = A "\/" C by SUB2Def7
.= W3 by A1,LATTICES:def 3;
then
A2: W1 is Submodule of W3 by SUB2Th12;
thus A "\/" (B "/\" C) = SubJoin(V).(A,BC) by SUB2Def8
.= W1 + (W2 /\ W3) by SUB2Def7
.= (W1 + W2) /\ W3 by A2,SUB2Th33
.= SubMeet(V).(AB,C) by SUB2Def8
.= (A "\/" B) "/\" C by SUB2Def7;
end;
hence thesis by LATTICES:def 12;
end;
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 SUB2Def3;
assume
A1: W1 is Submodule of W2;
A "\/" B = W1 + W2 by SUB2Def7
.= B by A1,SUB2Th12;
then A [= B by LATTICES:def 3;
then A "/\" C [= B "/\" C by LATTICES:9;
then
A2: (A "/\" C) "\/" (B "/\" C) = (B "/\" C) by LATTICES:def 3;
A3: B "/\" C = W2 /\ W3 by SUB2Def8;
(A "/\" C) "\/" (B "/\" C) = SubJoin(V).(SubMeet(V).(A,C),BC) by SUB2Def8
.= SubJoin(V).(AC,BC) by SUB2Def8
.= (W1 /\ W3) + (W2 /\ W3) by SUB2Def7;
hence thesis by A2,A3,SUB2Th12;
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 Z_ModuleStruct of V by SUB2Lm12;
theorem
ex C st v in C by SUB2Lm17;
begin :: 4.Transformation of Abelian group to Z-module
definition
let AG be non empty addLoopStr;
func Int-mult-left(AG) -> Function of
[:INT,the carrier of AG:], the carrier of AG means :DefIntMult:
for i being Element of INT, 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 INT,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));
P1: for x being Element of INT for y being Element of AG
ex z being Element of AG st P[x,y,z]
proof
let x be Element of INT, y be Element of AG;
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 X2: 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] by X2;
hence thesis;
end;
end;
consider f being Function of [:INT,the carrier of AG:],the carrier of AG
such that
P2: for x being Element of INT for y being Element of the carrier of AG
holds P[x,y,f.(x,y)] from BINOP_1:sch 3(P1);
take f;
thus thesis by P2;
end;
uniqueness
proof
let f1, f2 be Function of [:INT,the carrier of AG:], the carrier of AG;
assume
X1: for i being Element of INT,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
X2: for i being Element of INT,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 X10: x in INT & y in the carrier of AG;
then
reconsider x0=x as Element of INT;
reconsider y0=y as Element of AG by X10;
per cases;
suppose C1: 0 <= x0;
hence f1.(x,y) = (Nat-mult-left(AG)).(x0,y0) by X1
.= f2.(x,y) by X2,C1;
end;
suppose C2: 0 > x0;
hence f1.(x,y) = (Nat-mult-left(AG)).(-x0,-y0) by X1
.= f2.(x,y) by X2,C2;
end;
end;
hence f1=f2 by BINOP_1:def 21;
end;
end;
theorem
for R being non empty addLoopStr, a being Element of R,
i be Element of INT, i1 be Element of NAT st i=i1 holds
(Int-mult-left(R)).(i,a) = i1 * a by DefIntMult;
theorem IntMultTh13:
for R being non empty addLoopStr, a being Element of R,
i be Element of INT 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 Element of INT;
assume i=0;
hence (Int-mult-left(R)).(i,a) = 0 * a by DefIntMult
.=0.R by BINOM:12;
end;
theorem IntMultTh13G:
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 being add-associative right_zeroed right_complementable
non empty addLoopStr,
i be Element of NAT;
defpred P[Element of NAT] means (Nat-mult-left(R)).($1,0.R) = 0.R;
P1: P[0] by BINOM:def 3;
P2: for n be Element of NAT st P[n] holds P[n+1]
proof
let n be Element of NAT;
assume P2:P[n];
(Nat-mult-left(R)).(n+1,0.R) = 0.R + 0.R by P2,BINOM:def 3
.= 0.R by RLVECT_1:4;
hence P[n+1];
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(P1,P2);
hence thesis;
end;
theorem IntMultTh13F:
for R being add-associative right_zeroed right_complementable
non empty addLoopStr,
i be Element of INT holds
(Int-mult-left(R)).(i,0.R) = 0.R
proof
let R being add-associative right_zeroed right_complementable
non empty addLoopStr,
i be 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 DefIntMult
.=0.R by IntMultTh13G;
end;
suppose X2: 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 DefIntMult,X2
.= (Nat-mult-left(R)).(i1,0.R) by RLVECT_1:12
.=0.R by IntMultTh13G;
end;
end;
theorem IntMultTh14:
for R being right_zeroed non empty addLoopStr, a being Element of R,
i be Element of INT 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 Element of INT;
assume i=1;
hence (Int-mult-left(R)).(i,a) = 1 * a by DefIntMult
.= a by BINOM:13;
end;
theorem IntMultTh16A:
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 AS: i <= j & k = j-i;
A2:j*a = (k+i)*a by AS
.= 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 IntMultTh16B:
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[Element of NAT] means
(Nat-mult-left(R)).($1,a) + (Nat-mult-left(R)).($1,-a) =0.R;
P1: 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;
P2: for n be Element of NAT st P[n] holds P[n+1]
proof
let n be Element of NAT;
assume P2: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 P2,RLVECT_1:4
.= 0.R by RLVECT_1:5;
hence P[n+1];
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(P1,P2);
then
(Nat-mult-left(R)).(i,a) + (Nat-mult-left(R)).(i,-a) =0.R;
hence thesis by RLVECT_1:6;
end;
theorem IntMultTh16C:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT
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;
assume AS: i in NAT & not j in NAT;
then
reconsider i1=i as Element of NAT;
X0: j < 0 by AS,INT_1:3;
then
reconsider j1=-j as Element of NAT by INT_1:3;
Y0: i+j is Element of INT by INT_1:def 2;
per cases;
suppose X4: j1 <= i1;
reconsider k1=i1-j1 as Element of NAT by X4,INT_1:5;
thus (Int-mult-left(R)).(i+j,a) = (Nat-mult-left(R)).(k1,a)
by Y0,DefIntMult
.= (Nat-mult-left(R)).(i1,a) - (Nat-mult-left(R)).(j1,a)
by IntMultTh16A,X4
.=(Nat-mult-left(R)).(i1,a) + (Nat-mult-left(R)).(j1,-a)
by IntMultTh16B
.=(Int-mult-left(R)).(i,a) + (Nat-mult-left(R)).(j1,-a)
by DefIntMult
.=(Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a) by X0,DefIntMult;
end;
suppose Y6: j1 > i1;
then
reconsider k1=j1-i1 as Element of NAT by INT_1:5;
X5: i1-j1 < 0 by Y6,XREAL_1:49;
thus (Int-mult-left(R)).(i+j,a) = (Nat-mult-left(R)).(-(i1-j1),-a)
by Y0,X5,DefIntMult
.= (Nat-mult-left(R)).(k1,-a)
.= (Nat-mult-left(R)).(j1,-a) - (Nat-mult-left(R)).(i1,-a)
by IntMultTh16A,Y6
.=(Nat-mult-left(R)).(j1,-a) + (Nat-mult-left(R)).(i1,-(-a))
by IntMultTh16B
.=(Nat-mult-left(R)).(j1,-a) + (Nat-mult-left(R)).(i1,a)
by RLVECT_1:17
.=(Int-mult-left(R)).(j,a) + (Nat-mult-left(R)).(i1,a)
by X0,DefIntMult
.=(Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a) by DefIntMult;
end;
end;
theorem IntMultTh16:
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a being Element of R, i, j being Element of INT
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 being Element of R, i, j being 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;
X0: i+j is Element of INT by INT_1:def 2;
thus (Int-mult-left(R)).(i+j,a)
= (i1+j1)*a by X0,DefIntMult
.= i1*a + j1*a by BINOM:15
.= (Int-mult-left(R)).(i,a) + (Nat-mult-left(R)).(j1,a) by DefIntMult
.= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a) by DefIntMult;
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 IntMultTh16C;
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 IntMultTh16C;
end;
suppose not i in NAT & not j in NAT;
then
X0: i < 0 & j < 0 by INT_1:3;
then
reconsider i1=-i as Element of NAT by INT_1:3;
reconsider j1=-j as Element of NAT by X0,INT_1:3;
X6: -(i+j) = i1+j1;
Y0: i+j is Element of INT by INT_1:def 2;
thus (Int-mult-left(R)).(i+j,a)
=(i1+j1)*(-a) by X0,X6,Y0,DefIntMult
.=i1*(-a) + j1*(-a) by BINOM:15
.= (Int-mult-left(R)).(i,a) + (Nat-mult-left(R)).(j1,-a)
by X0,DefIntMult
.= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(j,a) by X0,DefIntMult;
end;
end;
theorem IntMultTh17A:
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[Element of NAT] means (Nat-mult-left(R)).($1,a+b)
= (Nat-mult-left(R)).($1,a) + (Nat-mult-left(R)).($1,b);
P1: 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;
P2: for n be Element of NAT st P[n] holds P[n+1]
proof
let n be Element of NAT;
assume P2: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 P2,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 Element of NAT holds P[n] from NAT_1:sch 1(P1,P2);
hence thesis;
end;
theorem IntMultTh17:
for R being Abelian right_zeroed add-associative
right_complementable non empty addLoopStr,
a, b being Element of R, i being Element of INT
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;
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 DefIntMult
.= i1*a + i1*b by IntMultTh17A
.= (Int-mult-left(R)).(i,a) + (Nat-mult-left(R)).(i1,b) by DefIntMult
.= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(i,b) by DefIntMult;
end;
suppose A4: 0 > i;
then
reconsider i1=-i 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
X4: -(a+b) = (-a) + (-b ) by RLVECT_1:6;
thus (Int-mult-left(R)).(i,a+b) = (Nat-mult-left(R)).(i1,-(a+b))
by DefIntMult,A4
.=i1*(-a) + i1*(-b) by X4,IntMultTh17A
.= (Int-mult-left(R)).(i,a) + (Nat-mult-left(R)).(i1,-b)
by A4,DefIntMult
.= (Int-mult-left(R)).(i,a) + (Int-mult-left(R)).(i,b)
by A4,DefIntMult;
end;
end;
theorem IntMultTh18A:
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[Element of NAT] means (Nat-mult-left(R)).($1*j,a)
=(Nat-mult-left(R)).($1,(Nat-mult-left(R)).(j,a));
P1: 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;
P2: for n be Element of NAT st P[n] holds P[n+1]
proof
let n be Element of NAT;
assume P2: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 P2,BINOM:def 3;
hence P[n+1];
end;
for n be Element of NAT holds P[n] from NAT_1:sch 1(P1,P2);
hence thesis;
end;
IntMultTh18B:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT 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;
assume AS: i <> 0 & j <> 0;
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;
X0: i*j is Element of INT by INT_1:def 2;
thus (Int-mult-left(R)).(i*j,a)
= (Nat-mult-left(R)).(i1*j1,a) by X0,DefIntMult
.= (Nat-mult-left(R)).(i1,(Nat-mult-left(R)).(j1,a)) by IntMultTh18A
.= (Nat-mult-left(R)).(i1,(Int-mult-left(R)).(j,a)) by DefIntMult
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by DefIntMult;
end;
suppose A2: i in NAT & not j in NAT;
then
X0: 0 < i & j < 0 by AS,INT_1:3;
reconsider i1= i as Element of NAT by A2;
reconsider j1=-j as Element of NAT by X0,INT_1:3;
X6: -(i*j) = i1*j1;
X5: j*i < 0 * i by X0,XREAL_1:68;
i*j is Element of INT by INT_1:def 2;
hence (Int-mult-left(R)).(i*j,a)
=(Nat-mult-left(R)).(i1*j1,-a) by X5,X6,DefIntMult
.= (Nat-mult-left(R)).(i1,(Nat-mult-left(R)).(j1,-a)) by IntMultTh18A
.= (Nat-mult-left(R)).(i1,(Int-mult-left(R)).(j,a)) by DefIntMult,X0
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by DefIntMult;
end;
suppose A3: not i in NAT & j in NAT;
then
X0: 0 < j & i < 0 by AS,INT_1:3;
then
reconsider i1= -i as Element of NAT by INT_1:3;
reconsider j1= j as Element of NAT by A3;
X6: -(i*j) = i1*j1;
X5: i*j < 0 * j by X0,XREAL_1:68;
Y0: i*j is Element of INT by INT_1:def 2;
thus (Int-mult-left(R)).(i*j,a)
=(Nat-mult-left(R)).(i1*j1,-a) by X5,X6,Y0,DefIntMult
.= (Nat-mult-left(R)).(i1,(Nat-mult-left(R)).(j1,-a)) by IntMultTh18A
.= (Nat-mult-left(R)).(i1,-((Nat-mult-left(R)).(j1,a))) by IntMultTh16B
.= (Nat-mult-left(R)).(i1,-(Int-mult-left(R)).(j,a)) by DefIntMult
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by X0,DefIntMult;
end;
suppose not i in NAT & not j in NAT;
then
X0: i < 0 & j < 0 by INT_1:3;
then
reconsider i1=-i as Element of NAT by INT_1:3;
reconsider j1=-j as Element of NAT by X0,INT_1:3;
Y0: i*j is Element of INT by INT_1:def 2;
-(Nat-mult-left(R)).(j1,a) = (Nat-mult-left(R)).(j1,-a) by IntMultTh16B;
then
(Nat-mult-left(R)).(j1,-a) + (Nat-mult-left(R)).(j1,a) = 0.R
by RLVECT_1:def 10;
then
Y1: (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 Y0,DefIntMult
.= (Nat-mult-left(R)).(i1,(Nat-mult-left(R)).(j1,a))
by IntMultTh18A
.= (Nat-mult-left(R)).(i1,-((Int-mult-left(R)).(j,a)))
by X0,Y1,DefIntMult
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a))
by X0,DefIntMult;
end;
end;
IntMultTh18C:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT 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;
assume AS: i = 0 or j = 0;
per cases by AS;
suppose A1: i = 0;
hence (Int-mult-left(R)).(i*j,a) = 0.R by IntMultTh13
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by A1,IntMultTh13;
end;
suppose A2: j = 0;
hence (Int-mult-left(R)).(i*j,a) = 0.R by IntMultTh13
.= (Int-mult-left(R)).(i,0.R) by IntMultTh13F
.= (Int-mult-left(R)).(i,(Int-mult-left(R)).(j,a)) by IntMultTh13,A2;
end;
end;
theorem IntMultTh18:
for R being Abelian right_zeroed add-associative right_complementable
non empty addLoopStr,
a being Element of R, i, j being Element of INT 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;
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 IntMultTh18C;
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 IntMultTh18B;
end;
end;
theorem
for AG be non empty Abelian add-associative right_zeroed
right_complementable addLoopStr holds
Z_ModuleStruct(# the carrier of AG, the ZeroF of AG, the addF 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 = Z_ModuleStruct(# the carrier of AG, the ZeroF of AG, the addF of AG,
Int-mult-left(AG) #) as non empty Z_ModuleStruct;
set ML= the Mult 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);
P1: for v, w being Element of ZS holds v + w = w + v
proof
let v, w being Element of ZS;
reconsider v1=v,w1=w as Element of AG;
thus v + w = v1+w1
.= w1+v1
.= w+v;
end;
P2: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
proof
let u, v, w being 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;
P3: 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;
P4: now
let v be VECTOR of ZS;
reconsider v1=v as Element of AG;
consider w1 being Element of AG such that
P2: v1+w1 = 0.AG by ALGSTR_0:def 11;
reconsider w=w1 as Element of ZS;
v+w = 0.ZS by P2;
hence v is right_complementable by ALGSTR_0:def 11;
end;
P5: for a, b be integer number, v being VECTOR of ZS
holds (a + b) * v = a * v + b * v
proof
let a, b be integer number, v being VECTOR of ZS;
reconsider a1=a,b1=b as Element of INT by INT_1:def 2;
reconsider v1=v as Element of AG;
thus (a+b) * v = MLI.(a1,v1) + MLI.(b1,v1) by IntMultTh16
.= a * v + b * v;
end;
P6: for a be integer number, v, w being VECTOR of ZS
holds a * (v + w) = a * v + a * w
proof
let a be integer number, v, w being VECTOR of ZS;
reconsider a1=a as Element of INT by INT_1:def 2;
reconsider v1=v,w1=w as Element of AG;
thus a * (v + w) = MLI.(a1,v1+w1)
.= MLI.(a1,v1) + MLI.(a1,w1) by IntMultTh17
.= a * v + a * w;
end;
P7: for a, b be integer number for v being VECTOR of
ZS holds (a * b) * v = a * (b * v)
proof
let a, b be integer number, v be VECTOR of ZS;
reconsider a1=a, b1=b as Element of INT by INT_1:def 2;
reconsider v1=v as Element of AG;
thus (a*b) * v = MLI.(a1,MLI.(b1,v1)) by IntMultTh18
.= a * (b * v);
end;
for v being VECTOR of ZS holds 1 * v = v
proof
let v be VECTOR of ZS;
reconsider i=1 as Element of INT by INT_1:def 2;
reconsider v1=v as Element of AG;
thus 1 * v = MLI.(i,v1)
.= v by IntMultTh14;
end;
hence thesis by P1,P2,P3,P4,P5,P6,P7,RL1Def8,RL1Def9,RL1Def10,RL1Def11,
ALGSTR_0:def 16,RLVECT_1:def 2,def 3,def 4;
end;