Theorem hoeq1

Description: A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of Beran p. 95. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoeq1	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ 𝑆 = 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		ffvelcdm	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
2		ffvelcdm	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
3		hial2eq	⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑆 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ) )
4	1 2 3	syl2an	⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ∀ 𝑦 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑆 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ) )
5	4	anandirs	⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑆 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ) )
6	5	ralbidva	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑆 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ) )
7		ffn	⊢ ( 𝑆 : ℋ ⟶ ℋ → 𝑆 Fn ℋ )
8		ffn	⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
9		eqfnfv	⊢ ( ( 𝑆 Fn ℋ ∧ 𝑇 Fn ℋ ) → ( 𝑆 = 𝑇 ↔ ∀ 𝑥 ∈ ℋ ( 𝑆 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ) )
10	7 8 9	syl2an	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 = 𝑇 ↔ ∀ 𝑥 ∈ ℋ ( 𝑆 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ) )
11	6 10	bitr4d	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ 𝑆 = 𝑇 ) )