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