Theorem hoeq

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

	Ref	Expression
Assertion	hoeq	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑈 ‘ 𝑥 ) ↔ 𝑇 = 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
2		ffn	⊢ ( 𝑈 : ℋ ⟶ ℋ → 𝑈 Fn ℋ )
3		eqfnfv	⊢ ( ( 𝑇 Fn ℋ ∧ 𝑈 Fn ℋ ) → ( 𝑇 = 𝑈 ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑈 ‘ 𝑥 ) ) )
4	3	bicomd	⊢ ( ( 𝑇 Fn ℋ ∧ 𝑈 Fn ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑈 ‘ 𝑥 ) ↔ 𝑇 = 𝑈 ) )
5	1 2 4	syl2an	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑈 ‘ 𝑥 ) ↔ 𝑇 = 𝑈 ) )