Metamath Proof Explorer

Theorem hhssnm

Description: The norm operation on a subspace. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhss.1 
|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
Assertion hhssnm 
|- ( normh |` H ) = ( normCV ` W )

Proof

Step Hyp Ref Expression
1 hhss.1 
 |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
2 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
3 2 nmcvfval 
 |-  ( normCV ` W ) = ( 2nd ` W )
4 1 fveq2i 
 |-  ( 2nd ` W ) = ( 2nd ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. )
5 opex 
 |-  <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. e. _V
6 normf 
 |-  normh : ~H --> RR
7 ax-hilex 
 |-  ~H e. _V
8 fex 
 |-  ( ( normh : ~H --> RR /\ ~H e. _V ) -> normh e. _V )
9 6 7 8 mp2an 
 |-  normh e. _V
10 9 resex 
 |-  ( normh |` H ) e. _V
11 5 10 op2nd 
 |-  ( 2nd ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) = ( normh |` H )
12 3 4 11 3eqtrri 
 |-  ( normh |` H ) = ( normCV ` W )