# 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$