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 )
38 ax-hfvadd 
 |-  +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 )