Metamath Proof Explorer

Theorem hoeq

Description: Equality of Hilbert space operators. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoeq ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ → ∀ x ∈ ℋ T ⁡ x = U ⁡ x ↔ T = U

Proof

Step Hyp Ref Expression
1 ffn ⊢ T : ℋ ⟶ ℋ → T Fn ℋ
2 ffn ⊢ U : ℋ ⟶ ℋ → U Fn ℋ
3 eqfnfv ⊢ T Fn ℋ ∧ U Fn ℋ → T = U ↔ ∀ x ∈ ℋ T ⁡ x = U ⁡ x
4 3 bicomd ⊢ T Fn ℋ ∧ U Fn ℋ → ∀ x ∈ ℋ T ⁡ x = U ⁡ x ↔ T = U
5 1 2 4 syl2an ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ → ∀ x ∈ ℋ T ⁡ x = U ⁡ x ↔ T = U