# Metamath Proof Explorer

## Theorem lnophm

Description: A linear operator is Hermitian if x .ih ( Tx ) takes only real values. Remark in ReedSimon p. 195. (Contributed by NM, 24-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion lnophm ${⊢}\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right)\to {T}\in \mathrm{HrmOp}$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({T}\in \mathrm{HrmOp}↔if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{HrmOp}\right)$
2 eleq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({T}\in \mathrm{LinOp}↔if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\right)$
3 id ${⊢}{x}={y}\to {x}={y}$
4 fveq2 ${⊢}{x}={y}\to {T}\left({x}\right)={T}\left({y}\right)$
5 3 4 oveq12d ${⊢}{x}={y}\to {x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)={y}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)$
6 5 eleq1d ${⊢}{x}={y}\to \left({x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ↔{y}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\in ℝ\right)$
7 6 cbvralvw ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\in ℝ$
8 fveq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to {T}\left({y}\right)=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)$
9 8 oveq2d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to {y}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)$
10 9 eleq1d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({y}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\in ℝ↔{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)$
11 10 ralbidv ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\in ℝ↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)$
12 7 11 syl5bb ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)$
13 2 12 anbi12d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right)↔\left(if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)\right)$
14 eleq1 ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}↔if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\right)$
15 fveq1 ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)$
16 15 oveq2d ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to {y}{\cdot }_{\mathrm{ih}}\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)={y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)$
17 16 eleq1d ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({y}{\cdot }_{\mathrm{ih}}\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ↔{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)$
18 17 ralbidv ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)$
19 14 18 anbi12d ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\left({\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)↔\left(if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)\right)$
20 idlnop ${⊢}{\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}$
21 fvresi ${⊢}{y}\in ℋ\to \left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)={y}$
22 21 oveq2d ${⊢}{y}\in ℋ\to {y}{\cdot }_{\mathrm{ih}}\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)={y}{\cdot }_{\mathrm{ih}}{y}$
23 hiidrcl ${⊢}{y}\in ℋ\to {y}{\cdot }_{\mathrm{ih}}{y}\in ℝ$
24 22 23 eqeltrd ${⊢}{y}\in ℋ\to {y}{\cdot }_{\mathrm{ih}}\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ$
25 24 rgen ${⊢}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ$
26 20 25 pm3.2i ${⊢}\left({\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)$
27 13 19 26 elimhyp ${⊢}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ\right)$
28 27 simpli ${⊢}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}$
29 27 simpri ${⊢}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\in ℝ$
30 28 29 lnophmi ${⊢}if\left(\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{HrmOp}$
31 1 30 dedth ${⊢}\left({T}\in \mathrm{LinOp}\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({x}\right)\in ℝ\right)\to {T}\in \mathrm{HrmOp}$