let V be RealUnitarySpace; 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;
reconsider d1 = 0. V as Element of D by A2, RLSUB_1:1;
set S = the scalar of V || V1;
set VV = the carrier of V;
set M = the Mult of V | [:REAL,V1:];
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, RLSUB_1:def 1;
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;
dom the addF of V = [: the carrier of V, the carrier of V:]
by FUNCT_2:def 1;
then A12:
dom ( the addF of V || V1) = [: the carrier of V, the carrier of V:] /\ [:V1,V1:]
by RELAT_1:61;
then reconsider S = the scalar of V || V1 as Function of [:D,D:],REAL by FUNCT_2:32;
A13:
dom ( the addF of V || V1) = [:D,D:]
by A12, 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 A16:
x in dom ( the addF of V || V1)
and A17:
y = ( the addF of V || V1) . x
;
y in Dconsider x1,
x2 being
object such that A18:
(
x1 in D &
x2 in D )
and A19:
x = [x1,x2]
by A13, A16, ZFMISC_1:def 2;
reconsider v1 =
x1,
v2 =
x2 as
Element of the
carrier of
V by A18;
[x1,x2] in [:V1,V1:]
by A18, ZFMISC_1:87;
then
y = v1 + v2
by A17, A19, FUNCT_1:49;
hence
y in D
by A2, A18, RLSUB_1:def 1;
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 A13, FUNCT_2:def 1, RELSET_1:4;
set W = UNITSTR(# D,d1,A,M,S #);
UNITSTR(# D,d1,A,M,S #) is Subspace of V
by Th18;
hence
ex W being strict Subspace of V st V1 = the carrier of W
; verum