Metamath Proof Explorer

Theorem elhmop

Description: Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion elhmop ⊢ T ∈ HrmOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ t = T → t ⁡ y = T ⁡ y
2 1 oveq2d ⊢ t = T → x ⋅ ih t ⁡ y = x ⋅ ih T ⁡ y
3 fveq1 ⊢ t = T → t ⁡ x = T ⁡ x
4 3 oveq1d ⊢ t = T → t ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y
5 2 4 eqeq12d ⊢ t = T → x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y ↔ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
6 5 2ralbidv ⊢ t = T → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
7 df-hmop ⊢ HrmOp = t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y
8 6 7 elrab2 ⊢ T ∈ HrmOp ↔ T ∈ ℋ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
9 ax-hilex ⊢ ℋ ∈ V
10 9 9 elmap ⊢ T ∈ ℋ ℋ ↔ T : ℋ ⟶ ℋ
11 10 anbi1i ⊢ T ∈ ℋ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
12 8 11 bitri ⊢ T ∈ HrmOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y