# 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 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔{S}={T}\right)$

### Proof

Step Hyp Ref Expression
1 ralcom ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)$
2 1 a1i ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)$
3 ffvelrn ${⊢}\left({S}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to {S}\left({y}\right)\in ℋ$
4 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to {T}\left({y}\right)\in ℋ$
5 hial2eq2 ${⊢}\left({S}\left({y}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔{S}\left({y}\right)={T}\left({y}\right)\right)$
6 hial2eq ${⊢}\left({S}\left({y}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{S}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={T}\left({y}\right){\cdot }_{\mathrm{ih}}{x}↔{S}\left({y}\right)={T}\left({y}\right)\right)$
7 5 6 bitr4d ${⊢}\left({S}\left({y}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{S}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={T}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
8 3 4 7 syl2an ${⊢}\left(\left({S}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\wedge \left({T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{S}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={T}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
9 8 anandirs ${⊢}\left(\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\wedge {y}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{S}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={T}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
10 9 ralbidva ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{S}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={T}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
11 hoeq1 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{S}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={T}\left({y}\right){\cdot }_{\mathrm{ih}}{x}↔{S}={T}\right)$
12 2 10 11 3bitrd ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)↔{S}={T}\right)$