Metamath Proof Explorer

Theorem hhsssm

Description: The scalar multiplication 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 hhsssm 
|- ( .h |` ( CC X. H ) ) = ( .sOLD ` W )

Proof

Step Hyp Ref Expression
1 hhss.1 
 |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
2 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
3 2 smfval 
 |-  ( .sOLD ` W ) = ( 2nd ` ( 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 
 |-  ( 2nd ` ( 1st ` W ) ) = ( 2nd ` <. ( +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 op2nd 
 |-  ( 2nd ` <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. ) = ( .h |` ( CC X. H ) )
20 3 13 19 3eqtrri 
 |-  ( .h |` ( CC X. H ) ) = ( .sOLD ` W )