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