Theorem ho01i

Description: A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) 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	ho01i	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=0\leftrightarrow T=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		ho0.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2		ffn	$$⊢T:\mathscr{H}⟶\mathscr{H}\to TFn\mathscr{H}$$
3	1 2	ax-mp	$$⊢TFn\mathscr{H}$$
4		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
5	4	elexi	$$⊢0_{ℎ}\in \mathrm{V}$$
6	5	fconst	$$⊢\left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right):\mathscr{H}⟶\left\{0_{ℎ}\right\}$$
7		ffn	$$⊢\left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right):\mathscr{H}⟶\left\{0_{ℎ}\right\}\to \left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)Fn\mathscr{H}$$
8	6 7	ax-mp	$$⊢\left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)Fn\mathscr{H}$$
9		eqfnfv	$$⊢\left(TFn\mathscr{H}\wedge \left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)Fn\mathscr{H}\right)\to \left(T=\mathscr{H}\times \left\{0_{ℎ}\right\}\leftrightarrow \forall x\in \mathscr{H}T\left(x\right)=\left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)\left(x\right)\right)$$
10	3 8 9	mp2an	$$⊢T=\mathscr{H}\times \left\{0_{ℎ}\right\}\leftrightarrow \forall x\in \mathscr{H}T\left(x\right)=\left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)\left(x\right)$$
11		df0op2	$$⊢0_{\mathrm{hop}}=\mathscr{H}\times 0_{\mathscr{H}}$$
12		df-ch0	$$⊢0_{\mathscr{H}}=\left\{0_{ℎ}\right\}$$
13	12	xpeq2i	$$⊢\mathscr{H}\times 0_{\mathscr{H}}=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
14	11 13	eqtri	$$⊢0_{\mathrm{hop}}=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
15	14	eqeq2i	$$⊢T=0_{\mathrm{hop}}\leftrightarrow T=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
16	1	ffvelrni	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
17		hial0	$$⊢T\left(x\right)\in \mathscr{H}\to \left(\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=0\leftrightarrow T\left(x\right)=0_{ℎ}\right)$$
18	16 17	syl	$$⊢x\in \mathscr{H}\to \left(\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=0\leftrightarrow T\left(x\right)=0_{ℎ}\right)$$
19	5	fvconst2	$$⊢x\in \mathscr{H}\to \left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)\left(x\right)=0_{ℎ}$$
20	19	eqeq2d	$$⊢x\in \mathscr{H}\to \left(T\left(x\right)=\left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)\left(x\right)\leftrightarrow T\left(x\right)=0_{ℎ}\right)$$
21	18 20	bitr4d	$$⊢x\in \mathscr{H}\to \left(\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=0\leftrightarrow T\left(x\right)=\left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)\left(x\right)\right)$$
22	21	ralbiia	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=0\leftrightarrow \forall x\in \mathscr{H}T\left(x\right)=\left(\mathscr{H}\times \left\{0_{ℎ}\right\}\right)\left(x\right)$$
23	10 15 22	3bitr4ri	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=0\leftrightarrow T=0_{\mathrm{hop}}$$