Metamath Proof Explorer

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

Proof

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