# 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 )`