rmod_3.miz
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;
::
RMOD_3:def1
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 be
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 be
Element of V : v
in V1 & u
in V2 }
proof
thus VS
c= { (v
+ u) where u,v be
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 be
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,
RMOD_2: 34;
end;
uniqueness by
RMOD_2: 29;
end
definition
let R;
let V;
let W1, W2;
::
RMOD_3:def2
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 ::
RMOD_3:1
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 ::
RMOD_3:2
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 ::
RMOD_3:3
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 be
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 ::
RMOD_3:4
for W be
strict
Submodule of V holds (W
+ W)
= W by
Lm3;
theorem ::
RMOD_3:5
(W1
+ W2)
= (W2
+ W1) by
Lm1;
theorem ::
RMOD_3:6
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 ::
RMOD_3:7
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 ::
RMOD_3:8
Th8: for W2 be
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 ::
RMOD_3:9
Th9: for W be
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 be
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 be
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 ::
RMOD_3:10
for V be
strict
RightMod of R holds ((
(0). V)
+ (
(Omega). V))
= V & ((
(Omega). V)
+ (
(0). V))
= V by
Th9;
theorem ::
RMOD_3:11
Th11: for V be
RightMod of R, W be
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 be
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 ::
RMOD_3:12
for V be
strict
RightMod of R holds ((
(Omega). V)
+ (
(Omega). V))
= V by
Th11;
theorem ::
RMOD_3:13
for W be
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 ::
RMOD_3:14
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 ::
RMOD_3:15
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 ::
RMOD_3:16
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 ::
RMOD_3:17
Th17: (for W1 be
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 be
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 ::
RMOD_3:18
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 ::
RMOD_3:19
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 ::
RMOD_3:20
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 ::
RMOD_3:21
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 ::
RMOD_3:22
Th22: for W be
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 ::
RMOD_3:23
for V be
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 ::
RMOD_3:24
(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 ::
RMOD_3:25
for W2 be
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 ::
RMOD_3:26
for W1 be
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 ::
RMOD_3:27
((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 ::
RMOD_3:28
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 ::
RMOD_3:29
(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 ::
RMOD_3:30
W1 is
Submodule of W2 implies (W2
+ (W1
/\ W3))
= ((W1
+ W2)
/\ (W2
+ W3)) by
Lm13,
RMOD_2: 29;
theorem ::
RMOD_3:31
Th31: for W1 be
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 ::
RMOD_3:32
for W1,W2 be
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 ::
RMOD_3:33
for W2,W3 be
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 ::
RMOD_3:34
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 ::
RMOD_3:35
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 ::
RMOD_3:36
(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 be
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 be
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;
::
RMOD_3:def3
func
Submodules (V) ->
set means
:
Def3: for x be
object holds x
in it iff ex W be
strict
Submodule of V st W
= x;
existence
proof
defpred
Q[
object,
object] means ex W be
strict
Submodule of V st $2
= W & $1
= the
carrier of W;
defpred
P[
object] means ex W be
strict
Submodule of V st $1
= the
carrier of W;
consider B be
set such that
A1: for x be
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 be
object st
Q[x, y1] &
Q[x, y2] holds y1
= y2 by
RMOD_2: 29;
consider f be
Function such that
A3: for x,y be
object holds
[x, y]
in f iff x
in B &
Q[x, y] from
FUNCT_1:sch 1(
A2);
for x be
object holds x
in B iff ex y be
object st
[x, y]
in f
proof
let x be
object;
thus x
in B implies ex y be
object st
[x, y]
in f
proof
assume
A4: x
in B;
then
consider W be
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 be
object holds y
in (
rng f) iff ex W be
strict
Submodule of V st y
= W
proof
let y be
object;
thus y
in (
rng f) implies ex W be
strict
Submodule of V st y
= W
proof
assume y
in (
rng f);
then
consider x be
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 be
strict
Submodule of V st y
= W & x
= the
carrier of W by
A3;
hence thesis;
end;
given W be
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 be
strict
Submodule of V st W
= $1;
for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
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 ::
RMOD_3:37
for V be
strict
RightMod of R holds V
in (
Submodules V)
proof
let V be
strict
RightMod of R;
ex W9 be
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;
::
RMOD_3:def4
pred V
is_the_direct_sum_of W1,W2 means the RightModStr of V
= (W1
+ W2) & (W1
/\ W2)
= (
(0). V);
end
Lm14: for V be
RightMod of R, W1,W2 be
Submodule of V holds (W1
+ W2)
= the RightModStr of V iff for v be
Vector of V holds ex v1,v2 be
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 be
Vector of V holds ex v1,v2 be
Vector of V st v1
in W1 & v2
in W2 & v
= (v1
+ v2) by
RLVECT_1: 1,
Th1;
assume
A1: for v be
Vector of V holds ex v1,v2 be
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 be
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 ::
RMOD_3:38
Th38: V
is_the_direct_sum_of (W1,W2) implies V
is_the_direct_sum_of (W2,W1) by
Th14,
Lm1;
theorem ::
RMOD_3:39
for V be
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 ::
RMOD_3:40
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 ::
RMOD_3:41
Th41: for V be
RightMod of R, W1,W2 be
Submodule of V holds V
is_the_direct_sum_of (W1,W2) iff for C1 be
Coset of W1, C2 be
Coset of W2 holds ex v be
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 be
Coset of W1, C2 be
Coset of W2 holds ex v be
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 be
Vector of V such that
A4: C1
= (v1
+ W1) by
RMOD_2:def 6;
v1
in (
(Omega). V);
then
consider v11,v12 be
Vector of V such that
A5: v11
in W1 and
A6: v12
in W2 and
A7: v1
= (v11
+ v12) by
A3,
Th1;
consider v2 be
Vector of V such that
A8: C2
= (v2
+ W2) by
RMOD_2:def 6;
v2
in (
(Omega). V);
then
consider v21,v22 be
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 be
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 be
Coset of W1, C2 be
Coset of W2 holds ex v be
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 be
Coset of W1 such that
A20: u
in C1 by
RMOD_2: 65;
consider v be
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 be
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 be
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 ::
RMOD_3:42
for V be
strict
RightMod of R, W1,W2 be
Submodule of V holds (W1
+ W2)
= V iff for v be
Vector of V holds ex v1,v2 be
Vector of V st v1
in W1 & v2
in W2 & v
= (v1
+ v2) by
Lm14;
theorem ::
RMOD_3:43
Th43: for V be
RightMod of R, W1,W2 be
Submodule of V, v,v1,v2,u1,u2 be
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 be
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 ::
RMOD_3:44
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,
RMOD_2: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 be
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);
::
RMOD_3:def5
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 be
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 ::
RMOD_3:45
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 ::
RMOD_3:46
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;
::
RMOD_3:def6
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 holds ex B st
P[A1, A2, B]
proof
let A1, A2;
consider W1 be
strict
Submodule of V such that
A2: W1
= A1 by
Def3;
consider W2 be
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 be
BinOp of (
Submodules V) st for a,b be
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 be
strict
Submodule of V such that
A8: W1
= x by
A6,
Def3;
consider W2 be
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;
::
RMOD_3:def7
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 holds ex B st
P[A1, A2, B]
proof
let A1, A2;
consider W1 be
strict
Submodule of V such that
A2: W1
= A1 by
Def3;
consider W2 be
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 be
BinOp of (
Submodules V) st for a,b be
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 be
strict
Submodule of V such that
A8: W1
= x by
A6,
Def3;
consider W2 be
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 ::
RMOD_3:47
Th47:
LattStr (# (
Submodules V), (
SubJoin V), (
SubMeet V) #) is
Lattice
proof
set S =
LattStr (# (
Submodules V), (
SubJoin V), (
SubMeet V) #);
A1: for A,B be
Element of S holds (A
"/\" B)
= (B
"/\" A)
proof
let A,B be
Element of S;
consider W1 be
strict
Submodule of V such that
A2: W1
= A by
Def3;
consider W2 be
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 be
Element of S holds ((A
"/\" B)
"\/" B)
= B
proof
let A,B be
Element of S;
consider W1 be
strict
Submodule of V such that
A5: W1
= A by
Def3;
consider W2 be
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 be
Element of S holds (A
"/\" (B
"/\" C))
= ((A
"/\" B)
"/\" C)
proof
let A,B,C be
Element of S;
consider W1 be
strict
Submodule of V such that
A8: W1
= A by
Def3;
consider W2 be
strict
Submodule of V such that
A9: W2
= B by
Def3;
consider W3 be
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 be
Element of S holds (A
"\/" (B
"\/" C))
= ((A
"\/" B)
"\/" C)
proof
let A,B,C be
Element of S;
consider W1 be
strict
Submodule of V such that
A12: W1
= A by
Def3;
consider W2 be
strict
Submodule of V such that
A13: W2
= B by
Def3;
consider W3 be
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 be
Element of S holds (A
"/\" (A
"\/" B))
= A
proof
let A,B be
Element of S;
consider W1 be
strict
Submodule of V such that
A16: W1
= A by
Def3;
consider W2 be
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 be
Element of S holds (A
"\/" B)
= (B
"\/" A)
proof
let A,B be
Element of S;
consider W1 be
strict
Submodule of V such that
A18: W1
= A by
Def3;
consider W2 be
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,
LATTICES:def 5,
LATTICES:def 6,
LATTICES:def 7,
LATTICES:def 8,
LATTICES:def 9;
hence thesis;
end;
theorem ::
RMOD_3:48
Th48:
LattStr (# (
Submodules V), (
SubJoin V), (
SubMeet V) #) is
0_Lattice
proof
set S =
LattStr (# (
Submodules V), (
SubJoin V), (
SubMeet V) #);
ex C be
Element of S st for A be
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 be
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 ::
RMOD_3:49
Th49: for V be
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 be
Element of S st for A be
Element of S holds (C
"\/" A)
= C & (A
"\/" C)
= C
proof
consider W9 be
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 be
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 ::
RMOD_3:50
for V be
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 ::
RMOD_3:51
LattStr (# (
Submodules V), (
SubJoin V), (
SubMeet V) #) is
M_Lattice
proof
set S =
LattStr (# (
Submodules V), (
SubJoin V), (
SubMeet V) #);
for A,B,C be
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 be
strict
Submodule of V such that
A2: W1
= A by
Def3;
consider W3 be
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 be
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;