Metamath Proof Explorer

Theorem hhssva

Description: The vector addition 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 hhssva
`|- ( +h |` ( H X. H ) ) = ( +v ` W )`

Proof

Step Hyp Ref Expression
1 hhss.1
` |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
2 eqid
` |-  ( +v ` W ) = ( +v ` W )`
3 2 vafval
` |-  ( +v ` W ) = ( 1st ` ( 1st ` W ) )`
4 1 fveq2i
` |-  ( 1st ` W ) = ( 1st ` <. <. ( +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 op1st
` |-  ( 1st ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) = <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >.`
12 4 11 eqtri
` |-  ( 1st ` W ) = <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >.`
13 12 fveq2i
` |-  ( 1st ` ( 1st ` W ) ) = ( 1st ` <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. )`
14 hilablo
` |-  +h e. AbelOp`
15 resexg
` |-  ( +h e. AbelOp -> ( +h |` ( H X. H ) ) e. _V )`
16 14 15 ax-mp
` |-  ( +h |` ( H X. H ) ) e. _V`
17 hvmulex
` |-  .h e. _V`
18 17 resex
` |-  ( .h |` ( CC X. H ) ) e. _V`
19 16 18 op1st
` |-  ( 1st ` <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. ) = ( +h |` ( H X. H ) )`
20 3 13 19 3eqtrri
` |-  ( +h |` ( H X. H ) ) = ( +v ` W )`