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 ⊢ T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ → T ∈ HrmOp

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ T = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → T ∈ HrmOp ↔ if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ∈ HrmOp
2 eleq1 ⊢ T = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → T ∈ LinOp ↔ if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ∈ LinOp
3 id ⊢ x = y → x = y
4 fveq2 ⊢ x = y → T ⁡ x = T ⁡ y
5 3 4 oveq12d ⊢ x = y → x ⋅ ih T ⁡ x = y ⋅ ih T ⁡ y
6 5 eleq1d ⊢ x = y → x ⋅ ih T ⁡ x ∈ ℝ ↔ y ⋅ ih T ⁡ y ∈ ℝ
7 6 cbvralvw ⊢ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ ↔ ∀ y ∈ ℋ y ⋅ ih T ⁡ y ∈ ℝ
8 fveq1 ⊢ T = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → T ⁡ y = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y
9 8 oveq2d ⊢ T = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → y ⋅ ih T ⁡ y = y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y
10 9 eleq1d ⊢ T = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → y ⋅ ih T ⁡ y ∈ ℝ ↔ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
11 10 ralbidv ⊢ T = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → ∀ y ∈ ℋ y ⋅ ih T ⁡ y ∈ ℝ ↔ ∀ y ∈ ℋ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
12 7 11 syl5bb ⊢ T = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ ↔ ∀ y ∈ ℋ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
13 2 12 anbi12d ⊢ T = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ ↔ if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ∈ LinOp ∧ ∀ y ∈ ℋ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
14 eleq1 ⊢ I ↾ ℋ = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → I ↾ ℋ ∈ LinOp ↔ if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ∈ LinOp
15 fveq1 ⊢ I ↾ ℋ = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → I ↾ ℋ ⁡ y = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y
16 15 oveq2d ⊢ I ↾ ℋ = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → y ⋅ ih I ↾ ℋ ⁡ y = y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y
17 16 eleq1d ⊢ I ↾ ℋ = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → y ⋅ ih I ↾ ℋ ⁡ y ∈ ℝ ↔ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
18 17 ralbidv ⊢ I ↾ ℋ = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → ∀ y ∈ ℋ y ⋅ ih I ↾ ℋ ⁡ y ∈ ℝ ↔ ∀ y ∈ ℋ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
19 14 18 anbi12d ⊢ I ↾ ℋ = if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ → I ↾ ℋ ∈ LinOp ∧ ∀ y ∈ ℋ y ⋅ ih I ↾ ℋ ⁡ y ∈ ℝ ↔ if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ∈ LinOp ∧ ∀ y ∈ ℋ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
20 idlnop ⊢ I ↾ ℋ ∈ LinOp
21 fvresi ⊢ y ∈ ℋ → I ↾ ℋ ⁡ y = y
22 21 oveq2d ⊢ y ∈ ℋ → y ⋅ ih I ↾ ℋ ⁡ y = y ⋅ ih y
23 hiidrcl ⊢ y ∈ ℋ → y ⋅ ih y ∈ ℝ
24 22 23 eqeltrd ⊢ y ∈ ℋ → y ⋅ ih I ↾ ℋ ⁡ y ∈ ℝ
25 24 rgen ⊢ ∀ y ∈ ℋ y ⋅ ih I ↾ ℋ ⁡ y ∈ ℝ
26 20 25 pm3.2i ⊢ I ↾ ℋ ∈ LinOp ∧ ∀ y ∈ ℋ y ⋅ ih I ↾ ℋ ⁡ y ∈ ℝ
27 13 19 26 elimhyp ⊢ if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ∈ LinOp ∧ ∀ y ∈ ℋ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
28 27 simpli ⊢ if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ∈ LinOp
29 27 simpri ⊢ ∀ y ∈ ℋ y ⋅ ih if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ⁡ y ∈ ℝ
30 28 29 lnophmi ⊢ if T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ T I ↾ ℋ ∈ HrmOp
31 1 30 dedth ⊢ T ∈ LinOp ∧ ∀ x ∈ ℋ x ⋅ ih T ⁡ x ∈ ℝ → T ∈ HrmOp