Theorem ho02i

Description: A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of Beran p. 95. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ho0.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	ho02i	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=0\leftrightarrow T=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		ho0.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2		ralcom	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=0\leftrightarrow \forall y\in \mathscr{H}\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=0$$
3	1	ffvelcdmi	$$⊢y\in \mathscr{H}\to T\left(y\right)\in \mathscr{H}$$
4		hial02	$$⊢T\left(y\right)\in \mathscr{H}\to \left(\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=0\leftrightarrow T\left(y\right)=0_{ℎ}\right)$$
5		hial0	$$⊢T\left(y\right)\in \mathscr{H}\to \left(\forall x\in \mathscr{H}T\left(y\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T\left(y\right)=0_{ℎ}\right)$$
6	4 5	bitr4d	$$⊢T\left(y\right)\in \mathscr{H}\to \left(\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=0\leftrightarrow \forall x\in \mathscr{H}T\left(y\right){\cdot }_{\mathrm{ih}}x=0\right)$$
7	3 6	syl	$$⊢y\in \mathscr{H}\to \left(\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=0\leftrightarrow \forall x\in \mathscr{H}T\left(y\right){\cdot }_{\mathrm{ih}}x=0\right)$$
8	7	ralbiia	$$⊢\forall y\in \mathscr{H}\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=0\leftrightarrow \forall y\in \mathscr{H}\forall x\in \mathscr{H}T\left(y\right){\cdot }_{\mathrm{ih}}x=0$$
9	1	ho01i	$$⊢\forall y\in \mathscr{H}\forall x\in \mathscr{H}T\left(y\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T=0_{\mathrm{hop}}$$
10	2 8 9	3bitri	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=0\leftrightarrow T=0_{\mathrm{hop}}$$