Theorem hoeq2

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

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

Proof

Step	Hyp	Ref	Expression
1		ralcom	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) )
2	1	a1i	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) )
3		ffvelrn	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑆 ‘ 𝑦 ) ∈ ℋ )
4		ffvelrn	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
5		hial2eq2	⊢ ( ( ( 𝑆 ‘ 𝑦 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) )
6		hial2eq	⊢ ( ( ( 𝑆 ‘ 𝑦 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑦 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ↔ ( 𝑆 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) )
7	5 6	bitr4d	⊢ ( ( ( 𝑆 ‘ 𝑦 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑦 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) )
8	3 4 7	syl2an	⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑦 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) )
9	8	anandirs	⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑦 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) )
10	9	ralbidva	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑦 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ) )
11		hoeq1	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑦 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) ↔ 𝑆 = 𝑇 ) )
12	2 10 11	3bitrd	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ↔ 𝑆 = 𝑇 ) )