rmod_2.miz
begin
reserve x,y,y1,y2 for
object;
reserve R for
Ring;
reserve a for
Scalar of R;
reserve V,X,Y for
RightMod of R;
reserve u,u1,u2,v,v1,v2 for
Vector of V;
reserve V1,V2,V3 for
Subset of V;
definition
let R, V, V1;
::
RMOD_2:def1
attr V1 is
linearly-closed means (for v, u st v
in V1 & u
in V1 holds (v
+ u)
in V1) & for a, v st v
in V1 holds (v
* a)
in V1;
end
theorem ::
RMOD_2:1
Th1: 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;
(x
* (
0. R))
in V1 by
A1,
A2;
hence thesis by
VECTSP_2: 32;
end;
theorem ::
RMOD_2:2
Th2: 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 (v
* (
- (
1_ R)))
in V1 by
A1;
hence thesis by
VECTSP_2: 32;
end;
theorem ::
RMOD_2:3
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,
Th2;
hence thesis by
A1,
A2;
end;
theorem ::
RMOD_2:4
Th4:
{(
0. V)} is
linearly-closed
proof
thus for v, u st v
in
{(
0. V)} & u
in
{(
0. V)} holds (v
+ u)
in
{(
0. V)}
proof
let v, u;
assume v
in
{(
0. V)} & u
in
{(
0. V)};
then v
= (
0. V) & u
= (
0. V) by
TARSKI:def 1;
then (v
+ u)
= (
0. V) by
RLVECT_1:def 4;
hence thesis by
TARSKI:def 1;
end;
let a, v;
assume
A1: v
in
{(
0. V)};
then v
= (
0. V) by
TARSKI:def 1;
hence thesis by
A1,
VECTSP_2: 32;
end;
theorem ::
RMOD_2:5
the
carrier of V
= V1 implies V1 is
linearly-closed;
theorem ::
RMOD_2:6
V1 is
linearly-closed & V2 is
linearly-closed & V3
= { (v
+ u) : v
in V1 & u
in V2 } implies V3 is
linearly-closed
proof
assume that
A1: V1 is
linearly-closed & V2 is
linearly-closed and
A2: V3
= { (v
+ u) : v
in V1 & u
in V2 };
thus for v, u st v
in V3 & u
in V3 holds (v
+ u)
in V3
proof
let v, u;
assume that
A3: v
in V3 and
A4: u
in V3;
consider v2, v1 such that
A5: v
= (v1
+ v2) and
A6: v1
in V1 & v2
in V2 by
A2,
A3;
consider u2, u1 such that
A7: u
= (u1
+ u2) and
A8: u1
in V1 & u2
in V2 by
A2,
A4;
A9: (v
+ u)
= (((v1
+ v2)
+ u1)
+ u2) by
A5,
A7,
RLVECT_1:def 3
.= (((v1
+ u1)
+ v2)
+ u2) by
RLVECT_1:def 3
.= ((v1
+ u1)
+ (v2
+ u2)) by
RLVECT_1:def 3;
(v1
+ u1)
in V1 & (v2
+ u2)
in V2 by
A1,
A6,
A8;
hence thesis by
A2,
A9;
end;
let a, v;
assume v
in V3;
then
consider v2, v1 such that
A10: v
= (v1
+ v2) and
A11: v1
in V1 & v2
in V2 by
A2;
A12: (v
* a)
= ((v1
* a)
+ (v2
* a)) by
A10,
VECTSP_2:def 9;
(v1
* a)
in V1 & (v2
* a)
in V2 by
A1,
A11;
hence thesis by
A2,
A12;
end;
theorem ::
RMOD_2:7
V1 is
linearly-closed & V2 is
linearly-closed implies (V1
/\ V2) is
linearly-closed
proof
assume that
A1: V1 is
linearly-closed and
A2: V2 is
linearly-closed;
thus for v, u st v
in (V1
/\ V2) & u
in (V1
/\ V2) holds (v
+ u)
in (V1
/\ V2)
proof
let v, u;
assume
A3: v
in (V1
/\ V2) & u
in (V1
/\ V2);
then v
in V2 & u
in V2 by
XBOOLE_0:def 4;
then
A4: (v
+ u)
in V2 by
A2;
v
in V1 & u
in V1 by
A3,
XBOOLE_0:def 4;
then (v
+ u)
in V1 by
A1;
hence thesis by
A4,
XBOOLE_0:def 4;
end;
let a, v;
assume
A5: v
in (V1
/\ V2);
then v
in V2 by
XBOOLE_0:def 4;
then
A6: (v
* a)
in V2 by
A2;
v
in V1 by
A5,
XBOOLE_0:def 4;
then (v
* a)
in V1 by
A1;
hence thesis by
A6,
XBOOLE_0:def 4;
end;
definition
let R;
let V;
::
RMOD_2:def2
mode
Submodule of V ->
RightMod of R means
:
Def2: 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
carrier of it :] qua
set) & the
rmult of it
= (the
rmult of V
|
[:the
carrier of it , the
carrier of R:] qua
set);
existence
proof
take V;
thus the
carrier of V
c= the
carrier of V & (
0. V)
= (
0. V);
thus thesis by
RELSET_1: 19;
end;
end
reserve W,W1,W2 for
Submodule of V;
reserve w,w1,w2 for
Vector of W;
theorem ::
RMOD_2:8
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
Def2;
hence thesis;
end;
theorem ::
RMOD_2:9
Th9: x
in W implies x
in V
proof
assume x
in W;
then
A1: x
in the
carrier of W;
the
carrier of W
c= the
carrier of V by
Def2;
hence thesis by
A1;
end;
theorem ::
RMOD_2:10
Th10: w is
Vector of V
proof
w
in V by
Th9,
RLVECT_1: 1;
hence thesis;
end;
theorem ::
RMOD_2:11
(
0. W)
= (
0. V) by
Def2;
theorem ::
RMOD_2:12
(
0. W1)
= (
0. W2)
proof
thus (
0. W1)
= (
0. V) by
Def2
.= (
0. W2) by
Def2;
end;
theorem ::
RMOD_2:13
Th13: w1
= v & w2
= u implies (w1
+ w2)
= (v
+ u)
proof
assume
A1: v
= w1 & u
= w2;
set IW =
[:the
carrier of W, the
carrier of W:];
(w1
+ w2)
= ((the
addF of V
| IW qua
set)
.
[w1, w2]) by
Def2;
hence thesis by
A1,
FUNCT_1: 49;
end;
theorem ::
RMOD_2:14
Th14: w
= v implies (w
* a)
= (v
* a)
proof
assume
A1: w
= v;
(w
* a)
= ((the
rmult of V
|
[:the
carrier of W, the
carrier of R:] qua
set)
.
[w, a]) by
Def2;
hence thesis by
A1,
FUNCT_1: 49;
end;
theorem ::
RMOD_2:15
Th15: w
= v implies (
- v)
= (
- w)
proof
A1: (
- v)
= (v
* (
- (
1_ R))) & (
- w)
= (w
* (
- (
1_ R))) by
VECTSP_2: 32;
assume w
= v;
hence thesis by
A1,
Th14;
end;
theorem ::
RMOD_2:16
Th16: w1
= v & w2
= u implies (w1
- w2)
= (v
- u)
proof
assume that
A1: w1
= v and
A2: w2
= u;
(
- w2)
= (
- u) by
A2,
Th15;
hence thesis by
A1,
Th13;
end;
Lm1: the
carrier of W
= V1 implies V1 is
linearly-closed
proof
set VW = the
carrier of W;
reconsider WW = W as
RightMod of R;
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
Th13;
end;
let a, v;
assume v
in V1;
then
reconsider vv = v as
Vector of WW by
A1;
reconsider vw = (vv
* a) as
Element of VW;
vw
in V1 by
A1;
hence thesis by
Th14;
end;
theorem ::
RMOD_2:17
Th17: (
0. V)
in W
proof
(
0. W)
in W;
hence thesis by
Def2;
end;
theorem ::
RMOD_2:18
(
0. W1)
in W2
proof
(
0. W1)
= (
0. V) by
Def2;
hence thesis by
Th17;
end;
theorem ::
RMOD_2:19
(
0. W)
in V by
Th9,
RLVECT_1: 1;
theorem ::
RMOD_2:20
Th20: u
in W & v
in W implies (u
+ v)
in W
proof
reconsider VW = the
carrier of W as
Subset of V by
Def2;
assume u
in W & v
in W;
then
A1: u
in the
carrier of W & v
in the
carrier of W;
VW is
linearly-closed by
Lm1;
then (u
+ v)
in the
carrier of W by
A1;
hence thesis;
end;
theorem ::
RMOD_2:21
Th21: v
in W implies (v
* a)
in W
proof
reconsider VW = the
carrier of W as
Subset of V by
Def2;
assume v
in W;
then
A1: v
in the
carrier of W;
VW is
linearly-closed by
Lm1;
then (v
* a)
in the
carrier of W by
A1;
hence thesis;
end;
theorem ::
RMOD_2:22
Th22: v
in W implies (
- v)
in W
proof
assume v
in W;
then (v
* (
- (
1_ R)))
in W by
Th21;
hence thesis by
VECTSP_2: 32;
end;
theorem ::
RMOD_2:23
Th23: 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,
Th22;
hence thesis by
A1,
Th20;
end;
theorem ::
RMOD_2:24
Th24: V is
Submodule of V
proof
A1: the
rmult of V
= (the
rmult of V
|
[:the
carrier of V, the
carrier of R:] qua
set) by
RELSET_1: 19;
(
0. V)
= (
0. V) & the
addF of V
= (the
addF of V
|
[:the
carrier of V, the
carrier of V:] qua
set) by
RELSET_1: 19;
hence thesis by
A1,
Def2;
end;
theorem ::
RMOD_2:25
Th25: for X,V be
strict
RightMod of R holds V is
Submodule of X & X is
Submodule of V implies V
= X
proof
let X,V be
strict
RightMod of R;
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,
Def2;
then
A3: VV
= VX;
set AX = the
addF of X;
set AV = the
addF of V;
AV
= (AX
|| VV) & AX
= (AV
|| VX) by
A1,
A2,
Def2;
then
A4: AV
= AX by
A3;
set MX = the
rmult of X;
set MV = the
rmult of V;
A5: MX
= (MV
|
[:VX, the
carrier of R:] qua
set) by
A2,
Def2;
(
0. V)
= (
0. X) & MV
= (MX
|
[:VV, the
carrier of R:] qua
set) by
A1,
Def2;
hence thesis by
A3,
A4,
A5;
end;
registration
let R, V;
cluster
strict for
Submodule of V;
existence
proof
set M = the
rmult of V;
set W =
RightModStr (# the
carrier of V, the
addF of V, (
0. V), M #);
A1: W is
RightMod-like
proof
let a,b be
Scalar of R;
let v,w be
Vector of W;
reconsider x = v, y = w as
Vector of V;
thus ((v
+ w)
* a)
= ((x
+ y)
* a)
.= ((x
* a)
+ (y
* a)) by
VECTSP_2:def 9
.= ((v
* a)
+ (w
* a));
thus (v
* (a
+ b))
= (x
* (a
+ b))
.= ((x
* a)
+ (x
* b)) by
VECTSP_2:def 9
.= ((v
* a)
+ (v
* b));
thus (v
* (b
* a))
= (x
* (b
* a))
.= ((x
* b)
* a) by
VECTSP_2:def 9
.= ((v
* b)
* a);
thus (v
* (
1_ R))
= (x
* (
1_ R))
.= v by
VECTSP_2:def 9;
end;
A2: for a,b be
Element of W holds for x,y be
Vector of V st x
= a & b
= y holds (a
+ b)
= (x
+ y);
W is
Abelian
add-associative
right_zeroed
right_complementable
proof
thus W is
Abelian
proof
let a,b be
Element of W;
reconsider x = a, y = b as
Vector of V;
thus (a
+ b)
= (y
+ x) by
A2
.= (b
+ a);
end;
hereby
let a,b,c be
Element of W;
reconsider x = a, y = b, z = c as
Vector of V;
thus ((a
+ b)
+ c)
= ((x
+ y)
+ z)
.= (x
+ (y
+ z)) by
RLVECT_1:def 3
.= (a
+ (b
+ c));
end;
hereby
let a be
Element of W;
reconsider x = a as
Vector of V;
thus (a
+ (
0. W))
= (x
+ (
0. V))
.= a by
RLVECT_1:def 4;
end;
let a be
Element of W;
reconsider x = a as
Vector of V;
reconsider b = ((
comp V)
. x) as
Element of W;
take b;
thus (a
+ b)
= (x
+ (
- x)) by
VECTSP_1:def 13
.= (
0. W) by
RLVECT_1: 5;
end;
then
reconsider W as
RightMod of R by
A1;
A3: (
0. W)
= (
0. V) & the
addF of W
= (the
addF of V
|| the
carrier of W) by
RELSET_1: 19;
the
rmult of W
= (the
rmult of V
|
[:the
carrier of W, the
carrier of R:] qua
set) by
RELSET_1: 19;
then
reconsider W as
Submodule of V by
A3,
Def2;
take W;
thus thesis;
end;
end
theorem ::
RMOD_2:26
Th26: 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,
Def2;
then
A3: the
carrier of V
c= the
carrier of Y;
A4: the
addF of V
= (the
addF of Y
|
[:the
carrier of V, the
carrier of V:] qua
set)
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,
Def2;
then
A5:
[:VV, VV:]
c=
[:VX, VX:] by
ZFMISC_1: 96;
AV
= (AX
|| VV) by
A1,
Def2;
then AV
= ((AY
|| VX)
|| VV) by
A2,
Def2;
hence thesis by
A5,
FUNCT_1: 51;
end;
set MY = the
rmult of Y;
set MX = the
rmult of X;
set MV = the
rmult of V;
set VX = the
carrier of X;
set VV = the
carrier of V;
VV
c= VX by
A1,
Def2;
then
A6:
[:VV, the
carrier of R:]
c=
[:the
carrier of X, the
carrier of R:] by
ZFMISC_1: 95;
MV
= (MX
|
[:VV, the
carrier of R:] qua
set) by
A1,
Def2;
then MV
= ((MY
|
[:VX, the
carrier of R:] qua
set)
|
[:VV, the
carrier of R:] qua
set) by
A2,
Def2;
then
A7: MV
= (MY
|
[:VV, the
carrier of R:] qua
set) by
A6,
FUNCT_1: 51;
(
0. V)
= (
0. X) by
A1,
Def2;
then (
0. V)
= (
0. Y) by
A2,
Def2;
hence thesis by
A3,
A4,
A7,
Def2;
end;
theorem ::
RMOD_2:27
Th27: 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 MW1 = the
rmult of W1;
set MW2 = the
rmult of W2;
set AV = the
addF of V;
set MV = the
rmult of V;
A1: the
addF of W1
= (AV
|| VW1) & the
addF of W2
= (AV
|| VW2) by
Def2;
assume
A2: the
carrier of W1
c= the
carrier of W2;
then
[:VW1, VW1:]
c=
[:VW2, VW2:] by
ZFMISC_1: 96;
then
A3: the
addF of W1
= (the
addF of W2
|
[:the
carrier of W1, the
carrier of W1:] qua
set) by
A1,
FUNCT_1: 51;
A4: MW1
= (MV
|
[:VW1, the
carrier of R:] qua
set) & MW2
= (MV
|
[:VW2, the
carrier of R:] qua
set) by
Def2;
[:VW1, the
carrier of R:]
c=
[:VW2, the
carrier of R:] by
A2,
ZFMISC_1: 95;
then
A5: MW1
= (MW2
|
[:VW1, the
carrier of R:] qua
set) by
A4,
FUNCT_1: 51;
(
0. W1)
= (
0. V) & (
0. W2)
= (
0. V) by
Def2;
hence thesis by
A2,
A3,
A5,
Def2;
end;
theorem ::
RMOD_2:28
(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
object;
assume
A2: x
in the
carrier of W1;
the
carrier of W1
c= the
carrier of V by
Def2;
then
reconsider v = x as
Vector of V by
A2;
v
in W1 by
A2;
then v
in W2 by
A1;
hence thesis;
end;
hence thesis by
Th27;
end;
theorem ::
RMOD_2:29
Th29: for W1,W2 be
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
Th27;
hence thesis by
Th25;
end;
theorem ::
RMOD_2:30
Th30: for W1,W2 be
strict
Submodule of V holds (for v be
Vector of 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 be
Vector of V holds v
in W1 iff v
in W2;
for x be
object holds x
in the
carrier of W1 iff x
in the
carrier of W2
proof
let x be
object;
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
Def2;
then
reconsider v = x as
Vector of V by
A2;
v
in W1 by
A2;
then v
in W2 by
A1;
hence thesis;
end;
assume
A3: x
in the
carrier of W2;
the
carrier of W2
c= the
carrier of V by
Def2;
then
reconsider v = x as
Vector of V by
A3;
v
in W2 by
A3;
then v
in W1 by
A1;
hence thesis;
end;
then the
carrier of W1
= the
carrier of W2 by
TARSKI: 2;
hence thesis by
Th29;
end;
theorem ::
RMOD_2:31
for V be
strict
RightMod of R, W be
strict
Submodule of V holds the
carrier of W
= the
carrier of V implies W
= V
proof
let V be
strict
RightMod of R, W be
strict
Submodule of V;
assume
A1: the
carrier of W
= the
carrier of V;
V is
Submodule of V by
Th24;
hence thesis by
A1,
Th29;
end;
theorem ::
RMOD_2:32
for V be
strict
RightMod of R, W be
strict
Submodule of V holds (for v be
Vector of V holds v
in W) implies W
= V
proof
let V be
strict
RightMod of R, W be
strict
Submodule of V;
assume for v be
Vector of V holds v
in W;
then
A1: for v be
Vector of V holds (v
in W iff v
in V);
V is
Submodule of V by
Th24;
hence thesis by
A1,
Th30;
end;
theorem ::
RMOD_2:33
the
carrier of W
= V1 implies V1 is
linearly-closed by
Lm1;
theorem ::
RMOD_2:34
Th34: V1
<>
{} & V1 is
linearly-closed implies ex W be
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;
reconsider d = (
0. V) as
Element of D by
A2,
Th1;
set VV = the
carrier of V;
set C = ((
comp V)
| D);
(
dom (
comp V))
= VV by
FUNCT_2:def 1;
then
A3: (
dom C)
= D by
RELAT_1: 62;
A4: (
rng C)
c= D
proof
let x be
object;
assume x
in (
rng C);
then
consider y be
object such that
A5: y
in (
dom C) and
A6: (C
. y)
= x by
FUNCT_1:def 3;
reconsider y as
Vector of V by
A3,
A5;
x
= ((
comp V)
. y) by
A5,
A6,
FUNCT_1: 47
.= (
- y) by
VECTSP_1:def 13;
hence thesis by
A2,
A3,
A5,
Th2;
end;
set M = (the
rmult of V
|
[:D, the
carrier of R:] qua
set);
(
dom the
rmult of V)
=
[:VV, the
carrier of R:] by
FUNCT_2:def 1;
then
A7: (
dom M)
=
[:D, the
carrier of R:] by
RELAT_1: 62,
ZFMISC_1: 96;
A8: (
rng M)
c= D
proof
let x be
object;
assume x
in (
rng M);
then
consider y be
object such that
A9: y
in (
dom M) and
A10: (M
. y)
= x by
FUNCT_1:def 3;
consider y2,y1 be
object such that
A11:
[y2, y1]
= y by
A7,
A9,
RELAT_1:def 1;
reconsider y1 as
Scalar of R by
A7,
A9,
A11,
ZFMISC_1: 87;
A12: y2
in V1 by
A7,
A9,
A11,
ZFMISC_1: 87;
then
reconsider y2 as
Vector of V;
x
= (y2
* y1) by
A9,
A10,
A11,
FUNCT_1: 47;
hence thesis by
A2,
A12;
end;
reconsider C as
UnOp of D by
A3,
A4,
FUNCT_2:def 1,
RELSET_1: 4;
set A = (the
addF of V
|| D);
(
dom the
addF of V)
=
[:VV, VV:] by
FUNCT_2:def 1;
then
A13: (
dom A)
=
[:D, D:] by
RELAT_1: 62,
ZFMISC_1: 96;
A14: (
rng A)
c= D
proof
let x be
object;
assume x
in (
rng A);
then
consider y be
object such that
A15: y
in (
dom A) and
A16: (A
. y)
= x by
FUNCT_1:def 3;
consider y1,y2 be
object such that
A17:
[y1, y2]
= y by
A13,
A15,
RELAT_1:def 1;
A18: y1
in D & y2
in D by
A13,
A15,
A17,
ZFMISC_1: 87;
then
reconsider y1, y2 as
Vector of V;
x
= (y1
+ y2) by
A15,
A16,
A17,
FUNCT_1: 47;
hence thesis by
A2,
A18;
end;
reconsider M as
Function of
[:D, the
carrier of R:], D by
A7,
A8,
FUNCT_2:def 1,
RELSET_1: 4;
reconsider A as
BinOp of D by
A13,
A14,
FUNCT_2:def 1,
RELSET_1: 4;
set W =
RightModStr (# D, A, d, M #);
A19: for a,b be
Element of W holds for x,y be
Vector of V st x
= a & b
= y holds (a
+ b)
= (x
+ y)
proof
let a,b be
Element of W;
let x,y be
Vector of V such that
A20: x
= a & b
= y;
thus (a
+ b)
= (A
.
[a, b])
.= (x
+ y) by
A13,
A20,
FUNCT_1: 47;
end;
A21: W is
Abelian
add-associative
right_zeroed
right_complementable
proof
thus W is
Abelian
proof
let a,b be
Element of W;
reconsider x = a, y = b as
Vector of V by
TARSKI:def 3;
thus (a
+ b)
= (y
+ x) by
A19
.= (b
+ a) by
A19;
end;
hereby
let a,b,c be
Element of W;
reconsider x = a, y = b, z = c as
Vector of V by
TARSKI:def 3;
A22: (b
+ c)
= (y
+ z) by
A19;
(a
+ b)
= (x
+ y) by
A19;
hence ((a
+ b)
+ c)
= ((x
+ y)
+ z) by
A19
.= (x
+ (y
+ z)) by
RLVECT_1:def 3
.= (a
+ (b
+ c)) by
A19,
A22;
end;
hereby
let a be
Element of W;
reconsider x = a as
Vector of V by
TARSKI:def 3;
thus (a
+ (
0. W))
= (x
+ (
0. V)) by
A19
.= a by
RLVECT_1:def 4;
end;
let a be
Element of W;
reconsider x = a as
Vector of V by
TARSKI:def 3;
reconsider b9 = ((
comp V)
. x) as
Vector of V;
(C
. x)
in D by
FUNCT_2: 5;
then
reconsider b = (((
comp V)
| D)
. x) as
Element of W;
take b;
thus (a
+ b)
= (x
+ b9) by
A19,
FUNCT_1: 49
.= (x
+ (
- x)) by
VECTSP_1:def 13
.= (
0. W) by
RLVECT_1: 5;
end;
W is
RightMod-like
proof
let a,b be
Scalar of R;
let v,w be
Vector of W;
reconsider x = v, y = w as
Vector of V by
TARSKI:def 3;
A23:
now
let a be
Scalar of R;
let x be
Element of W;
let y be
Vector of V;
assume
A24: y
= x;
[x, a]
in (
dom M) by
A7;
hence (x
* a)
= (y
* a) by
A24,
FUNCT_1: 47;
end;
then
A25: (v
* a)
= (x
* a);
A26: (w
* a)
= (y
* a) by
A23;
(v
+ w)
= (x
+ y) by
A19;
hence ((v
+ w)
* a)
= ((x
+ y)
* a) by
A23
.= ((x
* a)
+ (y
* a)) by
VECTSP_2:def 9
.= ((v
* a)
+ (w
* a)) by
A19,
A25,
A26;
A27: (v
* b)
= (x
* b) by
A23;
thus (v
* (a
+ b))
= (x
* (a
+ b)) by
A23
.= ((x
* a)
+ (x
* b)) by
VECTSP_2:def 9
.= ((v
* a)
+ (v
* b)) by
A19,
A27,
A25;
thus (v
* (b
* a))
= (x
* (b
* a)) by
A23
.= ((x
* b)
* a) by
VECTSP_2:def 9
.= ((v
* b)
* a) by
A23,
A27;
thus (v
* (
1_ R))
= (x
* (
1_ R)) by
A23
.= v by
VECTSP_2:def 9;
end;
then
reconsider W as
RightMod of R by
A21;
(
0. W)
= (
0. V);
then
reconsider W as
strict
Submodule of V by
Def2;
take W;
thus thesis;
end;
definition
let R;
let V;
::
RMOD_2:def3
func
(0). V ->
strict
Submodule of V means
:
Def3: the
carrier of it
=
{(
0. V)};
correctness by
Th4,
Th29,
Th34;
end
definition
let R;
let V;
::
RMOD_2:def4
func
(Omega). V ->
strict
Submodule of V equals the RightModStr of V;
coherence
proof
set W = the RightModStr of V;
A1: W is
RightMod-like
proof
let x,y be
Element of R, v,w be
Element of W;
reconsider v9 = v, w9 = w as
Vector of V;
thus ((v
+ w)
* x)
= ((v9
+ w9)
* x)
.= ((v9
* x)
+ (w9
* x)) by
VECTSP_2:def 9
.= ((v
* x)
+ (w
* x));
thus (v
* (x
+ y))
= (v9
* (x
+ y))
.= ((v9
* x)
+ (v9
* y)) by
VECTSP_2:def 9
.= ((v
* x)
+ (v
* y));
thus (v
* (y
* x))
= (v9
* (y
* x))
.= ((v9
* y)
* x) by
VECTSP_2:def 9
.= ((v
* y)
* x);
thus (v
* (
1_ R))
= (v9
* (
1_ R))
.= v by
VECTSP_2:def 9;
end;
A2: for a holds for v,w be
Vector of W, v9,w9 be
Vector of V st v
= v9 & w
= w9 holds (v
+ w)
= (v9
+ w9) & (v
* a)
= (v9
* a);
W is
Abelian
add-associative
right_zeroed
right_complementable
proof
thus W is
Abelian
proof
let x,y be
Element of W;
reconsider x9 = x, y9 = y as
Vector of V;
thus (x
+ y)
= (y9
+ x9) by
A2
.= (y
+ x);
end;
hereby
let x,y,z be
Element of W;
reconsider x9 = x, y9 = y, z9 = z as
Vector of V;
thus ((x
+ y)
+ z)
= ((x9
+ y9)
+ z9)
.= (x9
+ (y9
+ z9)) by
RLVECT_1:def 3
.= (x
+ (y
+ z));
end;
hereby
let x be
Element of W;
reconsider x9 = x as
Vector of V;
thus (x
+ (
0. W))
= (x9
+ (
0. V))
.= x by
RLVECT_1: 4;
end;
let x be
Element of W;
reconsider x9 = x as
Vector of V;
consider b be
Vector of V such that
A3: (x9
+ b)
= (
0. V) by
ALGSTR_0:def 11;
reconsider b9 = b as
Element of W;
take b9;
thus thesis by
A3;
end;
then
reconsider W as
RightMod of R by
A1;
A4: the
rmult of W
= (the
rmult of V
|
[:the
carrier of W, the
carrier of R:] qua
set) by
RELSET_1: 19;
(
0. W)
= (
0. V) & the
addF of W
= (the
addF of V
|
[:the
carrier of W, the
carrier of W:] qua
set) by
RELSET_1: 19;
hence thesis by
A4,
Def2;
end;
end
theorem ::
RMOD_2:35
x
in (
(0). V) iff x
= (
0. V)
proof
thus x
in (
(0). V) implies x
= (
0. V)
proof
assume x
in (
(0). V);
then x
in the
carrier of (
(0). V);
then x
in
{(
0. V)} by
Def3;
hence thesis by
TARSKI:def 1;
end;
thus thesis by
Th17;
end;
theorem ::
RMOD_2:36
Th36: (
(0). W)
= (
(0). V)
proof
the
carrier of (
(0). W)
=
{(
0. W)} & the
carrier of (
(0). V)
=
{(
0. V)} by
Def3;
then
A1: the
carrier of (
(0). W)
= the
carrier of (
(0). V) by
Def2;
(
(0). W) is
Submodule of V by
Th26;
hence thesis by
A1,
Th29;
end;
theorem ::
RMOD_2:37
Th37: (
(0). W1)
= (
(0). W2)
proof
(
(0). W1)
= (
(0). V) by
Th36;
hence thesis by
Th36;
end;
theorem ::
RMOD_2:38
(
(0). W) is
Submodule of V by
Th26;
theorem ::
RMOD_2:39
(
(0). V) is
Submodule of W
proof
(
(0). W)
= (
(0). V) by
Th36;
hence thesis;
end;
theorem ::
RMOD_2:40
(
(0). W1) is
Submodule of W2
proof
(
(0). W1)
= (
(0). W2) by
Th37;
hence thesis;
end;
theorem ::
RMOD_2:41
for V be
strict
RightMod of R holds V is
Submodule of (
(Omega). V);
definition
let R;
let V;
let v, W;
::
RMOD_2:def5
func v
+ W ->
Subset of V equals { (v
+ u) : u
in W };
coherence
proof
set Y = { (v
+ u) : u
in W };
defpred
P[
object] means ex u st $1
= (v
+ u) & u
in W;
consider X be
set such that
A1: for x be
object holds x
in X iff x
in the
carrier of V &
P[x] from
XBOOLE_0:sch 1;
X
c= the
carrier of V by
A1;
then
reconsider X as
Subset of V;
A2: Y
c= X
proof
let x be
object;
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
object;
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
Lm2: ((
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
object;
assume x
in the
carrier of W;
then
A2: x
in W;
then x
in V by
Th9;
then
reconsider y = x as
Element of V;
((
0. V)
+ y)
= x by
RLVECT_1:def 4;
hence thesis by
A2;
end;
A
c= the
carrier of W
proof
let x be
object;
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:def 4;
hence thesis by
A4;
end;
hence thesis by
A1;
end;
definition
let R;
let V;
let W;
::
RMOD_2:def6
mode
Coset of W ->
Subset of V means
:
Def6: ex v st it
= (v
+ W);
existence
proof
reconsider VW = the
carrier of W as
Subset of V by
Def2;
take VW;
take (
0. V);
thus thesis by
Lm2;
end;
end
reserve B,C for
Coset of W;
theorem ::
RMOD_2:42
Th42: x
in (v
+ W) iff ex u st u
in W & x
= (v
+ u)
proof
thus x
in (v
+ W) implies ex u st u
in W & x
= (v
+ u)
proof
assume x
in (v
+ W);
then
consider u such that
A1: x
= (v
+ u) & u
in W;
take u;
thus thesis by
A1;
end;
given u such that
A2: u
in W & x
= (v
+ u);
thus thesis by
A2;
end;
theorem ::
RMOD_2:43
Th43: (
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,
VECTSP_1: 16;
hence thesis by
A2,
Th22;
end;
assume v
in W;
then
A3: (
- v)
in W by
Th22;
(
0. V)
= (v
+ (
- v)) by
VECTSP_1: 19;
hence thesis by
A3;
end;
theorem ::
RMOD_2:44
Th44: v
in (v
+ W)
proof
(v
+ (
0. V))
= v & (
0. V)
in W by
Th17,
RLVECT_1:def 4;
hence thesis;
end;
theorem ::
RMOD_2:45
((
0. V)
+ W)
= the
carrier of W by
Lm2;
theorem ::
RMOD_2:46
Th46: (v
+ (
(0). V))
=
{v}
proof
thus (v
+ (
(0). V))
c=
{v}
proof
let x be
object;
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
Def3;
u
in the
carrier of (
(0). V) by
A2;
then u
= (
0. V) by
A3,
TARSKI:def 1;
then x
= v by
A1,
RLVECT_1:def 4;
hence thesis by
TARSKI:def 1;
end;
let x be
object;
assume x
in
{v};
then
A4: x
= v by
TARSKI:def 1;
(
0. V)
in (
(0). V) & v
= (v
+ (
0. V)) by
Th17,
RLVECT_1:def 4;
hence thesis by
A4;
end;
Lm3: v
in W iff (v
+ W)
= the
carrier of W
proof
(
0. V)
in W & (v
+ (
0. V))
= v by
Th17,
RLVECT_1:def 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
object;
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,
Th20;
hence thesis by
A3;
end;
let x be
object;
assume x
in the
carrier of W;
then
reconsider y = x, z = v as
Element of W by
A2;
reconsider y1 = y, z1 = z as
Vector of V by
Th10;
A5: (z
+ (y
- z))
= (y
+ (z
+ (
- z))) by
RLVECT_1:def 3
.= (y
+ (
0. W)) by
VECTSP_1: 19
.= x by
RLVECT_1:def 4;
(y
- z)
in W;
then
A6: (y1
- z1)
in W by
Th16;
(y
- z)
= (y1
- z1) by
Th16;
then (z1
+ (y1
- z1))
= x by
A5,
Th13;
hence thesis by
A6;
end;
assume
A7: (v
+ W)
= the
carrier of W;
assume not v
in W;
hence thesis by
A7,
A1;
end;
theorem ::
RMOD_2:47
Th47: (v
+ (
(Omega). V))
= the
carrier of V by
RLVECT_1: 1,
Lm3;
theorem ::
RMOD_2:48
Th48: (
0. V)
in (v
+ W) iff (v
+ W)
= the
carrier of W by
Th43,
Lm3;
theorem ::
RMOD_2:49
v
in W iff (v
+ W)
= the
carrier of W by
Lm3;
theorem ::
RMOD_2:50
v
in W implies ((v
* a)
+ W)
= the
carrier of W by
Th21,
Lm3;
theorem ::
RMOD_2:51
Th51: 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
object;
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
VECTSP_1: 19
.= x by
A2,
RLVECT_1:def 4;
(v1
- u)
in W by
A1,
A3,
Th23;
hence thesis by
A4;
end;
let x be
object;
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,
Th20;
hence thesis by
A7;
end;
assume
A8: (v
+ W)
= ((v
+ u)
+ W);
(
0. V)
in W & (v
+ (
0. V))
= v by
Th17,
RLVECT_1:def 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
+ (u
+ u1)) by
A9,
RLVECT_1:def 3;
then (u
+ u1)
= (
0. V) by
RLVECT_1: 9;
then u
= (
- u1) by
VECTSP_1: 16;
hence thesis by
A10,
Th22;
end;
theorem ::
RMOD_2:52
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
Th22;
hence thesis by
RLVECT_1: 17;
end;
(
- u)
in W iff (v
+ W)
= ((v
+ (
- u))
+ W) by
Th51;
hence thesis by
A1,
Th22;
end;
theorem ::
RMOD_2:53
Th53: 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 be
Vector of V such that
A1: v
= (u
+ z) and
A2: z
in W;
thus (u
+ W)
c= (v
+ W)
proof
let x be
object;
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
VECTSP_1: 19
.= u by
RLVECT_1:def 4;
then
A5: x
= (v
+ (v1
+ (
- z))) by
A3,
RLVECT_1:def 3
.= (v
+ (v1
- z));
(v1
- z)
in W by
A2,
A4,
Th23;
hence thesis by
A5;
end;
let x be
object;
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,
Th20,
RLVECT_1:def 3;
hence thesis;
end;
thus thesis by
Th44;
end;
theorem ::
RMOD_2:54
Th54: 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);
thus (v1
+ W)
= (u
+ W) by
A1,
Th53
.= (v2
+ W) by
A2,
Th53;
end;
theorem ::
RMOD_2:55
Th55: v
in W implies (v
* a)
in (v
+ W)
proof
assume v
in W;
then (v
+ W)
= the
carrier of W & (v
* a)
in W by
Lm3,
Th21;
hence thesis;
end;
theorem ::
RMOD_2:56
v
in W implies (
- v)
in (v
+ W)
proof
assume v
in W;
then (v
* (
- (
1_ R)))
in (v
+ W) by
Th55;
hence thesis by
VECTSP_2: 32;
end;
theorem ::
RMOD_2:57
Th57: (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 ::
RMOD_2:58
(v
- u)
in (v
+ W) iff u
in W
proof
A1: (v
- u)
= ((
- u)
+ v);
A2: (
- u)
in W implies (
- (
- u))
in W by
Th22;
u
in W implies (
- u)
in W by
Th22;
hence thesis by
A1,
A2,
Th57,
RLVECT_1: 17;
end;
theorem ::
RMOD_2:59
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,
Th22;
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,
Th22;
hence thesis by
A4;
end;
theorem ::
RMOD_2:60
Th60: (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,
Th42;
consider u1 such that
A5: u1
in W and
A6: v1
= (v
+ u1) by
A1,
Th42;
(v1
- v2)
= ((u1
+ v)
+ ((
- v)
- u2)) by
A6,
A4,
VECTSP_1: 17
.= (((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:def 4;
hence thesis by
A5,
A3,
Th23;
end;
assume (v1
- v2)
in W;
then
A7: (
- (v1
- v2))
in W by
Th22;
take v1;
thus v1
in (v1
+ W) by
Th44;
(v1
+ (
- (v1
- v2)))
= (v1
+ ((
- v1)
+ v2)) by
VECTSP_1: 17
.= ((v1
+ (
- v1))
+ v2) by
RLVECT_1:def 3
.= ((
0. V)
+ v2) by
RLVECT_1: 5
.= v2 by
RLVECT_1:def 4;
hence thesis by
A7;
end;
theorem ::
RMOD_2:61
Th61: (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
Th44;
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,
VECTSP_1: 19
.= (u1
+ (u
- v)) by
RLVECT_1:def 3;
then v1
= (
- u1) by
VECTSP_1: 16;
hence v1
in W by
A2,
Th22;
thus (v
+ v1)
= ((u
+ v)
- v) by
RLVECT_1:def 3
.= (u
+ (v
- v)) by
RLVECT_1:def 3
.= (u
+ (
0. V)) by
VECTSP_1: 19
.= u by
RLVECT_1:def 4;
end;
theorem ::
RMOD_2:62
Th62: (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
Th44;
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,
VECTSP_1: 19
.= (u1
+ (v
- u)) by
RLVECT_1:def 3;
then v1
= (
- u1) by
VECTSP_1: 16;
hence v1
in W by
A2,
Th22;
thus (v
- v1)
= ((v
- v)
+ u) by
RLVECT_1: 29
.= ((
0. V)
+ u) by
VECTSP_1: 19
.= u by
RLVECT_1:def 4;
end;
theorem ::
RMOD_2:63
Th63: for W1,W2 be
strict
Submodule of V holds (v
+ W1)
= (v
+ W2) iff W1
= W2
proof
let W1,W2 be
strict
Submodule of V;
thus (v
+ W1)
= (v
+ W2) implies W1
= W2
proof
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
Def2;
thus the
carrier of W1
c= the
carrier of W2
proof
let x be
object;
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;
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;
end;
let x be
object;
assume
A6: x
in the
carrier of W2;
the
carrier of W2
c= the
carrier of V by
Def2;
then
reconsider y = x as
Element of V by
A6;
set z = (v
+ y);
x
in W2 by
A6;
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;
end;
hence thesis by
Th29;
end;
thus thesis;
end;
theorem ::
RMOD_2:64
Th64: for W1,W2 be
strict
Submodule of V holds (v
+ W1)
= (u
+ W2) implies 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;
then x
in V by
Th9;
then
reconsider x as
Element of V;
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:def 4
.= ((v
+ (
- v))
+ x) by
VECTSP_1: 19
.= ((
- v)
+ (u
+ u1)) by
A5,
RLVECT_1:def 3;
then
A7: ((v
+ ((
- v)
+ (u
+ u1)))
+ W1)
= (v
+ W1) by
A4,
Th51;
(v
+ ((
- v)
+ (u
+ u1)))
= ((v
+ (
- v))
+ (u
+ u1)) by
RLVECT_1:def 3
.= ((
0. V)
+ (u
+ u1)) by
VECTSP_1: 19
.= (u
+ u1) by
RLVECT_1:def 4;
then ((u
+ u1)
+ W2)
= ((u
+ u1)
+ W1) by
A1,
A6,
A7,
Th51;
hence thesis by
A2,
Th63;
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;
then x
in V by
Th9;
then
reconsider x as
Element of V;
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:def 4
.= ((u
+ (
- u))
+ x) by
VECTSP_1: 19
.= ((
- u)
+ (v
+ u1)) by
A10,
RLVECT_1:def 3;
then
A12: ((u
+ ((
- u)
+ (v
+ u1)))
+ W2)
= (u
+ W2) by
A9,
Th51;
(u
+ ((
- u)
+ (v
+ u1)))
= ((u
+ (
- u))
+ (v
+ u1)) by
RLVECT_1:def 3
.= ((
0. V)
+ (v
+ u1)) by
VECTSP_1: 19
.= (v
+ u1) by
RLVECT_1:def 4;
then ((v
+ u1)
+ W1)
= ((v
+ u1)
+ W2) by
A1,
A11,
A12,
Th51;
hence thesis by
A2,
Th63;
end;
V1
<> V2 by
A2,
Th29;
then not V1
c= V2 or not V2
c= V1;
hence thesis by
A3,
A8,
XBOOLE_1: 37;
end;
theorem ::
RMOD_2:65
ex C st v
in C
proof
reconsider C = (v
+ W) as
Coset of W by
Def6;
take C;
thus thesis by
Th44;
end;
theorem ::
RMOD_2:66
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
Def6;
C
<>
{} by
A2,
Th44;
then (
0. V)
in (v
+ W) by
A1,
A2,
Th1;
hence thesis by
A2,
Th48;
end;
thus thesis by
Lm1;
end;
theorem ::
RMOD_2:67
for W1,W2 be
strict
Submodule of V holds for C1 be
Coset of W1, C2 be
Coset of W2 holds C1
= C2 implies W1
= W2
proof
let W1,W2 be
strict
Submodule of V;
let C1 be
Coset of W1, C2 be
Coset of W2;
(ex v1 be
Vector of V st C1
= (v1
+ W1)) & ex v2 be
Vector of V st C2
= (v2
+ W2) by
Def6;
hence thesis by
Th64;
end;
theorem ::
RMOD_2:68
{v} is
Coset of (
(0). V)
proof
(v
+ (
(0). V))
=
{v} by
Th46;
hence thesis by
Def6;
end;
theorem ::
RMOD_2:69
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
Def6;
take v;
thus thesis by
A1,
Th46;
end;
theorem ::
RMOD_2:70
the
carrier of W is
Coset of W
proof
the
carrier of W
= ((
0. V)
+ W) by
Lm2;
hence thesis by
Def6;
end;
theorem ::
RMOD_2:71
the
carrier of V is
Coset of (
(Omega). V)
proof
set v = the
Vector of V;
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
Th47;
hence thesis by
Def6;
end;
theorem ::
RMOD_2:72
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
Def6;
hence thesis by
Th47;
end;
theorem ::
RMOD_2:73
(
0. V)
in C iff C
= the
carrier of W
proof
ex v st C
= (v
+ W) by
Def6;
hence thesis by
Th48;
end;
theorem ::
RMOD_2:74
Th74: 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
Def6;
hence thesis by
A1,
Th53;
end;
thus thesis by
Th44;
end;
theorem ::
RMOD_2:75
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
Th74;
hence thesis by
Th61;
end;
theorem ::
RMOD_2:76
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
Th74;
hence thesis by
Th62;
end;
theorem ::
RMOD_2:77
(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
Def6;
hence thesis by
A1,
Th60;
end;
assume (v1
- v2)
in W;
then
consider v such that
A2: v1
in (v
+ W) & v2
in (v
+ W) by
Th60;
reconsider C = (v
+ W) as
Coset of W by
Def6;
take C;
thus thesis by
A2;
end;
theorem ::
RMOD_2:78
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
Def6;
hence thesis by
A1,
Th54;
end;