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⋅ihT⁡y=T⁡x⋅ihy

Proof

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