let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
let V be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
let V1 be Subset of V; :: thesis: ( V1 <> {} & V1 is linearly-closed implies ex W being strict Subspace of V st V1 = the carrier of W )
assume that
A1:
V1 <> {}
and
A2:
V1 is linearly-closed
; :: thesis: ex W being strict Subspace of V st V1 = the carrier of W
set VV = the carrier of V;
reconsider D = V1 as non empty set by A1;
set A = the addF of V || D;
( V1 c= the carrier of V & dom the addF of V = [:the carrier of V,the carrier of V:] )
by FUNCT_2:def 1;
then A3:
dom (the addF of V || D) = [:D,D:]
by RELAT_1:91, ZFMISC_1:119;
rng (the addF of V || D) c= D
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng (the addF of V || D) or x in D )
assume
x in rng (the addF of V || D)
;
:: thesis: x in D
then consider y being
set such that A4:
y in dom (the addF of V || D)
and A5:
(the addF of V || D) . y = x
by FUNCT_1:def 5;
consider y1,
y2 being
set such that A6:
[y1,y2] = y
by A3, A4, RELAT_1:def 1;
A7:
(
y1 in D &
y2 in D &
D c= the
carrier of
V )
by A3, A4, A6, ZFMISC_1:106;
then reconsider y1 =
y1,
y2 =
y2 as
Element of
V ;
x = y1 + y2
by A4, A5, A6, FUNCT_1:70;
hence
x in D
by A2, A7, Def1;
:: thesis: verum
end;
then reconsider A = the addF of V || D as BinOp of D by A3, FUNCT_2:def 1, RELSET_1:11;
set C = (comp V) | D;
( V1 c= the carrier of V & dom (comp V) = the carrier of V )
by FUNCT_2:def 1;
then A8:
dom ((comp V) | D) = D
by RELAT_1:91;
rng ((comp V) | D) c= D
then reconsider C = (comp V) | D as UnOp of D by A8, FUNCT_2:def 1, RELSET_1:11;
set M = the lmult of V | [:the carrier of GF,D:];
reconsider d = 0. V as Element of D by A2, Th4;
dom the lmult of V = [:the carrier of GF,the carrier of V:]
by FUNCT_2:def 1;
then A11:
dom (the lmult of V | [:the carrier of GF,D:]) = [:the carrier of GF,D:]
by RELAT_1:91, ZFMISC_1:119;
rng (the lmult of V | [:the carrier of GF,D:]) c= D
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng (the lmult of V | [:the carrier of GF,D:]) or x in D )
assume
x in rng (the lmult of V | [:the carrier of GF,D:])
;
:: thesis: x in D
then consider y being
set such that A12:
y in dom (the lmult of V | [:the carrier of GF,D:])
and A13:
(the lmult of V | [:the carrier of GF,D:]) . y = x
by FUNCT_1:def 5;
consider y1,
y2 being
set such that A14:
[y1,y2] = y
by A11, A12, RELAT_1:def 1;
A15:
(
y1 in the
carrier of
GF &
y2 in V1 )
by A11, A12, A14, ZFMISC_1:106;
reconsider y1 =
y1 as
Element of
GF by A11, A12, A14, ZFMISC_1:106;
reconsider y2 =
y2 as
Element of
V by A15;
x = y1 * y2
by A12, A13, A14, FUNCT_1:70;
hence
x in D
by A2, A15, Def1;
:: thesis: verum
end;
then reconsider M = the lmult of V | [:the carrier of GF,D:] as Function of [:the carrier of GF,D:],D by A11, FUNCT_2:def 1, RELSET_1:11;
set W = VectSpStr(# D,A,d,M #);
A16:
for a, b being Element of VectSpStr(# D,A,d,M #)
for x, y being Element of V st x = a & b = y holds
a + b = x + y
A18:
( VectSpStr(# D,A,d,M #) is Abelian & VectSpStr(# D,A,d,M #) is add-associative & VectSpStr(# D,A,d,M #) is right_zeroed & VectSpStr(# D,A,d,M #) is right_complementable )
proof
thus
VectSpStr(#
D,
A,
d,
M #) is
Abelian
:: thesis: ( VectSpStr(# D,A,d,M #) is add-associative & VectSpStr(# D,A,d,M #) is right_zeroed & VectSpStr(# D,A,d,M #) is right_complementable )
let a be
Element of
VectSpStr(#
D,
A,
d,
M #);
:: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x =
a as
Element of
V by TARSKI:def 3;
reconsider a' =
a as
Element of
D ;
reconsider b =
C . a' as
Element of
D ;
reconsider b =
b as
Element of
VectSpStr(#
D,
A,
d,
M #) ;
take
b
;
:: according to ALGSTR_0:def 11 :: thesis: a + b = 0. VectSpStr(# D,A,d,M #)
thus a + b =
x + ((comp V) . x)
by A8, A16, FUNCT_1:70
.=
x + (- x)
by VECTSP_1:def 25
.=
0. VectSpStr(#
D,
A,
d,
M #)
by RLVECT_1:16
;
:: thesis: verum
end;
VectSpStr(# D,A,d,M #) is VectSp-like
proof
let a,
b be
Element of
GF;
:: according to VECTSP_1:def 26 :: thesis: for b1, b2 being Element of the carrier of VectSpStr(# D,A,d,M #) holds
( a * (b1 + b2) = (a * b1) + (a * b2) & (a + b) * b1 = (a * b1) + (b * b1) & (a * b) * b1 = a * (b * b1) & (1. GF) * b1 = b1 )let v,
w be
Element of
VectSpStr(#
D,
A,
d,
M #);
:: thesis: ( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. GF) * v = v )
reconsider x =
v,
y =
w as
Element of
V by TARSKI:def 3;
then A22:
(
b * v = b * x &
a * v = a * x &
a * w = a * y )
;
then
(
(a * v) + (a * w) = (a * x) + (a * y) &
v + w = x + y )
by A16;
hence a * (v + w) =
a * (x + y)
by A20
.=
(a * x) + (a * y)
by VECTSP_1:def 26
.=
(a * v) + (a * w)
by A16, A22
;
:: thesis: ( (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. GF) * v = v )
thus (a + b) * v =
(a + b) * x
by A20
.=
(a * x) + (b * x)
by VECTSP_1:def 26
.=
(a * v) + (b * v)
by A16, A22
;
:: thesis: ( (a * b) * v = a * (b * v) & (1. GF) * v = v )
thus (a * b) * v =
(a * b) * x
by A20
.=
a * (b * x)
by VECTSP_1:def 26
.=
a * (b * v)
by A20, A22
;
:: thesis: (1. GF) * v = v
thus (1. GF) * v =
(1_ GF) * x
by A20
.=
v
by VECTSP_1:def 26
;
:: thesis: verum
end;
then reconsider W = VectSpStr(# D,A,d,M #) as non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF by A18;
0. W = 0. V
;
then reconsider W = W as strict Subspace of V by Def2;
take
W
; :: thesis: V1 = the carrier of W
thus
V1 = the carrier of W
; :: thesis: verum