# Metamath Proof Explorer

## Theorem hhshsslem1

Description: Lemma for hhsssh . (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsst.1
`|- U = <. <. +h , .h >. , normh >.`
hhsst.2
`|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
hhssp3.3
`|- W e. ( SubSp ` U )`
hhssp3.4
`|- H C_ ~H`
Assertion hhshsslem1
`|- H = ( BaseSet ` W )`

### Proof

Step Hyp Ref Expression
1 hhsst.1
` |-  U = <. <. +h , .h >. , normh >.`
2 hhsst.2
` |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
3 hhssp3.3
` |-  W e. ( SubSp ` U )`
4 hhssp3.4
` |-  H C_ ~H`
5 eqid
` |-  ( BaseSet ` W ) = ( BaseSet ` W )`
6 eqid
` |-  ( +v ` W ) = ( +v ` W )`
7 5 6 bafval
` |-  ( BaseSet ` W ) = ran ( +v ` W )`
8 1 hhnv
` |-  U e. NrmCVec`
9 eqid
` |-  ( SubSp ` U ) = ( SubSp ` U )`
10 9 sspnv
` |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> W e. NrmCVec )`
11 8 3 10 mp2an
` |-  W e. NrmCVec`
12 6 nvgrp
` |-  ( W e. NrmCVec -> ( +v ` W ) e. GrpOp )`
13 grporndm
` |-  ( ( +v ` W ) e. GrpOp -> ran ( +v ` W ) = dom dom ( +v ` W ) )`
14 11 12 13 mp2b
` |-  ran ( +v ` W ) = dom dom ( +v ` W )`
15 2 fveq2i
` |-  ( +v ` W ) = ( +v ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. )`
16 eqid
` |-  ( +v ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) = ( +v ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. )`
17 16 vafval
` |-  ( +v ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) = ( 1st ` ( 1st ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) )`
18 opex
` |-  <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. e. _V`
19 normf
` |-  normh : ~H --> RR`
20 ax-hilex
` |-  ~H e. _V`
21 fex
` |-  ( ( normh : ~H --> RR /\ ~H e. _V ) -> normh e. _V )`
22 19 20 21 mp2an
` |-  normh e. _V`
23 22 resex
` |-  ( normh |` H ) e. _V`
24 18 23 op1st
` |-  ( 1st ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) = <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >.`
25 24 fveq2i
` |-  ( 1st ` ( 1st ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) ) = ( 1st ` <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. )`
26 hilablo
` |-  +h e. AbelOp`
27 resexg
` |-  ( +h e. AbelOp -> ( +h |` ( H X. H ) ) e. _V )`
28 26 27 ax-mp
` |-  ( +h |` ( H X. H ) ) e. _V`
29 hvmulex
` |-  .h e. _V`
30 29 resex
` |-  ( .h |` ( CC X. H ) ) e. _V`
31 28 30 op1st
` |-  ( 1st ` <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. ) = ( +h |` ( H X. H ) )`
32 25 31 eqtri
` |-  ( 1st ` ( 1st ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) ) = ( +h |` ( H X. H ) )`
33 17 32 eqtri
` |-  ( +v ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) = ( +h |` ( H X. H ) )`
34 15 33 eqtri
` |-  ( +v ` W ) = ( +h |` ( H X. H ) )`
35 34 dmeqi
` |-  dom ( +v ` W ) = dom ( +h |` ( H X. H ) )`
36 xpss12
` |-  ( ( H C_ ~H /\ H C_ ~H ) -> ( H X. H ) C_ ( ~H X. ~H ) )`
37 4 4 36 mp2an
` |-  ( H X. H ) C_ ( ~H X. ~H )`
` |-  +h : ( ~H X. ~H ) --> ~H`
39 38 fdmi
` |-  dom +h = ( ~H X. ~H )`
40 37 39 sseqtrri
` |-  ( H X. H ) C_ dom +h`
41 ssdmres
` |-  ( ( H X. H ) C_ dom +h <-> dom ( +h |` ( H X. H ) ) = ( H X. H ) )`
42 40 41 mpbi
` |-  dom ( +h |` ( H X. H ) ) = ( H X. H )`
43 35 42 eqtri
` |-  dom ( +v ` W ) = ( H X. H )`
44 43 dmeqi
` |-  dom dom ( +v ` W ) = dom ( H X. H )`
45 dmxpid
` |-  dom ( H X. H ) = H`
46 44 45 eqtri
` |-  dom dom ( +v ` W ) = H`
47 14 46 eqtri
` |-  ran ( +v ` W ) = H`
48 7 47 eqtri
` |-  ( BaseSet ` W ) = H`
49 48 eqcomi
` |-  H = ( BaseSet ` W )`