Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > lnophmi | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
lnophm.1 | ⊢ 𝑇 ∈ LinOp |
lnophm.2 | ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ |
Ref | Expression |
---|---|
lnophmi | ⊢ 𝑇 ∈ HrmOp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lnophm.1 | . . 3 ⊢ 𝑇 ∈ LinOp | |
2 | 1 | lnopfi 30079 | . 2 ⊢ 𝑇: ℋ⟶ ℋ |
3 | oveq1 7241 | . . . . 5 ⊢ (𝑦 = if(𝑦 ∈ ℋ, 𝑦, 0ℎ) → (𝑦 ·ih (𝑇‘𝑧)) = (if(𝑦 ∈ ℋ, 𝑦, 0ℎ) ·ih (𝑇‘𝑧))) | |
4 | fveq2 6738 | . . . . . 6 ⊢ (𝑦 = if(𝑦 ∈ ℋ, 𝑦, 0ℎ) → (𝑇‘𝑦) = (𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0ℎ))) | |
5 | 4 | oveq1d 7249 | . . . . 5 ⊢ (𝑦 = if(𝑦 ∈ ℋ, 𝑦, 0ℎ) → ((𝑇‘𝑦) ·ih 𝑧) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0ℎ)) ·ih 𝑧)) |
6 | 3, 5 | eqeq12d 2755 | . . . 4 ⊢ (𝑦 = if(𝑦 ∈ ℋ, 𝑦, 0ℎ) → ((𝑦 ·ih (𝑇‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) ↔ (if(𝑦 ∈ ℋ, 𝑦, 0ℎ) ·ih (𝑇‘𝑧)) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0ℎ)) ·ih 𝑧))) |
7 | fveq2 6738 | . . . . . 6 ⊢ (𝑧 = if(𝑧 ∈ ℋ, 𝑧, 0ℎ) → (𝑇‘𝑧) = (𝑇‘if(𝑧 ∈ ℋ, 𝑧, 0ℎ))) | |
8 | 7 | oveq2d 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ℎ))) | |
10 | 8, 9 | eqeq12d 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 (𝑇‘𝑥)) ∈ ℝ | |
14 | 11, 12, 1, 13 | lnophmlem2 30127 | . . . 4 ⊢ (if(𝑦 ∈ ℋ, 𝑦, 0ℎ) ·ih (𝑇‘if(𝑧 ∈ ℋ, 𝑧, 0ℎ))) = ((𝑇‘if(𝑦 ∈ ℋ, 𝑦, 0ℎ)) ·ih if(𝑧 ∈ ℋ, 𝑧, 0ℎ)) |
15 | 6, 10, 14 | dedth2h 4514 | . . 3 ⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 ·ih (𝑇‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧)) |
16 | 15 | rgen2 3126 | . 2 ⊢ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑦 ·ih (𝑇‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧) |
17 | elhmop 29983 | . 2 ⊢ (𝑇 ∈ HrmOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑦 ·ih (𝑇‘𝑧)) = ((𝑇‘𝑦) ·ih 𝑧))) | |
18 | 2, 16, 17 | mpbir2an 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 0ℎc0v 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 |