# Metamath Proof Explorer

## Theorem lnophmi

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
Hypotheses lnophm.1 $⊢ T ∈ LinOp$
lnophm.2 $⊢ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ$
Assertion lnophmi $⊢ T ∈ HrmOp$

### Proof

Step Hyp Ref Expression
1 lnophm.1 $⊢ T ∈ LinOp$
2 lnophm.2 $⊢ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ$
3 1 lnopfi $⊢ T : ℋ ⟶ ℋ$
4 oveq1 $⊢ y = if y ∈ ℋ y 0 ℎ → y ⋅ ih T ⁡ z = if y ∈ ℋ y 0 ℎ ⋅ ih T ⁡ z$
5 fveq2 $⊢ y = if y ∈ ℋ y 0 ℎ → T ⁡ y = T ⁡ if y ∈ ℋ y 0 ℎ$
6 5 oveq1d $⊢ y = if y ∈ ℋ y 0 ℎ → T ⁡ y ⋅ ih z = T ⁡ if y ∈ ℋ y 0 ℎ ⋅ ih z$
7 4 6 eqeq12d $⊢ y = if y ∈ ℋ y 0 ℎ → y ⋅ ih T ⁡ z = T ⁡ y ⋅ ih z ↔ if y ∈ ℋ y 0 ℎ ⋅ ih T ⁡ z = T ⁡ if y ∈ ℋ y 0 ℎ ⋅ ih z$
8 fveq2 $⊢ z = if z ∈ ℋ z 0 ℎ → T ⁡ z = T ⁡ if z ∈ ℋ z 0 ℎ$
9 8 oveq2d $⊢ z = if z ∈ ℋ z 0 ℎ → if y ∈ ℋ y 0 ℎ ⋅ ih T ⁡ z = if y ∈ ℋ y 0 ℎ ⋅ ih T ⁡ if z ∈ ℋ z 0 ℎ$
10 oveq2 $⊢ z = if z ∈ ℋ z 0 ℎ → T ⁡ if y ∈ ℋ y 0 ℎ ⋅ ih z = T ⁡ if y ∈ ℋ y 0 ℎ ⋅ ih if z ∈ ℋ z 0 ℎ$
11 9 10 eqeq12d $⊢ z = if z ∈ ℋ z 0 ℎ → if y ∈ ℋ y 0 ℎ ⋅ ih T ⁡ z = T ⁡ if y ∈ ℋ y 0 ℎ ⋅ ih z ↔ if y ∈ ℋ y 0 ℎ ⋅ ih T ⁡ if z ∈ ℋ z 0 ℎ = T ⁡ if y ∈ ℋ y 0 ℎ ⋅ ih if z ∈ ℋ z 0 ℎ$
12 ifhvhv0 $⊢ if y ∈ ℋ y 0 ℎ ∈ ℋ$
13 ifhvhv0 $⊢ if z ∈ ℋ z 0 ℎ ∈ ℋ$
14 12 13 1 2 lnophmlem2 $⊢ if y ∈ ℋ y 0 ℎ ⋅ ih T ⁡ if z ∈ ℋ z 0 ℎ = T ⁡ if y ∈ ℋ y 0 ℎ ⋅ ih if z ∈ ℋ z 0 ℎ$
15 7 11 14 dedth2h $⊢ y ∈ ℋ ∧ z ∈ ℋ → y ⋅ ih T ⁡ z = T ⁡ y ⋅ ih z$
16 15 rgen2 $⊢ ∀ y ∈ ℋ ∀ z ∈ ℋ y ⋅ ih T ⁡ z = T ⁡ y ⋅ ih z$
17 elhmop $⊢ T ∈ HrmOp ↔ T : ℋ ⟶ ℋ ∧ ∀ y ∈ ℋ ∀ z ∈ ℋ y ⋅ ih T ⁡ z = T ⁡ y ⋅ ih z$
18 3 16 17 mpbir2an $⊢ T ∈ HrmOp$