Metamath Proof Explorer

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 ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ S ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y ↔ S = T

Proof

Step Hyp Ref Expression
1 ffvelrn ⊢ S : ℋ ⟶ ℋ ∧ x ∈ ℋ → S ⁡ x ∈ ℋ
2 ffvelrn ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
3 hial2eq ⊢ S ⁡ x ∈ ℋ ∧ T ⁡ x ∈ ℋ → ∀ y ∈ ℋ S ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y ↔ S ⁡ x = T ⁡ x
4 1 2 3 syl2an ⊢ S : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → ∀ y ∈ ℋ S ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y ↔ S ⁡ x = T ⁡ x
5 4 anandirs ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → ∀ y ∈ ℋ S ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y ↔ S ⁡ x = T ⁡ x
6 5 ralbidva ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ S ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ S ⁡ x = T ⁡ x
7 ffn ⊢ S : ℋ ⟶ ℋ → S Fn ℋ
8 ffn ⊢ T : ℋ ⟶ ℋ → T Fn ℋ
9 eqfnfv ⊢ S Fn ℋ ∧ T Fn ℋ → S = T ↔ ∀ x ∈ ℋ S ⁡ x = T ⁡ x
10 7 8 9 syl2an ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → S = T ↔ ∀ x ∈ ℋ S ⁡ x = T ⁡ x
11 6 10 bitr4d ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ S ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y ↔ S = T