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⋅ihy=T⁡x⋅ihy↔S=T

Proof

Step Hyp Ref Expression
1 ffvelcdm ⊢S:ℋ⟶ℋ∧x∈ℋ→S⁡x∈ℋ
2 ffvelcdm ⊢T:ℋ⟶ℋ∧x∈ℋ→T⁡x∈ℋ
3 hial2eq ⊢S⁡x∈ℋ∧T⁡x∈ℋ→∀y∈ℋS⁡x⋅ihy=T⁡x⋅ihy↔S⁡x=T⁡x
4 1 2 3 syl2an ⊢S:ℋ⟶ℋ∧x∈ℋ∧T:ℋ⟶ℋ∧x∈ℋ→∀y∈ℋS⁡x⋅ihy=T⁡x⋅ihy↔S⁡x=T⁡x
5 4 anandirs ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ∧x∈ℋ→∀y∈ℋS⁡x⋅ihy=T⁡x⋅ihy↔S⁡x=T⁡x
6 5 ralbidva ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋS⁡x⋅ihy=T⁡x⋅ihy↔∀x∈ℋS⁡x=T⁡x
7 ffn ⊢S:ℋ⟶ℋ→SFnℋ
8 ffn ⊢T:ℋ⟶ℋ→TFnℋ
9 eqfnfv ⊢SFnℋ∧TFnℋ→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⋅ihy=T⁡x⋅ihy↔S=T