let V be RealLinearSpace; 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; ( 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
; ex W being strict Subspace of V st V1 = the carrier of W
reconsider D = V1 as non empty set by A1;
set M = the Mult of V | [:REAL,V1:];
set VV = the carrier of V;
dom the Mult of V = [:REAL, the carrier of V:]
by FUNCT_2:def 1;
then A3:
dom ( the Mult of V | [:REAL,V1:]) = [:REAL, the carrier of V:] /\ [:REAL,V1:]
by RELAT_1:61;
[:REAL,V1:] c= [:REAL, the carrier of V:]
by ZFMISC_1:95;
then A4:
dom ( the Mult of V | [:REAL,V1:]) = [:REAL,D:]
by A3, XBOOLE_1:28;
now for y being object holds
( ( y in D implies ex x being object st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) ) & ( ex x being object st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) implies y in D ) )let y be
object ;
( ( y in D implies ex x being object st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) ) & ( ex x being object st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) implies y in D ) )thus
(
y in D implies ex
x being
object st
(
x in dom ( the Mult of V | [:REAL,V1:]) &
y = ( the Mult of V | [:REAL,V1:]) . x ) )
( ex x being object st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) implies y in D )proof
assume A5:
y in D
;
ex x being object st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x )
then reconsider v1 =
y as
Element of the
carrier of
V ;
A6:
[jj,y] in [:REAL,D:]
by A5, ZFMISC_1:87;
then ( the Mult of V | [:REAL,V1:]) . [1,y] =
1
* v1
by FUNCT_1:49
.=
y
by RLVECT_1:def 8
;
hence
ex
x being
object st
(
x in dom ( the Mult of V | [:REAL,V1:]) &
y = ( the Mult of V | [:REAL,V1:]) . x )
by A4, A6;
verum
end; given x being
object such that A7:
x in dom ( the Mult of V | [:REAL,V1:])
and A8:
y = ( the Mult of V | [:REAL,V1:]) . x
;
y in Dconsider x1,
x2 being
object such that A9:
x1 in REAL
and A10:
x2 in D
and A11:
x = [x1,x2]
by A4, A7, ZFMISC_1:def 2;
reconsider xx1 =
x1 as
Real by A9;
reconsider v2 =
x2 as
Element of the
carrier of
V by A10;
[x1,x2] in [:REAL,V1:]
by A9, A10, ZFMISC_1:87;
then
y = xx1 * v2
by A8, A11, FUNCT_1:49;
hence
y in D
by A2, A10;
verum end;
then
D = rng ( the Mult of V | [:REAL,V1:])
by FUNCT_1:def 3;
then reconsider M = the Mult of V | [:REAL,V1:] as Function of [:REAL,D:],D by A4, FUNCT_2:def 1, RELSET_1:4;
set A = the addF of V || V1;
reconsider d1 = 0. V as Element of D by A2, Th1;
dom the addF of V = [: the carrier of V, the carrier of V:]
by FUNCT_2:def 1;
then
dom ( the addF of V || V1) = [: the carrier of V, the carrier of V:] /\ [:V1,V1:]
by RELAT_1:61;
then A12:
dom ( the addF of V || V1) = [:D,D:]
by XBOOLE_1:28;
now for y being object holds
( ( y in D implies ex x being object st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) ) & ( ex x being object st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D ) )let y be
object ;
( ( y in D implies ex x being object st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) ) & ( ex x being object st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D ) )thus
(
y in D implies ex
x being
object st
(
x in dom ( the addF of V || V1) &
y = ( the addF of V || V1) . x ) )
( ex x being object st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D )given x being
object such that A15:
x in dom ( the addF of V || V1)
and A16:
y = ( the addF of V || V1) . x
;
y in Dconsider x1,
x2 being
object such that A17:
(
x1 in D &
x2 in D )
and A18:
x = [x1,x2]
by A12, A15, ZFMISC_1:def 2;
reconsider v1 =
x1,
v2 =
x2 as
Element of the
carrier of
V by A17;
[x1,x2] in [:V1,V1:]
by A17, ZFMISC_1:87;
then
y = v1 + v2
by A16, A18, FUNCT_1:49;
hence
y in D
by A2, A17;
verum end;
then
D = rng ( the addF of V || V1)
by FUNCT_1:def 3;
then reconsider A = the addF of V || V1 as Function of [:D,D:],D by A12, FUNCT_2:def 1, RELSET_1:4;
set W = RLSStruct(# D,d1,A,M #);
RLSStruct(# D,d1,A,M #) is Subspace of V
by Th24;
hence
ex W being strict Subspace of V st V1 = the carrier of W
; verum