Theorem hoeq

Description: Equality of Hilbert space operators. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoeq	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(\forall x\in \mathscr{H}T\left(x\right)=U\left(x\right)\leftrightarrow T=U\right)$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢T:\mathscr{H}⟶\mathscr{H}\to TFn\mathscr{H}$$
2		ffn	$$⊢U:\mathscr{H}⟶\mathscr{H}\to UFn\mathscr{H}$$
3		eqfnfv	$$⊢\left(TFn\mathscr{H}\wedge UFn\mathscr{H}\right)\to \left(T=U\leftrightarrow \forall x\in \mathscr{H}T\left(x\right)=U\left(x\right)\right)$$
4	3	bicomd	$$⊢\left(TFn\mathscr{H}\wedge UFn\mathscr{H}\right)\to \left(\forall x\in \mathscr{H}T\left(x\right)=U\left(x\right)\leftrightarrow T=U\right)$$
5	1 2 4	syl2an	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(\forall x\in \mathscr{H}T\left(x\right)=U\left(x\right)\leftrightarrow T=U\right)$$