Metamath Proof Explorer

Theorem nvss

Description: Structure of the class of all normed complex vectors spaces. (Contributed by NM, 28-Nov-2006) (Revised by Mario Carneiro, 1-May-2015) (New usage is discouraged.)

Ref Expression
Assertion nvss 
|- NrmCVec C_ ( CVecOLD X. _V )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( w = <. g , s >. -> ( w e. CVecOLD <-> <. g , s >. e. CVecOLD ) )
2 1 biimpar 
 |-  ( ( w = <. g , s >. /\ <. g , s >. e. CVecOLD ) -> w e. CVecOLD )
3 2 3ad2antr1 
 |-  ( ( w = <. g , s >. /\ ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) ) -> w e. CVecOLD )
4 3 exlimivv 
 |-  ( E. g E. s ( w = <. g , s >. /\ ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) ) -> w e. CVecOLD )
5 vex 
 |-  n e. _V
6 4 5 jctir 
 |-  ( E. g E. s ( w = <. g , s >. /\ ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) ) -> ( w e. CVecOLD /\ n e. _V ) )
7 6 ssopab2i 
 |-  { <. w , n >. | E. g E. s ( w = <. g , s >. /\ ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) ) } C_ { <. w , n >. | ( w e. CVecOLD /\ n e. _V ) }
8 df-nv 
 |-  NrmCVec = { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }
9 dfoprab2 
 |-  { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) } = { <. w , n >. | E. g E. s ( w = <. g , s >. /\ ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) ) }
10 8 9 eqtri 
 |-  NrmCVec = { <. w , n >. | E. g E. s ( w = <. g , s >. /\ ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) ) }
11 df-xp 
 |-  ( CVecOLD X. _V ) = { <. w , n >. | ( w e. CVecOLD /\ n e. _V ) }
12 7 10 11 3sstr4i 
 |-  NrmCVec C_ ( CVecOLD X. _V )