Metamath Proof Explorer

Theorem sspval

Description: The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses sspval.g 
|- G = ( +v ` U )
sspval.s 
|- S = ( .sOLD ` U )
sspval.n 
|- N = ( normCV ` U )
sspval.h 
|- H = ( SubSp ` U )
Assertion sspval 
|- ( U e. NrmCVec -> H = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } )

Proof

Step Hyp Ref Expression
1 sspval.g 
 |-  G = ( +v ` U )
2 sspval.s 
 |-  S = ( .sOLD ` U )
3 sspval.n 
 |-  N = ( normCV ` U )
4 sspval.h 
 |-  H = ( SubSp ` U )
5 fveq2 
 |-  ( u = U -> ( +v ` u ) = ( +v ` U ) )
6 5 1 eqtr4di 
 |-  ( u = U -> ( +v ` u ) = G )
7 6 sseq2d 
 |-  ( u = U -> ( ( +v ` w ) C_ ( +v ` u ) <-> ( +v ` w ) C_ G ) )
8 fveq2 
 |-  ( u = U -> ( .sOLD ` u ) = ( .sOLD ` U ) )
9 8 2 eqtr4di 
 |-  ( u = U -> ( .sOLD ` u ) = S )
10 9 sseq2d 
 |-  ( u = U -> ( ( .sOLD ` w ) C_ ( .sOLD ` u ) <-> ( .sOLD ` w ) C_ S ) )
11 fveq2 
 |-  ( u = U -> ( normCV ` u ) = ( normCV ` U ) )
12 11 3 eqtr4di 
 |-  ( u = U -> ( normCV ` u ) = N )
13 12 sseq2d 
 |-  ( u = U -> ( ( normCV ` w ) C_ ( normCV ` u ) <-> ( normCV ` w ) C_ N ) )
14 7 10 13 3anbi123d 
 |-  ( u = U -> ( ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) <-> ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) ) )
15 14 rabbidv 
 |-  ( u = U -> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } )
16 df-ssp 
 |-  SubSp = ( u e. NrmCVec |-> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } )
17 1 fvexi 
 |-  G e. _V
18 17 pwex 
 |-  ~P G e. _V
19 2 fvexi 
 |-  S e. _V
20 19 pwex 
 |-  ~P S e. _V
21 18 20 xpex 
 |-  ( ~P G X. ~P S ) e. _V
22 3 fvexi 
 |-  N e. _V
23 22 pwex 
 |-  ~P N e. _V
24 21 23 xpex 
 |-  ( ( ~P G X. ~P S ) X. ~P N ) e. _V
25 rabss 
 |-  ( { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } C_ ( ( ~P G X. ~P S ) X. ~P N ) <-> A. w e. NrmCVec ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) -> w e. ( ( ~P G X. ~P S ) X. ~P N ) ) )
26 fvex 
 |-  ( +v ` w ) e. _V
27 26 elpw 
 |-  ( ( +v ` w ) e. ~P G <-> ( +v ` w ) C_ G )
28 fvex 
 |-  ( .sOLD ` w ) e. _V
29 28 elpw 
 |-  ( ( .sOLD ` w ) e. ~P S <-> ( .sOLD ` w ) C_ S )
30 opelxpi 
 |-  ( ( ( +v ` w ) e. ~P G /\ ( .sOLD ` w ) e. ~P S ) -> <. ( +v ` w ) , ( .sOLD ` w ) >. e. ( ~P G X. ~P S ) )
31 27 29 30 syl2anbr 
 |-  ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S ) -> <. ( +v ` w ) , ( .sOLD ` w ) >. e. ( ~P G X. ~P S ) )
32 fvex 
 |-  ( normCV ` w ) e. _V
33 32 elpw 
 |-  ( ( normCV ` w ) e. ~P N <-> ( normCV ` w ) C_ N )
34 33 biimpri 
 |-  ( ( normCV ` w ) C_ N -> ( normCV ` w ) e. ~P N )
35 opelxpi 
 |-  ( ( <. ( +v ` w ) , ( .sOLD ` w ) >. e. ( ~P G X. ~P S ) /\ ( normCV ` w ) e. ~P N ) -> <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. e. ( ( ~P G X. ~P S ) X. ~P N ) )
36 31 34 35 syl2an 
 |-  ( ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S ) /\ ( normCV ` w ) C_ N ) -> <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. e. ( ( ~P G X. ~P S ) X. ~P N ) )
37 36 3impa 
 |-  ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) -> <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. e. ( ( ~P G X. ~P S ) X. ~P N ) )
38 eqid 
 |-  ( +v ` w ) = ( +v ` w )
39 eqid 
 |-  ( .sOLD ` w ) = ( .sOLD ` w )
40 eqid 
 |-  ( normCV ` w ) = ( normCV ` w )
41 38 39 40 nvop 
 |-  ( w e. NrmCVec -> w = <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. )
42 41 eleq1d 
 |-  ( w e. NrmCVec -> ( w e. ( ( ~P G X. ~P S ) X. ~P N ) <-> <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. e. ( ( ~P G X. ~P S ) X. ~P N ) ) )
43 37 42 syl5ibr 
 |-  ( w e. NrmCVec -> ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) -> w e. ( ( ~P G X. ~P S ) X. ~P N ) ) )
44 25 43 mprgbir 
 |-  { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } C_ ( ( ~P G X. ~P S ) X. ~P N )
45 24 44 ssexi 
 |-  { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } e. _V
46 15 16 45 fvmpt 
 |-  ( U e. NrmCVec -> ( SubSp ` U ) = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } )
47 4 46 syl5eq 
 |-  ( U e. NrmCVec -> H = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } )