HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  hhshsslem1 Structured version   Unicode version

Theorem hhshsslem1 24800
Description: Lemma for hhsssh 24802. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
Hypotheses
Ref Expression
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
Ref Expression
hhshsslem1  |-  H  =  ( BaseSet `  W )

Proof of Theorem hhshsslem1
StepHypRef Expression
1 eqid 2451 . . . 4  |-  ( BaseSet `  W )  =  (
BaseSet `  W )
2 eqid 2451 . . . 4  |-  ( +v
`  W )  =  ( +v `  W
)
31, 2bafval 24114 . . 3  |-  ( BaseSet `  W )  =  ran  ( +v `  W )
4 hhsst.1 . . . . . . 7  |-  U  = 
<. <.  +h  ,  .h  >. ,  normh >.
54hhnv 24699 . . . . . 6  |-  U  e.  NrmCVec
6 hhssp3.3 . . . . . 6  |-  W  e.  ( SubSp `  U )
7 eqid 2451 . . . . . . 7  |-  ( SubSp `  U )  =  (
SubSp `  U )
87sspnv 24256 . . . . . 6  |-  ( ( U  e.  NrmCVec  /\  W  e.  ( SubSp `  U )
)  ->  W  e.  NrmCVec )
95, 6, 8mp2an 672 . . . . 5  |-  W  e.  NrmCVec
102nvgrp 24127 . . . . 5  |-  ( W  e.  NrmCVec  ->  ( +v `  W )  e.  GrpOp )
11 grporndm 23829 . . . . 5  |-  ( ( +v `  W )  e.  GrpOp  ->  ran  ( +v
`  W )  =  dom  dom  ( +v `  W ) )
129, 10, 11mp2b 10 . . . 4  |-  ran  ( +v `  W )  =  dom  dom  ( +v `  W )
13 hhsst.2 . . . . . . . . . 10  |-  W  = 
<. <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >.
1413fveq2i 5789 . . . . . . . . 9  |-  ( +v
`  W )  =  ( +v `  <. <.
(  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )
15 eqid 2451 . . . . . . . . . . 11  |-  ( +v
`  <. <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )  =  ( +v `  <. <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )
1615vafval 24113 . . . . . . . . . 10  |-  ( +v
`  <. <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )  =  ( 1st `  ( 1st `  <. <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )
)
17 opex 4651 . . . . . . . . . . . . 13  |-  <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>.  e.  _V
18 normf 24657 . . . . . . . . . . . . . . 15  |-  normh : ~H --> RR
19 ax-hilex 24533 . . . . . . . . . . . . . . 15  |-  ~H  e.  _V
20 fex 6046 . . . . . . . . . . . . . . 15  |-  ( (
normh : ~H --> RR  /\  ~H  e.  _V )  ->  normh  e.  _V )
2118, 19, 20mp2an 672 . . . . . . . . . . . . . 14  |-  normh  e.  _V
2221resex 5245 . . . . . . . . . . . . 13  |-  ( normh  |`  H )  e.  _V
2317, 22op1st 6682 . . . . . . . . . . . 12  |-  ( 1st `  <. <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )  =  <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>.
2423fveq2i 5789 . . . . . . . . . . 11  |-  ( 1st `  ( 1st `  <. <.
(  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )
)  =  ( 1st `  <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. )
25 hilablo 24694 . . . . . . . . . . . . 13  |-  +h  e.  AbelOp
26 resexg 5244 . . . . . . . . . . . . 13  |-  (  +h  e.  AbelOp  ->  (  +h  |`  ( H  X.  H ) )  e.  _V )
2725, 26ax-mp 5 . . . . . . . . . . . 12  |-  (  +h  |`  ( H  X.  H
) )  e.  _V
28 hvmulex 24545 . . . . . . . . . . . . 13  |-  .h  e.  _V
2928resex 5245 . . . . . . . . . . . 12  |-  (  .h  |`  ( CC  X.  H
) )  e.  _V
3027, 29op1st 6682 . . . . . . . . . . 11  |-  ( 1st `  <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. )  =  (  +h  |`  ( H  X.  H ) )
3124, 30eqtri 2479 . . . . . . . . . 10  |-  ( 1st `  ( 1st `  <. <.
(  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )
)  =  (  +h  |`  ( H  X.  H
) )
3216, 31eqtri 2479 . . . . . . . . 9  |-  ( +v
`  <. <. (  +h  |`  ( H  X.  H ) ) ,  (  .h  |`  ( CC  X.  H ) )
>. ,  ( normh  |`  H ) >. )  =  (  +h  |`  ( H  X.  H ) )
3314, 32eqtri 2479 . . . . . . . 8  |-  ( +v
`  W )  =  (  +h  |`  ( H  X.  H ) )
3433dmeqi 5136 . . . . . . 7  |-  dom  ( +v `  W )  =  dom  (  +h  |`  ( H  X.  H ) )
35 hhssp3.4 . . . . . . . . . 10  |-  H  C_  ~H
36 xpss12 5040 . . . . . . . . . 10  |-  ( ( H  C_  ~H  /\  H  C_ 
~H )  ->  ( H  X.  H )  C_  ( ~H  X.  ~H )
)
3735, 35, 36mp2an 672 . . . . . . . . 9  |-  ( H  X.  H )  C_  ( ~H  X.  ~H )
38 ax-hfvadd 24534 . . . . . . . . . 10  |-  +h  :
( ~H  X.  ~H )
--> ~H
3938fdmi 5659 . . . . . . . . 9  |-  dom  +h  =  ( ~H  X.  ~H )
4037, 39sseqtr4i 3484 . . . . . . . 8  |-  ( H  X.  H )  C_  dom  +h
41 ssdmres 5227 . . . . . . . 8  |-  ( ( H  X.  H ) 
C_  dom  +h  <->  dom  (  +h  |`  ( H  X.  H
) )  =  ( H  X.  H ) )
4240, 41mpbi 208 . . . . . . 7  |-  dom  (  +h  |`  ( H  X.  H ) )  =  ( H  X.  H
)
4334, 42eqtri 2479 . . . . . 6  |-  dom  ( +v `  W )  =  ( H  X.  H
)
4443dmeqi 5136 . . . . 5  |-  dom  dom  ( +v `  W )  =  dom  ( H  X.  H )
45 dmxpid 5154 . . . . 5  |-  dom  ( H  X.  H )  =  H
4644, 45eqtri 2479 . . . 4  |-  dom  dom  ( +v `  W )  =  H
4712, 46eqtri 2479 . . 3  |-  ran  ( +v `  W )  =  H
483, 47eqtri 2479 . 2  |-  ( BaseSet `  W )  =  H
4948eqcomi 2463 1  |-  H  =  ( BaseSet `  W )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758   _Vcvv 3065    C_ wss 3423   <.cop 3978    X. cxp 4933   dom cdm 4935   ran crn 4936    |` cres 4937   -->wf 5509   ` cfv 5513   1stc1st 6672   CCcc 9378   RRcr 9379   GrpOpcgr 23805   AbelOpcablo 23900   NrmCVeccnv 24094   +vcpv 24095   BaseSetcba 24096   SubSpcss 24251   ~Hchil 24453    +h cva 24454    .h csm 24455   normhcno 24457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4498  ax-sep 4508  ax-nul 4516  ax-pow 4565  ax-pr 4626  ax-un 6469  ax-cnex 9436  ax-resscn 9437  ax-1cn 9438  ax-icn 9439  ax-addcl 9440  ax-addrcl 9441  ax-mulcl 9442  ax-mulrcl 9443  ax-mulcom 9444  ax-addass 9445  ax-mulass 9446  ax-distr 9447  ax-i2m1 9448  ax-1ne0 9449  ax-1rid 9450  ax-rnegex 9451  ax-rrecex 9452  ax-cnre 9453  ax-pre-lttri 9454  ax-pre-lttrn 9455  ax-pre-ltadd 9456  ax-pre-mulgt0 9457  ax-pre-sup 9458  ax-hilex 24533  ax-hfvadd 24534  ax-hvcom 24535  ax-hvass 24536  ax-hv0cl 24537  ax-hvaddid 24538  ax-hfvmul 24539  ax-hvmulid 24540  ax-hvmulass 24541  ax-hvdistr1 24542  ax-hvdistr2 24543  ax-hvmul0 24544  ax-hfi 24613  ax-his1 24616  ax-his2 24617  ax-his3 24618  ax-his4 24619
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-nel 2645  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3067  df-sbc 3282  df-csb 3384  df-dif 3426  df-un 3428  df-in 3430  df-ss 3437  df-pss 3439  df-nul 3733  df-if 3887  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4187  df-iun 4268  df-br 4388  df-opab 4446  df-mpt 4447  df-tr 4481  df-eprel 4727  df-id 4731  df-po 4736  df-so 4737  df-fr 4774  df-we 4776  df-ord 4817  df-on 4818  df-lim 4819  df-suc 4820  df-xp 4941  df-rel 4942  df-cnv 4943  df-co 4944  df-dm 4945  df-rn 4946  df-res 4947  df-ima 4948  df-iota 5476  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6148  df-ov 6190  df-oprab 6191  df-mpt2 6192  df-om 6574  df-1st 6674  df-2nd 6675  df-recs 6929  df-rdg 6963  df-er 7198  df-en 7408  df-dom 7409  df-sdom 7410  df-sup 7789  df-pnf 9518  df-mnf 9519  df-xr 9520  df-ltxr 9521  df-le 9522  df-sub 9695  df-neg 9696  df-div 10092  df-nn 10421  df-2 10478  df-3 10479  df-4 10480  df-n0 10678  df-z 10745  df-uz 10960  df-rp 11090  df-seq 11905  df-exp 11964  df-cj 12687  df-re 12688  df-im 12689  df-sqr 12823  df-abs 12824  df-grpo 23810  df-gid 23811  df-ablo 23901  df-vc 24056  df-nv 24102  df-va 24105  df-ba 24106  df-sm 24107  df-0v 24108  df-nmcv 24110  df-ssp 24252  df-hnorm 24502  df-hvsub 24505
This theorem is referenced by:  hhshsslem2  24801  hhssba  24804
  Copyright terms: Public domain W3C validator