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⋅ihS⁡y=x⋅ihT⁡y↔S=T

Proof

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