HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  lnophm Structured version   Visualization version   GIF version
Theorem lnophm 31527
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.)
Assertion
Ref Expression
lnophm ((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„) โ†’ ๐‘‡ โˆˆ HrmOp)
Distinct variable group:   ๐‘ฅ,๐‘‡
Proof of Theorem lnophm
Dummy variable ๐‘ฆ is distinct from all other variables.
StepHypRef Expression
1 eleq1 2821 . 2 (๐‘‡ = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (๐‘‡ โˆˆ HrmOp โ†” if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โˆˆ HrmOp))
2 eleq1 2821 . . . . . 6 (๐‘‡ = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (๐‘‡ โˆˆ LinOp โ†” if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โˆˆ LinOp))
3 id 22 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ ๐‘ฅ = ๐‘ฆ)
4 fveq2 6891 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘‡โ€˜๐‘ฅ) = (๐‘‡โ€˜๐‘ฆ))
53, 4oveq12d 7429 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) = (๐‘ฆ ยทih (๐‘‡โ€˜๐‘ฆ)))
65eleq1d 2818 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„ โ†” (๐‘ฆ ยทih (๐‘‡โ€˜๐‘ฆ)) โˆˆ โ„))
76cbvralvw 3234 . . . . . . 7 (โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„ โ†” โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (๐‘‡โ€˜๐‘ฆ)) โˆˆ โ„)
8 fveq1 6890 . . . . . . . . . 10 (๐‘‡ = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (๐‘‡โ€˜๐‘ฆ) = (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ))
98oveq2d 7427 . . . . . . . . 9 (๐‘‡ = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (๐‘ฆ ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)))
109eleq1d 2818 . . . . . . . 8 (๐‘‡ = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ ((๐‘ฆ ยทih (๐‘‡โ€˜๐‘ฆ)) โˆˆ โ„ โ†” (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„))
1110ralbidv 3177 . . . . . . 7 (๐‘‡ = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (๐‘‡โ€˜๐‘ฆ)) โˆˆ โ„ โ†” โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„))
127, 11bitrid 282 . . . . . 6 (๐‘‡ = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„ โ†” โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„))
132, 12anbi12d 631 . . . . 5 (๐‘‡ = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ ((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„) โ†” (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โˆˆ LinOp โˆง โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„)))
14 eleq1 2821 . . . . . 6 (( I โ†พ โ„‹) = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (( I โ†พ โ„‹) โˆˆ LinOp โ†” if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โˆˆ LinOp))
15 fveq1 6890 . . . . . . . . 9 (( I โ†พ โ„‹) = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (( I โ†พ โ„‹)โ€˜๐‘ฆ) = (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ))
1615oveq2d 7427 . . . . . . . 8 (( I โ†พ โ„‹) = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (๐‘ฆ ยทih (( I โ†พ โ„‹)โ€˜๐‘ฆ)) = (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)))
1716eleq1d 2818 . . . . . . 7 (( I โ†พ โ„‹) = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ ((๐‘ฆ ยทih (( I โ†พ โ„‹)โ€˜๐‘ฆ)) โˆˆ โ„ โ†” (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„))
1817ralbidv 3177 . . . . . 6 (( I โ†พ โ„‹) = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ (โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (( I โ†พ โ„‹)โ€˜๐‘ฆ)) โˆˆ โ„ โ†” โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„))
1914, 18anbi12d 631 . . . . 5 (( I โ†พ โ„‹) = if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โ†’ ((( I โ†พ โ„‹) โˆˆ LinOp โˆง โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (( I โ†พ โ„‹)โ€˜๐‘ฆ)) โˆˆ โ„) โ†” (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โˆˆ LinOp โˆง โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„)))
20 idlnop 31500 . . . . . 6 ( I โ†พ โ„‹) โˆˆ LinOp
21 fvresi 7173 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„‹ โ†’ (( I โ†พ โ„‹)โ€˜๐‘ฆ) = ๐‘ฆ)
2221oveq2d 7427 . . . . . . . 8 (๐‘ฆ โˆˆ โ„‹ โ†’ (๐‘ฆ ยทih (( I โ†พ โ„‹)โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ))
23 hiidrcl 30603 . . . . . . . 8 (๐‘ฆ โˆˆ โ„‹ โ†’ (๐‘ฆ ยทih ๐‘ฆ) โˆˆ โ„)
2422, 23eqeltrd 2833 . . . . . . 7 (๐‘ฆ โˆˆ โ„‹ โ†’ (๐‘ฆ ยทih (( I โ†พ โ„‹)โ€˜๐‘ฆ)) โˆˆ โ„)
2524rgen 3063 . . . . . 6 โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (( I โ†พ โ„‹)โ€˜๐‘ฆ)) โˆˆ โ„
2620, 25pm3.2i 471 . . . . 5 (( I โ†พ โ„‹) โˆˆ LinOp โˆง โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (( I โ†พ โ„‹)โ€˜๐‘ฆ)) โˆˆ โ„)
2713, 19, 26elimhyp 4593 . . . 4 (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โˆˆ LinOp โˆง โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„)
2827simpli 484 . . 3 if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โˆˆ LinOp
2927simpri 486 . . 3 โˆ€๐‘ฆ โˆˆ โ„‹ (๐‘ฆ ยทih (if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹))โ€˜๐‘ฆ)) โˆˆ โ„
3028, 29lnophmi 31526 . 2 if((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„), ๐‘‡, ( I โ†พ โ„‹)) โˆˆ HrmOp
311, 30dedth 4586 1 ((๐‘‡ โˆˆ LinOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ (๐‘ฅ ยทih (๐‘‡โ€˜๐‘ฅ)) โˆˆ โ„) โ†’ ๐‘‡ โˆˆ HrmOp)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3061  ifcif 4528   I cid 5573   โ†พ cres 5678  โ€˜cfv 6543  (class class class)co 7411  โ„cr 11111   โ„‹chba 30427   ยทih csp 30430  LinOpclo 30455  HrmOpcho 30458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-hilex 30507  ax-hfvadd 30508  ax-hvcom 30509  ax-hvass 30510  ax-hv0cl 30511  ax-hvaddid 30512  ax-hfvmul 30513  ax-hvmulid 30514  ax-hvmulass 30515  ax-hvdistr1 30516  ax-hvdistr2 30517  ax-hvmul0 30518  ax-hfi 30587  ax-his1 30590  ax-his2 30591  ax-his3 30592  ax-his4 30593
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-2 12279  df-3 12280  df-4 12281  df-cj 15050  df-re 15051  df-im 15052  df-hvsub 30479  df-lnop 31349  df-unop 31351  df-hmop 31352
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator