Theorem hoeqi

Description: Equality of Hilbert space operators. (Contributed by NM, 14-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hoeqi	$$⊢\forall x\in \mathscr{H}S\left(x\right)=T\left(x\right)\leftrightarrow S=T$$

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
2		hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
3		hoeq	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(\forall x\in \mathscr{H}S\left(x\right)=T\left(x\right)\leftrightarrow S=T\right)$$
4	1 2 3	mp2an	$$⊢\forall x\in \mathscr{H}S\left(x\right)=T\left(x\right)\leftrightarrow S=T$$