let R be Ring; for V being RightMod of R
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Submodule of V st V1 = the carrier of W
let V be RightMod of R; for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Submodule of V st V1 = the carrier of W
let V1 be Subset of V; ( V1 <> {} & V1 is linearly-closed implies ex W being strict Submodule of V st V1 = the carrier of W )
assume that
A1:
V1 <> {}
and
A2:
V1 is linearly-closed
; ex W being strict Submodule of V st V1 = the carrier of W
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) = the carrier of V
by FUNCT_2:def 1;
then A3:
dom ((comp V) | D) = D
by RELAT_1:62;
A4:
rng ((comp V) | D) c= D
set M = the rmult of V | [:D, the carrier of R:];
dom the rmult of V = [: the carrier of V, the carrier of R:]
by FUNCT_2:def 1;
then A7:
dom ( the rmult of V | [:D, the carrier of R:]) = [:D, the carrier of R:]
by RELAT_1:62, ZFMISC_1:96;
A8:
rng ( the rmult of V | [:D, the carrier of R:]) c= D
proof
let x be
object ;
TARSKI:def 3 ( not x in rng ( the rmult of V | [:D, the carrier of R:]) or x in D )
assume
x in rng ( the rmult of V | [:D, the carrier of R:])
;
x in D
then consider y being
object such that A9:
y in dom ( the rmult of V | [:D, the carrier of R:])
and A10:
( the rmult of V | [:D, the carrier of R:]) . y = x
by FUNCT_1:def 3;
consider y2,
y1 being
object such that A11:
[y2,y1] = y
by A7, A9, RELAT_1:def 1;
reconsider y1 =
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 =
y2 as
Vector of
V ;
x = y2 * y1
by A9, A10, A11, FUNCT_1:47;
hence
x in D
by A2, A12;
verum
end;
reconsider C = (comp V) | D 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 = [: the carrier of V, the carrier of V:]
by FUNCT_2:def 1;
then A13:
dom ( the addF of V || D) = [:D,D:]
by RELAT_1:62, ZFMISC_1:96;
A14:
rng ( the addF of V || D) c= D
proof
let x be
object ;
TARSKI:def 3 ( not x in rng ( the addF of V || D) or x in D )
assume
x in rng ( the addF of V || D)
;
x in D
then consider y being
object such that A15:
y in dom ( the addF of V || D)
and A16:
( the addF of V || D) . y = x
by FUNCT_1:def 3;
consider y1,
y2 being
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 =
y1,
y2 =
y2 as
Vector of
V ;
x = y1 + y2
by A15, A16, A17, FUNCT_1:47;
hence
x in D
by A2, A18;
verum
end;
reconsider M = the rmult of V | [:D, the carrier of R:] as Function of [:D, the carrier of R:],D by A7, A8, FUNCT_2:def 1, RELSET_1:4;
reconsider A = the addF of V || D 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 being Element of RightModStr(# D,A,d,M #)
for x, y being Vector of V st x = a & b = y holds
a + b = x + y
A21:
( RightModStr(# D,A,d,M #) is Abelian & RightModStr(# D,A,d,M #) is add-associative & RightModStr(# D,A,d,M #) is right_zeroed & RightModStr(# D,A,d,M #) is right_complementable )
proof
thus
RightModStr(#
D,
A,
d,
M #) is
Abelian
( RightModStr(# D,A,d,M #) is add-associative & RightModStr(# D,A,d,M #) is right_zeroed & RightModStr(# D,A,d,M #) is right_complementable )
let a be
Element of
RightModStr(#
D,
A,
d,
M #);
ALGSTR_0:def 16 a is right_complementable
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
RightModStr(#
D,
A,
d,
M #) ;
take
b
;
ALGSTR_0:def 11 a + b = 0. RightModStr(# D,A,d,M #)
thus a + b =
x + b9
by A19, FUNCT_1:49
.=
x + (- x)
by VECTSP_1:def 13
.=
0. RightModStr(#
D,
A,
d,
M #)
by RLVECT_1:5
;
verum
end;
RightModStr(# D,A,d,M #) is RightMod-like
proof
let a,
b be
Scalar of
R;
VECTSP_2:def 8 for b1, b2 being Element of the carrier of RightModStr(# D,A,d,M #) holds
( (b1 + b2) * a = (b1 * a) + (b2 * a) & b1 * (a + b) = (b1 * a) + (b1 * b) & b1 * (b * a) = (b1 * b) * a & b1 * (1_ R) = b1 )let v,
w be
Vector of
RightModStr(#
D,
A,
d,
M #);
( (v + w) * a = (v * a) + (w * a) & v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v )
reconsider x =
v,
y =
w as
Vector of
V by TARSKI:def 3;
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
;
( v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v )
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
;
( v * (b * a) = (v * b) * a & v * (1_ R) = v )
thus v * (b * a) =
x * (b * a)
by A23
.=
(x * b) * a
by VECTSP_2:def 9
.=
(v * b) * a
by A23, A27
;
v * (1_ R) = v
thus v * (1_ R) =
x * (1_ R)
by A23
.=
v
by VECTSP_2:def 9
;
verum
end;
then reconsider W = RightModStr(# D,A,d,M #) as RightMod of R by A21;
0. W = 0. V
;
then reconsider W = W as strict Submodule of V by Def2;
take
W
; V1 = the carrier of W
thus
V1 = the carrier of W
; verum