HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  lnophmi Structured version   Visualization version   GIF version

Theorem lnophmi 30128
Description: A linear operator is Hermitian if 𝑥 ·ih (𝑇𝑥) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
lnophm.1 𝑇 ∈ LinOp
lnophm.2 𝑥 ∈ ℋ (𝑥 ·ih (𝑇𝑥)) ∈ ℝ
Assertion
Ref Expression
lnophmi 𝑇 ∈ HrmOp
Distinct variable group:   𝑥,𝑇

Proof of Theorem lnophmi
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lnophm.1 . . 3 𝑇 ∈ LinOp
21lnopfi 30079 . 2 𝑇: ℋ⟶ ℋ
3 oveq1 7241 . . . . 5 (𝑦 = if(𝑦 ∈ ℋ, 𝑦, 0) → (𝑦 ·ih (𝑇𝑧)) = (if(𝑦 ∈ ℋ, 𝑦, 0) ·ih (𝑇𝑧)))
4 fveq2 6738 . . . . . 6 (𝑦 = if(𝑦 ∈ ℋ, 𝑦, 0) → (𝑇𝑦) = (𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0)))
54oveq1d 7249 . . . . 5 (𝑦 = if(𝑦 ∈ ℋ, 𝑦, 0) → ((𝑇𝑦) ·ih 𝑧) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0)) ·ih 𝑧))
63, 5eqeq12d 2755 . . . 4 (𝑦 = if(𝑦 ∈ ℋ, 𝑦, 0) → ((𝑦 ·ih (𝑇𝑧)) = ((𝑇𝑦) ·ih 𝑧) ↔ (if(𝑦 ∈ ℋ, 𝑦, 0) ·ih (𝑇𝑧)) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0)) ·ih 𝑧)))
7 fveq2 6738 . . . . . 6 (𝑧 = if(𝑧 ∈ ℋ, 𝑧, 0) → (𝑇𝑧) = (𝑇‘if(𝑧 ∈ ℋ, 𝑧, 0)))
87oveq2d 7250 . . . . 5 (𝑧 = if(𝑧 ∈ ℋ, 𝑧, 0) → (if(𝑦 ∈ ℋ, 𝑦, 0) ·ih (𝑇𝑧)) = (if(𝑦 ∈ ℋ, 𝑦, 0) ·ih (𝑇‘if(𝑧 ∈ ℋ, 𝑧, 0))))
9 oveq2 7242 . . . . 5 (𝑧 = if(𝑧 ∈ ℋ, 𝑧, 0) → ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0)) ·ih 𝑧) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0)) ·ih if(𝑧 ∈ ℋ, 𝑧, 0)))
108, 9eqeq12d 2755 . . . 4 (𝑧 = if(𝑧 ∈ ℋ, 𝑧, 0) → ((if(𝑦 ∈ ℋ, 𝑦, 0) ·ih (𝑇𝑧)) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0)) ·ih 𝑧) ↔ (if(𝑦 ∈ ℋ, 𝑦, 0) ·ih (𝑇‘if(𝑧 ∈ ℋ, 𝑧, 0))) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0)) ·ih if(𝑧 ∈ ℋ, 𝑧, 0))))
11 ifhvhv0 29132 . . . . 5 if(𝑦 ∈ ℋ, 𝑦, 0) ∈ ℋ
12 ifhvhv0 29132 . . . . 5 if(𝑧 ∈ ℋ, 𝑧, 0) ∈ ℋ
13 lnophm.2 . . . . 5 𝑥 ∈ ℋ (𝑥 ·ih (𝑇𝑥)) ∈ ℝ
1411, 12, 1, 13lnophmlem2 30127 . . . 4 (if(𝑦 ∈ ℋ, 𝑦, 0) ·ih (𝑇‘if(𝑧 ∈ ℋ, 𝑧, 0))) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0)) ·ih if(𝑧 ∈ ℋ, 𝑧, 0))
156, 10, 14dedth2h 4514 . . 3 ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 ·ih (𝑇𝑧)) = ((𝑇𝑦) ·ih 𝑧))
1615rgen2 3126 . 2 𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑦 ·ih (𝑇𝑧)) = ((𝑇𝑦) ·ih 𝑧)
17 elhmop 29983 . 2 (𝑇 ∈ HrmOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑦 ·ih (𝑇𝑧)) = ((𝑇𝑦) ·ih 𝑧)))
182, 16, 17mpbir2an 711 1 𝑇 ∈ HrmOp
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wcel 2112  wral 3063  ifcif 4455  wf 6396  cfv 6400  (class class class)co 7234  cr 10755  chba 29029   ·ih csp 29032  0c0v 29034  LinOpclo 29057  HrmOpcho 29060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-resscn 10813  ax-1cn 10814  ax-icn 10815  ax-addcl 10816  ax-addrcl 10817  ax-mulcl 10818  ax-mulrcl 10819  ax-mulcom 10820  ax-addass 10821  ax-mulass 10822  ax-distr 10823  ax-i2m1 10824  ax-1ne0 10825  ax-1rid 10826  ax-rnegex 10827  ax-rrecex 10828  ax-cnre 10829  ax-pre-lttri 10830  ax-pre-lttrn 10831  ax-pre-ltadd 10832  ax-pre-mulgt0 10833  ax-hilex 29109  ax-hfvadd 29110  ax-hvcom 29111  ax-hvass 29112  ax-hv0cl 29113  ax-hvaddid 29114  ax-hfvmul 29115  ax-hvmulid 29116  ax-hvmulass 29117  ax-hvdistr1 29118  ax-hvdistr2 29119  ax-hvmul0 29120  ax-hfi 29189  ax-his1 29192  ax-his2 29193  ax-his3 29194
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3711  df-csb 3828  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-id 5471  df-po 5485  df-so 5486  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-er 8414  df-map 8533  df-en 8650  df-dom 8651  df-sdom 8652  df-pnf 10896  df-mnf 10897  df-xr 10898  df-ltxr 10899  df-le 10900  df-sub 11091  df-neg 11092  df-div 11517  df-2 11920  df-3 11921  df-4 11922  df-cj 14692  df-re 14693  df-im 14694  df-hvsub 29081  df-lnop 29951  df-hmop 29954
This theorem is referenced by:  lnophm  30129
  Copyright terms: Public domain W3C validator