:: Operations on Submodules in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCSDOM, VECTSP_2, RMOD_2, VECTSP_1, ARYTM_3, STRUCT_0,
SUBSET_1, TARSKI, SUPINF_2, RLSUB_1, XBOOLE_0, ARYTM_1, ZFMISC_1,
FUNCT_1, RELAT_1, RLSUB_2, FINSEQ_4, MCART_1, BINOP_1, LATTICES, EQREL_1,
PBOOLE, RMOD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1,
STRUCT_0, LATTICES, RLVECT_1, DOMAIN_1, VECTSP_1, VECTSP_2, RMOD_2;
constructors BINOP_1, DOMAIN_1, LATTICES, RMOD_2;
registrations SUBSET_1, STRUCT_0, LATTICES, VECTSP_2, RMOD_2, RELAT_1,
XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, RMOD_2, XBOOLE_0;
equalities RMOD_2, XBOOLE_0, RLVECT_1, STRUCT_0;
expansions TARSKI, RMOD_2, XBOOLE_0, STRUCT_0;
theorems BINOP_1, FUNCT_1, LATTICES, MCART_1, TARSKI, VECTSP_1, ZFMISC_1,
RMOD_2, RLVECT_1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes BINOP_1, FUNCT_1, XBOOLE_0;
begin
reserve R for Ring,
V for RightMod of R,
W,W1,W2,W3 for Submodule of V,
u,u1, u2,v,v1,v2 for Vector of V,
x,y,y1,y2 for object;
definition
let R;
let V;
let W1,W2;
func W1 + W2 -> strict Submodule of V means
:Def1:
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 RMOD_2:def 2;
set VS = {v + u where u,v is Element of V: v in W1 & u in W2};
VS c= the carrier of V
proof
let x be object;
assume x in VS;
then ex v2,v1 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:def 4;
0.V in W1 & 0.V in W2 by RMOD_2:17;
then
A2: 0.V in VS by A1;
A3: VS = {v + u where u,v is Element of V : v in V1 & u in V2}
proof
thus VS c= {v + u where u,v is Element of V: v in V1 & u in V2}
proof
let x be object;
assume x in VS;
then consider u,v such that
A4: x = v + u and
A5: v in W1 & u in W2;
v in V1 & u in V2 by A5;
hence thesis by A4;
end;
let x be object;
assume x in {v + u where u,v is Element of V: v in V1 & u in V2};
then consider u,v such that
A6: x = v + u and
A7: v in V1 & u in V2;
v in W1 & u in W2 by A7;
hence thesis by A6;
end;
V1 is linearly-closed & V2 is linearly-closed by RMOD_2:33;
hence thesis by A2,A3,RMOD_2:6,34;
end;
uniqueness by RMOD_2:29;
end;
definition
let R;
let V;
let W1,W2;
func W1 /\ W2 -> strict Submodule of V means
:Def2:
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 RMOD_2:17;
then
A1: 0.V in VW2;
VW1 c= VV & VW2 c= VV by RMOD_2:def 2;
then VW1 /\ VW2 c= VV /\ VV by XBOOLE_1:27;
then reconsider V1 = VW1, V2 = VW2, V3 = VW1 /\ VW2 as Subset of V by
RMOD_2:def 2;
V1 is linearly-closed & V2 is linearly-closed by RMOD_2:33;
then
A2: V3 is linearly-closed by RMOD_2:7;
0.V in W1 by RMOD_2:17;
then 0.V in VW1;
then VW1 /\ VW2 <> {} by A1,XBOOLE_0:def 4;
hence thesis by A2,RMOD_2:34;
end;
uniqueness by RMOD_2:29;
end;
theorem Th1:
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;
then x in {v + u : v in W1 & u in W2} by Def1;
then consider v2,v1 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 Def1;
hence thesis;
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 RLVECT_1:def 4,RMOD_2:17;
hence thesis by A2,Th1;
end;
suppose
A3: v in W2;
v = 0.V + v & 0.V in W1 by RLVECT_1:def 4,RMOD_2:17;
hence thesis by A3,Th1;
end;
end;
hence thesis;
end;
theorem Th3:
x in W1 /\ W2 iff x in W1 & x in W2
proof
x in W1 /\ W2 iff x in (the carrier of W1) /\ (the carrier of W2) by
Def2;
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;
end;
Lm1: W1 + W2 = W2 + W1
proof
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 object;
assume x in B;
then ex u,v st x = v + u & v in W2 & u in W1;
hence thesis;
end;
A2: the carrier of W1 + W2 = A by Def1;
A c= B
proof
let x be object;
assume x in A;
then ex u,v st x = v + u & v in W1 & u in W2;
hence thesis;
end;
then A = B by A1;
hence thesis by A2,Def1;
end;
Lm2: the carrier of W1 c= the carrier of W1 + W2
proof
let x be object;
set A = {v + u : v in W1 & u in W2};
assume x in the carrier of W1;
then reconsider v = x as Element of W1;
reconsider v as Vector of V by RMOD_2:10;
A1: v = v + 0.V by RLVECT_1:def 4;
v in W1 & 0.V in W2 by RMOD_2:17;
then x in A by A1;
hence thesis by Def1;
end;
Lm3: 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 object;
assume x in the carrier of W1 + W2;
then x in {v + u : v in W1 & u in W2} by Def1;
then consider u,v such that
A3: x = v + u and
A4: v in W1 and
A5: u in W2;
W1 is Submodule of W2 by A1,RMOD_2:27;
then v in W2 by A4,RMOD_2:8;
then v + u in W2 by A5,RMOD_2:20;
hence thesis by A3;
end;
W1 + W2 = W2 + W1 by Lm1;
then the carrier of W2 c= the carrier of W1 + W2 by Lm2;
then the carrier of W1 + W2 = the carrier of W2 by A2;
hence thesis by RMOD_2:29;
end;
theorem
for W being strict Submodule of V holds W + W = W by Lm3;
theorem
W1 + W2 = W2 + W1 by Lm1;
theorem Th6:
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 Def1;
A2: C c= D
proof
let x be object;
assume x in C;
then consider u,v 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;
then v in A by Def1;
then consider u2,u1 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 Def1;
then
A9: u2 + u in W2 + W3;
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 object;
assume x in D;
then consider u,v 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;
then u in B by Def1;
then consider u2,u1 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 Def1;
then
A16: v + u1 in W1 + W2;
v + u = (v + u1) + u2 by A13,RLVECT_1:def 3;
hence thesis by A10,A15,A16;
end;
then D = C by A2;
hence thesis by A1,Def1;
end;
theorem Th7:
W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2
proof
the carrier of W1 c= the carrier of W1 + W2 by Lm2;
hence W1 is Submodule of W1 + W2 by RMOD_2:27;
the carrier of W2 c= the carrier of W2 + W1 by Lm2;
then the carrier of W2 c= the carrier of W1 + W2 by Lm1;
hence thesis by RMOD_2:27;
end;
theorem Th8:
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 RMOD_2:def 2;
hence thesis by Lm3;
end;
thus thesis by Th7;
end;
theorem Th9:
for W being strict Submodule of V holds (0).V + W = W & W + (0). V = W
proof
let W be strict Submodule of V;
(0).V is Submodule of W by RMOD_2:39;
then the carrier of (0).V c= the carrier of W by RMOD_2:def 2;
hence (0).V + W = W by Lm3;
hence thesis by Lm1;
end;
Lm4: for W,W9,W1 being Submodule of V st the carrier of W = the carrier of W9
holds W1 + W = W1 + W9 & W + W1 = W9 + W1
proof
let W,W9,W1 be Submodule of V such that
A1: the carrier of W = the carrier of W9;
A2: now
let v;
set W1W9 = {v1 + v2 where v2,v1: v1 in W1 & v2 in W9};
set W1W = {v1 + v2 where v2,v1: v1 in W1 & v2 in W};
thus v in W1 + W implies v in W1 + W9
proof
assume v in W1 + W;
then v in the carrier of W1 + W;
then v in W1W by Def1;
then consider v2,v1 such that
A3: v = v1 + v2 & v1 in W1 and
A4: v2 in W;
v2 in the carrier of W9 by A1,A4;
then v2 in W9;
then v in W1W9 by A3;
then v in the carrier of W1 + W9 by Def1;
hence thesis;
end;
assume v in W1 + W9;
then v in the carrier of W1 + W9;
then v in W1W9 by Def1;
then consider v2,v1 such that
A5: v = v1 + v2 & v1 in W1 and
A6: v2 in W9;
v2 in the carrier of W by A1,A6;
then v2 in W;
then v in W1W by A5;
then v in the carrier of W1 + W by Def1;
hence v in W1 + W;
end;
hence W1 + W = W1 + W9 by RMOD_2:30;
W1 + W = W + W1 & W1 + W9 = W9 + W1 by Lm1;
hence thesis by A2,RMOD_2:30;
end;
Lm5: for W being Submodule of V holds W is Submodule of (Omega).V
proof
let W be Submodule of V;
thus the carrier of W c= the carrier of (Omega).V by RMOD_2:def 2;
thus 0.W = 0.V by RMOD_2:def 2
.= 0.(Omega).V;
thus thesis by RMOD_2:def 2;
end;
theorem
for V being strict RightMod of R holds (0).V + (Omega).V = V &
(Omega).V + (0).V = V by Th9;
theorem Th11:
for V being RightMod of R, W being Submodule of V holds (Omega).
V + W = the RightModStr of V & W + (Omega). V = the RightModStr of V
proof
let V be RightMod of R, W be Submodule of V;
consider W9 being strict Submodule of V such that
A1: the carrier of W9 = the carrier of (Omega).V;
A2: the carrier of W c= the carrier of W9 by A1,RMOD_2:def 2;
A3: W9 is Submodule of (Omega).V by Lm5;
W + (Omega).V = W + W9 by A1,Lm4
.= W9 by A2,Lm3
.= the RightModStr of V by A1,A3,RMOD_2:31;
hence thesis by Lm1;
end;
theorem
for V being strict RightMod of R holds (Omega).V + (Omega).V = V by Th11;
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 Def2;
end;
theorem Th14:
W1 /\ W2 = W2 /\ W1
proof
the carrier of W1 /\ W2 =(the carrier of W2) /\ (the carrier of W1) by Def2;
hence thesis by Def2;
end;
theorem Th15:
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 Def2
.= V1 /\ (V2 /\ V3) by Def2
.= (V1 /\ V2) /\ V3 by XBOOLE_1:16
.= (the carrier of W1 /\ W2) /\ V3 by Def2;
hence thesis by Def2;
end;
Lm6: 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 Def2;
hence thesis by XBOOLE_1:17;
end;
theorem Th16:
W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2
proof
the carrier of W1 /\ W2 c= the carrier of W1 by Lm6;
hence W1 /\ W2 is Submodule of W1 by RMOD_2:27;
the carrier of W2 /\ W1 c= the carrier of W2 by Lm6;
then the carrier of W1 /\ W2 c= the carrier of W2 by Th14;
hence thesis by RMOD_2:27;
end;
theorem Th17:
(for W1 being strict Submodule of V holds W1 is Submodule of W2
implies W1 /\ W2 = W1) & for W1 st W1 /\ W2 = W1 holds W1 is Submodule of W2
proof
thus for W1 being strict Submodule of V holds W1 is Submodule of W2 implies
W1 /\ W2 = W1
proof
let W1 be strict Submodule of V;
assume W1 is Submodule of W2;
then
A1: the carrier of W1 c= the carrier of W2 by RMOD_2:def 2;
the carrier of W1 /\ W2 = (the carrier of W1) /\ (the carrier of W2)
by Def2;
hence thesis by A1,RMOD_2:29,XBOOLE_1:28;
end;
thus thesis by Th16;
end;
theorem
W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3
proof
set A1 = the carrier of W1;
set A2 = the carrier of W2;
set A3 = the carrier of W3;
set A4 = the carrier of W1 /\ W3;
assume W1 is Submodule of W2;
then A1 c= A2 by RMOD_2:def 2;
then A1 /\ A3 c= A2 /\ A3 by XBOOLE_1:26;
then A4 c= A2 /\ A3 by Def2;
then A4 c= (the carrier of W2 /\ W3) by Def2;
hence thesis by RMOD_2:27;
end;
theorem
W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3
proof
assume
A1: W1 is Submodule of W3;
W1 /\ W2 is Submodule of W1 by Th16;
hence thesis by A1,RMOD_2:26;
end;
theorem
W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule
of W2 /\ W3
proof
assume
A1: W1 is Submodule of W2 & W1 is Submodule of W3;
now
let v;
assume v in W1;
then v in W2 & v in W3 by A1,RMOD_2:8;
hence v in W2 /\ W3 by Th3;
end;
hence thesis by RMOD_2:28;
end;
theorem Th21:
(0).V /\ W = (0).V & W /\ (0).V = (0).V
proof
0.V in W by RMOD_2:17;
then 0.V in the carrier of W;
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 Def2
.= {0.V} /\ (the carrier of W) by RMOD_2:def 3;
hence (0).V /\ W = (0).V by A1,RMOD_2:def 3;
hence thesis by Th14;
end;
theorem Th22:
for W being strict Submodule of V holds (Omega).V /\ W = W & W
/\ (Omega).V = 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 Def2,RMOD_2:def 2;
hence (Omega).V /\ W = W by RMOD_2:29,XBOOLE_1:28;
hence thesis by Th14;
end;
theorem
for V being strict RightMod of R holds (Omega).V /\ (Omega).V = V by Th22;
Lm7: 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 Lm2,Lm6;
hence thesis;
end;
theorem
W1 /\ W2 is Submodule of W1 + W2 by Lm7,RMOD_2:27;
Lm8: the carrier of (W1 /\ W2) + W2 = the carrier of W2
proof
thus the carrier of (W1 /\ W2) + W2 c= the carrier of W2
proof
let x be object;
assume x in the carrier of (W1 /\ W2) + W2;
then x in {u + v where v,u: u in W1 /\ W2 & v in W2} by Def1;
then consider v,u such that
A1: x = u + v and
A2: u in W1 /\ W2 and
A3: v in W2;
u in W2 by A2,Th3;
then u + v in W2 by A3,RMOD_2:20;
hence thesis by A1;
end;
let x be object;
the carrier of W2 c= the carrier of W2 + (W1 /\ W2) by Lm2;
then
A4: the carrier of W2 c= the carrier of (W1 /\ W2) + W2 by Lm1;
assume x in the carrier of W2;
hence thesis by A4;
end;
theorem
for W2 being strict Submodule of V holds (W1 /\ W2) + W2 = W2 by Lm8,
RMOD_2:29;
Lm9: the carrier of W1 /\ (W1 + W2) = the carrier of W1
proof
thus the carrier of W1 /\ (W1 + W2) c= the carrier of W1
proof
let x be object;
assume
A1: x in the carrier of W1 /\ (W1 + W2);
the carrier of W1 /\ (W1 + W2) = (the carrier of W1) /\ (the carrier
of W1 + W2) by Def2;
hence thesis by A1,XBOOLE_0:def 4;
end;
let x be object;
assume
A2: x in the carrier of W1;
the carrier of W1 c= the carrier of V by RMOD_2:def 2;
then reconsider x1 = x as Element of V by A2;
A3: x1 + 0.V = x1 & 0.V in W2 by RLVECT_1:def 4,RMOD_2:17;
x in W1 by A2;
then x in {u + v where v,u: u in W1 & v in W2} by A3;
then x in the carrier of W1 + W2 by Def1;
then x in (the carrier of W1) /\ (the carrier of W1 + W2) by A2,
XBOOLE_0:def 4;
hence thesis by Def2;
end;
theorem
for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1 by Lm9,
RMOD_2:29;
Lm10: the carrier of (W1 /\ W2) + (W2 /\ W3) c= the carrier of W2 /\ (W1 + W3)
proof
let x be object;
assume x in the carrier of (W1 /\ W2) + (W2 /\ W3);
then x in {u + v where v,u: u in W1 /\ W2 & v in W2 /\ W3} by Def1;
then consider v,u such that
A1: x = u + v and
A2: u in W1 /\ W2 & v in W2 /\ W3;
u in W2 & v in W2 by A2,Th3;
then
A3: x in W2 by A1,RMOD_2:20;
u in W1 & v in W3 by A2,Th3;
then x in W1 + W3 by A1,Th1;
then x in W2 /\ (W1 + W3) by A3,Th3;
hence thesis;
end;
theorem
(W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3) by Lm10,RMOD_2:27;
Lm11: 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 object;
assume x in the carrier of W2 /\ (W1 + W3);
then
A2: x in (the carrier of W2) /\ (the carrier of W1 + W3) by Def2;
then x in the carrier of W1 + W3 by XBOOLE_0:def 4;
then x in {u + v where v,u: u in W1 & v in W3} by Def1;
then consider v1,u1 such that
A3: x = u1 + v1 and
A4: u1 in W1 and
A5: v1 in W3;
A6: u1 in W2 by A1,A4,RMOD_2:8;
x in the carrier of W2 by A2,XBOOLE_0:def 4;
then u1 + v1 in W2 by A3;
then (v1 + u1) - u1 in W2 by A6,RMOD_2:23;
then v1 + (u1 - u1) in W2 by RLVECT_1:def 3;
then v1 + 0.V in W2 by VECTSP_1:19;
then v1 in W2 by RLVECT_1:def 4;
then
A7: v1 in W2 /\ W3 by A5,Th3;
u1 in W1 /\ W2 by A4,A6,Th3;
then x in (W1 /\ W2) + (W2 /\ W3) by A3,A7,Th1;
hence thesis;
end;
thus thesis by Lm10;
end;
theorem
W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3
) by Lm11,RMOD_2:29;
Lm12: the carrier of W2 + (W1 /\ W3) c= the carrier of (W1 + W2) /\ (W2 + W3)
proof
let x be object;
assume x in the carrier of W2 + (W1 /\ W3);
then x in {u + v where v,u: u in W2 & v in W1 /\ W3} by Def1;
then consider v,u such that
A1: x = u + v & u in W2 and
A2: v in W1 /\ W3;
v in W3 by A2,Th3;
then x in {u1 + u2 where u2,u1: u1 in W2 & u2 in W3} by A1;
then
A3: x in the carrier of W2 + W3 by Def1;
v in W1 by A2,Th3;
then x in {v1 + v2 where v2,v1: v1 in W1 & v2 in W2} by A1;
then x in the carrier of W1 + W2 by Def1;
then x in (the carrier of W1 + W2) /\ (the carrier of W2 + W3) by A3,
XBOOLE_0:def 4;
hence thesis by Def2;
end;
theorem
W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3) by Lm12,RMOD_2:27;
Lm13: 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 RMOD_2:def 2;
A1: V2 is linearly-closed by RMOD_2:33;
assume W1 is Submodule of W2;
then
A2: the carrier of W1 c= the carrier of W2 by RMOD_2:def 2;
thus the carrier of W2 + (W1 /\ W3) c= the carrier of (W1 + W2) /\ (W2 + W3)
by Lm12;
let x be object;
assume x in the carrier of (W1 + W2) /\ (W2 + W3);
then x in (the carrier of W1 + W2) /\ (the carrier of W2 + W3) by Def2;
then x in the carrier of W1 + W2 by XBOOLE_0:def 4;
then x in {u1 + u2 where u2,u1: u1 in W1 & u2 in W2} by Def1;
then consider u2,u1 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;
then u1 + u2 in V2 by A2,A1;
then
A5: u1 + u2 in W2;
0.V in W1 /\ W3 & (u1 + u2) + 0.V = u1 + u2 by RLVECT_1:def 4,RMOD_2:17;
then x in {u + v where v,u: u in W2 & v in W1 /\ W3} by A3,A5;
hence thesis by Def1;
end;
theorem
W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
by Lm13,RMOD_2:29;
theorem Th31:
for W1 being strict Submodule of V holds W1 is Submodule of W3
implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3
proof
let W1 be strict Submodule of V;
assume
A1: W1 is Submodule of W3;
thus (W1 + W2) /\ W3 = W3 /\ (W1 + W2) by Th14
.= (W1 /\ W3) + (W3 /\ W2) by A1,Lm11,RMOD_2:29
.= W1 + (W3 /\ W2) by A1,Th17
.= W1 + (W2 /\ W3) by Th14;
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 Th8;
hence thesis by Th17;
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 Lm1
.= ((W1 + W3) + W3) + W2 by Th6
.= (W1 + (W3 + W3)) + W2 by Th6
.= (W1 + W3) + W2 by Lm3
.= W1 + (W3 + W2) by Th6
.= W1 + (W2 + W3) by Lm1
.= (W1 + W2) + W3 by Th6
.= W2 + W3 by A1,Th8;
hence thesis by Th8;
end;
theorem
W1 is Submodule of W2 implies W1 is Submodule of W2 + W3
proof
assume
A1: W1 is Submodule of W2;
W2 is Submodule of W2 + W3 by Th7;
hence thesis by A1,RMOD_2:26;
end;
theorem
W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is
Submodule of W3
proof
assume
A1: W1 is Submodule of W3 & W2 is Submodule of W3;
now
let v;
assume v in W1 + W2;
then consider v1,v2 such that
A2: v1 in W1 & v2 in W2 and
A3: v = v1 + v2 by Th1;
v1 in W3 & v2 in W3 by A1,A2,RMOD_2:8;
hence v in W3 by A3,RMOD_2:20;
end;
hence thesis by RMOD_2:28;
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,RMOD_2:27;
then consider y being object such that
A4: y in VW2 and
A5: not y in VW1;
reconsider y as Element of VW2 by A4;
reconsider y as Vector of V by RMOD_2:10;
reconsider A1 = VW as Subset of V by RMOD_2:def 2;
A6: A1 is linearly-closed by RMOD_2:33;
not VW1 c= VW2 by A2,RMOD_2:27;
then consider x being object such that
A7: x in VW1 and
A8: not x in VW2;
reconsider x as Element of VW1 by A7;
reconsider x as Vector of V by RMOD_2:10;
A9: now
reconsider A2 = VW2 as Subset of V by RMOD_2:def 2;
A10: A2 is linearly-closed by RMOD_2:33;
assume x + y in VW2;
then (x + y) - y in VW2 by A10,RMOD_2:3;
then x + (y - y) in VW2 by RLVECT_1:def 3;
then x + 0.V in VW2 by VECTSP_1:19;
hence contradiction by A8,RLVECT_1:def 4;
end;
A11: now
reconsider A2 = VW1 as Subset of V by RMOD_2:def 2;
A12: A2 is linearly-closed by RMOD_2:33;
assume x + y in VW1;
then (y + x) - x in VW1 by A12,RMOD_2:3;
then y + (x - x) in VW1 by RLVECT_1:def 3;
then y + 0.V in VW1 by VECTSP_1:19;
hence contradiction by A5,RLVECT_1:def 4;
end;
x in VW & y in VW by A1,XBOOLE_0:def 3;
then x + y in VW by A6;
hence thesis by A1,A11,A9,XBOOLE_0:def 3;
end;
A13: now
assume W1 is Submodule of W2;
then VW1 c= VW2 by RMOD_2:def 2;
then VW1 \/ VW2 = VW2 by XBOOLE_1:12;
hence thesis;
end;
A14: now
assume W2 is Submodule of W1;
then VW2 c= VW1 by RMOD_2:def 2;
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 R;
let V;
func Submodules(V) -> set means
:Def3:
for x being object
holds x in it iff ex W being strict Submodule of V st W = x;
existence
proof
defpred Q[object,object] means
ex W being strict Submodule of V st $2 = W & $1 = the carrier of W;
defpred P[object] means
ex W being strict Submodule of V st $1 = the carrier of W;
consider B being set such that
A1: for x being object holds x in B iff x in bool the carrier of V & P[x] from
XBOOLE_0:sch 1;
A2: for x,y1,y2 being object st Q[x,y1] & Q[x,y2] holds y1 = y2 by RMOD_2:29;
consider f being Function such that
A3: for x,y being object holds [x,y] in f iff x in B & Q[x,y]
from FUNCT_1:sch 1(A2);
for x being object holds x in B iff ex y being object st [x,y] in f
proof
let x be object;
thus x in B implies ex y being object 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;
take W;
thus thesis by A3,A4,A5;
end;
thus thesis by A3;
end;
then
A6: B = dom f by XTUPLE_0:def 12;
for y being object
holds y in rng f iff ex W being strict Submodule of V st y = W
proof
let y be object;
thus y in rng f implies ex W being strict Submodule of V st y = W
proof
assume y in rng f;
then consider x being object such that
A7: x in dom f & y = f.x by FUNCT_1:def 3;
[x,y] in f by A7,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;
given W being strict Submodule of V such that
A8: y = W;
reconsider W = y as Submodule of V by A8;
reconsider x = the carrier of W as set;
A9: y is set by TARSKI:1;
the carrier of W c= the carrier of V by RMOD_2:def 2;
then
A10: x in dom f by A1,A6,A8;
then [x,y] in f by A3,A6,A8;
then y = f.x by A10,FUNCT_1:def 2,A9;
hence thesis by A10,FUNCT_1:def 3;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means ex W being strict Submodule of V st W = $1;
for X1,X2 being set st (for x being object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
hence thesis;
end;
end;
registration
let R;
let V;
cluster Submodules(V) -> non empty;
coherence
proof
set W = the strict Submodule of V;
W in Submodules(V) by Def3;
hence thesis;
end;
end;
theorem
for V being strict RightMod of R holds V in Submodules(V)
proof
let V be strict RightMod of R;
ex W9 being strict Submodule of V st the carrier of (Omega).V = the
carrier of W9;
hence thesis by Def3;
end;
definition
let R;
let V;
let W1,W2;
pred V is_the_direct_sum_of W1,W2 means
the RightModStr of V = W1 + W2 & W1 /\ W2 = (0).V;
end;
Lm14: for V being RightMod of R, W1,W2 being Submodule of V holds W1 + W2 =
the RightModStr 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 RightMod of R, W1,W2 be Submodule of V;
thus W1 + W2 = the RightModStr of V implies for v being Vector of V ex v1,v2
being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2
by RLVECT_1:1,Th1;
assume
A1: for v being Vector of V ex v1,v2 being Vector of V st v1 in W1 & v2
in W2 & v = v1 + v2;
now
thus W1 + W2 is Submodule of (Omega).V by Lm5;
let u be Vector of V;
ex v1,v2 being Vector of V st v1 in W1 & v2 in W2 & u = v1 + v2 by A1;
hence u in W1 + W2 by Th1;
end;
hence thesis by RMOD_2:32;
end;
Lm15: v = v1 + v2 iff v1 = v - v2
proof
thus v = v1 + v2 implies v1 = v - v2
proof
assume
A1: v = v1 + v2;
thus v1 = 0.V + v1 by RLVECT_1:def 4
.= v + (- (v2 + v1)) + v1 by A1,VECTSP_1:19
.= v + ((- v2) + (- v1)) + v1 by RLVECT_1:31
.= (v + (- v2)) + (- v1) + v1 by RLVECT_1:def 3
.= (v + (- v2)) + ((- v1) + v1) by RLVECT_1:def 3
.= v + (- v2) + 0.V by RLVECT_1:5
.= v - v2 by RLVECT_1:def 4;
end;
assume
A2: v1 = v - v2;
thus v = v + 0.V by RLVECT_1:def 4
.= v + (v1 + (- v1)) by RLVECT_1:5
.= (v + v1) + (- (v - v2)) by A2,RLVECT_1:def 3
.= (v + v1) + ((- v) + v2) by RLVECT_1:33
.= (v + v1) + (- v) + v2 by RLVECT_1:def 3
.= v + (- v) + v1 + v2 by RLVECT_1:def 3
.= 0.V + v1 + v2 by RLVECT_1:5
.= v1 + v2 by RLVECT_1:def 4;
end;
theorem Th38:
V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2, W1
by Th14,Lm1;
theorem
for V being strict RightMod of R holds V is_the_direct_sum_of (0).V,
(Omega).V & V is_the_direct_sum_of (Omega).V,(0).V
by Th9,Th21;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;
theorem Th40:
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 RMOD_2:74;
v in C1 by A1,XBOOLE_0:def 4;
then
A3: C1 = v + W1 by RMOD_2:74;
C is Coset of W1 /\ W2
proof
take v;
thus C c= v + W1 /\ W2
proof
let x be object;
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,RMOD_2:42;
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,RMOD_2:42;
u1 = u2 by A6,A8,RLVECT_1:8;
then u1 in W1 /\ W2 by A5,A7,Th3;
hence thesis by A6;
end;
let x be object;
assume x in v + (W1 /\ W2);
then consider u such that
A9: u in W1 /\ W2 and
A10: x = v + u by RMOD_2:42;
u in W2 by A9,Th3;
then
A11: x in C2 by A2,A10;
u in W1 by A9,Th3;
then x in C1 by A3,A10;
hence thesis by A11,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem Th41:
for V being RightMod of R, 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 RightMod of R, W1,W2 be Submodule of V;
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
A1: W1 + W2 is Submodule of (Omega).V by Lm5;
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 RightModStr of V = W1 + W2;
let C1 be Coset of W1, C2 be Coset of W2;
consider v1 being Vector of V such that
A4: C1 = v1 + W1 by RMOD_2:def 6;
v1 in (Omega).V;
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,Th1;
consider v2 being Vector of V such that
A8: C2 = v2 + W2 by RMOD_2:def 6;
v2 in (Omega).V;
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,Th1;
take v = v12 + v21;
{v} = C1 /\ C2
proof
thus
A12: {v} c= C1 /\ C2
proof
let x be object;
assume x in {v};
then
A13: x = v by TARSKI:def 1;
v21 = v2 - v22 by A11,Lm15;
then v21 in C2 by A8,A10,RMOD_2:59;
then C2 = v21 + W2 by RMOD_2:74;
then
A14: x in C2 by A6,A13;
v12 = v1 - v11 by A7,Lm15;
then v12 in C1 by A4,A5,RMOD_2:59;
then C1 = v12 + W1 by RMOD_2:74;
then x in C1 by A9,A13;
hence thesis by A14,XBOOLE_0:def 4;
end;
let x be object;
assume
A15: x in C1 /\ C2;
then C1 meets C2;
then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th40;
A16: v in {v} by TARSKI:def 1;
W1 /\ W2 = (0).V by A2;
then ex u being Vector of V st C = {u} by RMOD_2:69;
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 RMOD_2:70;
A19: the carrier of V c= the carrier of W1 + W2
proof
let x be object;
assume x in the carrier of V;
then reconsider u = x as Vector of V;
consider C1 being Coset of W1 such that
A20: u in C1 by RMOD_2:65;
consider v being Vector of V such that
A21: C1 /\ VW2 = {v} by A18,A17;
A22: v in {v} by TARSKI:def 1;
then v in C1 by A21,XBOOLE_0:def 4;
then consider v1 being Vector of V such that
A23: v1 in W1 and
A24: u - v1 = v by A20,RMOD_2:76;
v in VW2 by A21,A22,XBOOLE_0:def 4;
then
A25: v in W2;
u = v1 + v by A24,Lm15;
then x in W1 + W2 by A25,A23,Th1;
hence thesis;
end;
VW1 is Coset of W1 by RMOD_2:70;
then consider v being Vector of V such that
A26: VW1 /\ VW2 = {v} by A18,A17;
the carrier of W1 + W2 c= the carrier of V by RMOD_2:def 2;
then the carrier of V = the carrier of W1 + W2 by A19;
hence the RightModStr of V = W1 + W2 by A1,RMOD_2:31;
0.V in W2 by RMOD_2:17;
then
A27: 0.V in VW2;
0.V in W1 by RMOD_2:17;
then 0.V in VW1;
then
A28: 0.V in {v} by A26,A27,XBOOLE_0:def 4;
the carrier of (0).V = {0.V} by RMOD_2:def 3
.= VW1 /\ VW2 by A26,A28,TARSKI:def 1
.= the carrier of W1 /\ W2 by Def2;
hence thesis by RMOD_2:29;
end;
theorem
for V being strict RightMod of R, W1,W2 being Submodule of V holds W1
+ W2 = 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 Lm14;
theorem Th43:
for V being RightMod of R, W1,W2 being Submodule of V, v,v1,v2,
u1,u2 being Vector of V holds V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v =
u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies v1 = u1 & v2 = u2
proof
let V be RightMod of R, W1,W2 be Submodule of V, v,v1,v2,u1,u2 be Vector of
V;
reconsider C2 = v1 + W2 as Coset of W2 by RMOD_2:def 6;
reconsider C1 = the carrier of W1 as Coset of W1 by RMOD_2:70;
A1: v1 in C2 by RMOD_2:44;
assume V is_the_direct_sum_of W1,W2;
then consider u being Vector of V such that
A2: C1 /\ C2 = {u} by Th41;
assume that
A3: v = v1 + v2 & v = 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,RMOD_2:23;
v1 in C1 by A4;
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,Lm15
.= v1 + (v2 - u2) by RLVECT_1:def 3;
then
A9: u1 in C2 by A7;
u1 in C1 by A5;
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 v = v1 + v2 & v = 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 RMOD_2:39
,def 3;
then
A2: {0.V} c= the carrier of W1 /\ W2 by RMOD_2:def 2;
given v such that
A3: for v1,v2,u1,u2 st v = v1 + v2 & v = 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;
then the carrier of W1 /\ W2 <> {0.V} by RMOD_2:def 3;
then {0.V} c< the carrier of W1 /\ W2 by A2;
then consider x being object such that
A4: x in the carrier of W1 /\ W2 and
A5: not x in {0.V} by XBOOLE_0:6;
A6: x in W1 /\ W2 by A4;
then x in V by RMOD_2:9;
then reconsider u = x as Vector of V;
consider v1,v2 such that
A7: v1 in W1 and
A8: v2 in W2 and
A9: v = v1 + v2 by A1,Lm14;
A10: v = v1 + v2 + 0.V by A9,RLVECT_1:def 4
.= (v1 + v2) + (u - u) by VECTSP_1:19
.= ((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 A6,Th3;
then
A11: v2 - u in W2 by A8,RMOD_2:23;
x in W1 by A6,Th3;
then v1 + u in W1 by A7,RMOD_2:20;
then v2 + (- u) = v2 by A3,A7,A8,A9,A10,A11
.= v2 + 0.V by RLVECT_1:def 4;
then - u = 0.V by RLVECT_1:8;
then
A12: u = - 0.V by RLVECT_1:17;
x <> 0.V by A5,TARSKI:def 1;
hence thesis by A12,RLVECT_1:12;
end;
definition
let R;
let V be RightMod of R;
let v be Vector of V;
let W1,W2 be Submodule of V;
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
:Def5:
v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
existence
proof
W1 + W2 = the RightModStr of V by A1;
then consider v1,v2 being Vector of V such that
A2: v1 in W1 & v2 in W2 & v = v1 + v2 by Lm14;
take [v1,v2];
thus thesis by A2;
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,Th43;
t1 = [t1`1,t1`2] by MCART_1:21;
hence thesis by A3,MCART_1:21;
end;
end;
theorem
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 Def5;
A3: V is_the_direct_sum_of W2,W1 by A1,Th38;
then
A4: v = (v |-- (W2,W1))`2 + (v |-- (W2,W1))`1 & (v |-- (W2,W1))`1 in W2 by Def5
;
A5: (v |-- (W2,W1))`2 in W1 by A3,Def5;
v = (v |-- (W1,W2))`1 + (v |-- (W1,W2))`2 & (v |-- (W1,W2))`1 in W1 by A1
,Def5;
hence thesis by A1,A2,A4,A5,Th43;
end;
theorem
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 Def5;
A3: V is_the_direct_sum_of W2,W1 by A1,Th38;
then
A4: v = (v |-- (W2,W1))`2 + (v |-- (W2,W1))`1 & (v |-- (W2,W1))`1 in W2 by Def5
;
A5: (v |-- (W2,W1))`2 in W1 by A3,Def5;
v = (v |-- (W1,W2))`1 + (v |-- (W1,W2))`2 & (v |-- (W1,W2))`1 in W1 by A1
,Def5;
hence thesis by A1,A2,A4,A5,Th43;
end;
reserve A1,A2,B for Element of Submodules(V);
definition
let R;
let V;
func SubJoin(V) -> BinOp of Submodules(V) means
:Def6:
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;
consider W1 being strict Submodule of V such that
A2: W1 = A1 by Def3;
consider W2 being strict Submodule of V such that
A3: W2 = A2 by Def3;
reconsider C = W1 + W2 as Element of Submodules(V) by Def3;
take C;
thus thesis by A2,A3;
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
A4: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o1.(A1,A2) = W1 + W2;
assume
A5: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o2.(A1,A2) = W1 + W2;
now
let x,y be set;
assume that
A6: x in Submodules(V) and
A7: y in Submodules(V);
reconsider A = x, B = y as Element of Submodules(V) by A6,A7;
consider W1 being strict Submodule of V such that
A8: W1 = x by A6,Def3;
consider W2 being strict Submodule of V such that
A9: W2 = y by A7,Def3;
o1.(A,B) = W1 + W2 by A4,A8,A9;
hence o1.(x,y) = o2.(x,y) by A5,A8,A9;
end;
hence thesis by BINOP_1:1;
end;
end;
definition
let R;
let V;
func SubMeet(V) -> BinOp of Submodules(V) means
:Def7:
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;
consider W1 being strict Submodule of V such that
A2: W1 = A1 by Def3;
consider W2 being strict Submodule of V such that
A3: W2 = A2 by Def3;
reconsider C = W1 /\ W2 as Element of Submodules(V) by Def3;
take C;
thus thesis by A2,A3;
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
A4: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o1.(A1,A2) = W1 /\ W2;
assume
A5: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o2.(A1,A2) = W1 /\ W2;
now
let x,y be set;
assume that
A6: x in Submodules(V) and
A7: y in Submodules(V);
reconsider A = x, B = y as Element of Submodules(V) by A6,A7;
consider W1 being strict Submodule of V such that
A8: W1 = x by A6,Def3;
consider W2 being strict Submodule of V such that
A9: W2 = y by A7,Def3;
o1.(A,B) = W1 /\ W2 by A4,A8,A9;
hence o1.(x,y) = o2.(x,y) by A5,A8,A9;
end;
hence thesis by BINOP_1:1;
end;
end;
theorem Th47:
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;
consider W1 being strict Submodule of V such that
A2: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A3: W2 = B by Def3;
thus A "/\" B = SubMeet(V).(A,B) by LATTICES:def 2
.= W1 /\ W2 by A2,A3,Def7
.= W2 /\ W1 by Th14
.= SubMeet(V).(B,A) by A2,A3,Def7
.= B "/\" A by LATTICES:def 2;
end;
A4: for A,B being Element of S holds (A "/\" B) "\/" B = B
proof
let A,B be Element of S;
consider W1 being strict Submodule of V such that
A5: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A6: W2 = B by Def3;
reconsider AB = W1 /\ W2 as Element of S by Def3;
thus (A "/\" B) "\/" B = SubJoin(V).(A "/\" B,B) by LATTICES:def 1
.= SubJoin(V).(SubMeet(V).(A,B),B) by LATTICES:def 2
.= SubJoin(V).(AB,B) by A5,A6,Def7
.= (W1 /\ W2) + W2 by A6,Def6
.= B by A6,Lm8,RMOD_2:29;
end;
A7: for A,B,C being Element of S holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A,B,C be Element of S;
consider W1 being strict Submodule of V such that
A8: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A9: W2 = B by Def3;
consider W3 being strict Submodule of V such that
A10: W3 = C by Def3;
reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of S by Def3;
thus A "/\" (B "/\" C) = SubMeet(V).(A,B "/\" C) by LATTICES:def 2
.= SubMeet(V).(A,SubMeet(V).(B,C)) by LATTICES:def 2
.= SubMeet(V).(A,BC) by A9,A10,Def7
.= W1 /\ (W2 /\ W3) by A8,Def7
.= (W1 /\ W2) /\ W3 by Th15
.= SubMeet(V).(AB,C) by A10,Def7
.= SubMeet(V).(SubMeet(V).(A,B),C) by A8,A9,Def7
.= SubMeet(V).(A "/\" B,C) by LATTICES:def 2
.= (A "/\" B) "/\" C by LATTICES:def 2;
end;
A11: for A,B,C being Element of S holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A,B,C be Element of S;
consider W1 being strict Submodule of V such that
A12: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A13: W2 = B by Def3;
consider W3 being strict Submodule of V such that
A14: W3 = C by Def3;
reconsider AB = W1 + W2, BC = W2 + W3 as Element of S by Def3;
thus A "\/" (B "\/" C) = SubJoin(V).(A,B "\/" C) by LATTICES:def 1
.= SubJoin(V).(A,SubJoin(V).(B,C)) by LATTICES:def 1
.= SubJoin(V).(A,BC) by A13,A14,Def6
.= W1 + (W2 + W3) by A12,Def6
.= (W1 + W2) + W3 by Th6
.= SubJoin(V).(AB,C) by A14,Def6
.= SubJoin(V).(SubJoin(V).(A,B),C) by A12,A13,Def6
.= SubJoin(V).(A "\/" B,C) by LATTICES:def 1
.= (A "\/" B) "\/" C by LATTICES:def 1;
end;
A15: for A,B being Element of S holds A "/\" (A "\/" B) = A
proof
let A,B be Element of S;
consider W1 being strict Submodule of V such that
A16: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A17: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of S by Def3;
thus A "/\" (A "\/" B) = SubMeet(V).(A,A "\/" B) by LATTICES:def 2
.= SubMeet(V).(A,SubJoin(V).(A,B)) by LATTICES:def 1
.= SubMeet(V).(A,AB) by A16,A17,Def6
.= W1 /\ (W1 + W2) by A16,Def7
.= A by A16,Lm9,RMOD_2:29;
end;
for A,B being Element of S holds A "\/" B = B "\/" A
proof
let A,B be Element of S;
consider W1 being strict Submodule of V such that
A18: W1 = A by Def3;
consider W2 being strict Submodule of V such that
A19: W2 = B by Def3;
thus A "\/" B = SubJoin(V).(A,B) by LATTICES:def 1
.= W1 + W2 by A18,A19,Def6
.= W2 + W1 by Lm1
.= SubJoin(V).(B,A) by A18,A19,Def6
.= B "\/" A by LATTICES:def 1;
end;
then S is join-commutative join-associative meet-absorbing meet-commutative
meet-associative join-absorbing by A11,A4,A1,A7,A15,LATTICES:def 4,def 5
,def 6,def 7,def 8,def 9;
hence thesis;
end;
theorem Th48:
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 0_Lattice
proof
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 Def3;
take C;
let A be Element of S;
consider W being strict Submodule of V such that
A1: W = A by Def3;
thus C "/\" A = SubMeet(V).(C,A) by LATTICES:def 2
.= (0).V /\ W by A1,Def7
.= C by Th21;
thus A "/\" C = SubMeet(V).(A,C) by LATTICES:def 2
.= W /\ (0).V by A1,Def7
.= C by Th21;
end;
hence thesis by Th47,LATTICES:def 13;
end;
theorem Th49:
for V being RightMod of R holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is 1_Lattice
proof
let V be RightMod of R;
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
consider W9 being strict Submodule of V such that
A1: the carrier of W9 = the carrier of (Omega).V;
reconsider C = W9 as Element of S by Def3;
take C;
let A be Element of S;
consider W being strict Submodule of V such that
A2: W = A by Def3;
A3: C is Submodule of (Omega).V by Lm5;
thus C "\/" A = SubJoin(V).(C,A) by LATTICES:def 1
.= W9 + W by A2,Def6
.= (Omega).V + W by A1,Lm4
.= the RightModStr of V by Th11
.= C by A1,A3,RMOD_2:31;
thus A "\/" C = SubJoin(V).(A,C) by LATTICES:def 1
.= W + W9 by A2,Def6
.= W + (Omega).V by A1,Lm4
.= the RightModStr of V by Th11
.= C by A1,A3,RMOD_2:31;
end;
hence thesis by Th47,LATTICES:def 14;
end;
theorem
for V being RightMod of R holds LattStr (# Submodules(V), SubJoin(V),
SubMeet(V) #) is 01_Lattice
proof
let V be RightMod of R;
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is lower-bounded
upper-bounded Lattice by Th48,Th49;
hence thesis;
end;
theorem
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is M_Lattice
proof
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;
assume
A1: A [= C;
consider W1 being strict Submodule of V such that
A2: W1 = A by Def3;
consider W3 being strict Submodule of V such that
A3: W3 = C by Def3;
W1 + W3 = SubJoin(V).(A,C) by A2,A3,Def6
.= A "\/" C by LATTICES:def 1
.= W3 by A1,A3,LATTICES:def 3;
then
A4: W1 is Submodule of W3 by Th8;
consider W2 being strict Submodule of V such that
A5: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of S by Def3;
reconsider BC = W2 /\ W3 as Element of S by Def3;
thus A "\/" (B "/\" C) = SubJoin(V).(A,B "/\" C) by LATTICES:def 1
.= SubJoin(V).(A,SubMeet(V).(B,C)) by LATTICES:def 2
.= SubJoin(V).(A,BC) by A5,A3,Def7
.= W1 + (W2 /\ W3) by A2,Def6
.= (W1 + W2) /\ W3 by A4,Th31
.= SubMeet(V).(AB,C) by A3,Def7
.= SubMeet(V).(SubJoin(V).(A,B),C) by A2,A5,Def6
.= SubMeet(V).(A "\/" B,C) by LATTICES:def 1
.= (A "\/" B) "/\" C by LATTICES:def 2;
end;
hence thesis by Th47,LATTICES:def 12;
end;