Theorem lnopeq0i

Description: A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form ( Tx ) .ih x ) . (Contributed by NM, 26-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnopeq0.1	$$⊢T\in \mathrm{LinOp}$$
Assertion	lnopeq0i	$$⊢\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		lnopeq0.1	$$⊢T\in \mathrm{LinOp}$$
2	1	lnopeq0lem2	$$⊢\left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to T\left(y\right){\cdot }_{\mathrm{ih}}z=\frac{\left(T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)\right)-\left(T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)\right)+\mathrm{i}\left(\left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)\right)}{4}$$
3	2	adantl	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to T\left(y\right){\cdot }_{\mathrm{ih}}z=\frac{\left(T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)\right)-\left(T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)\right)+\mathrm{i}\left(\left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)\right)}{4}$$
4		hvaddcl	$$⊢\left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to y{+}_{ℎ}z\in \mathscr{H}$$
5		fveq2	$$⊢x=y{+}_{ℎ}z\to T\left(x\right)=T\left(y{+}_{ℎ}z\right)$$
6		id	$$⊢x=y{+}_{ℎ}z\to x=y{+}_{ℎ}z$$
7	5 6	oveq12d	$$⊢x=y{+}_{ℎ}z\to T\left(x\right){\cdot }_{\mathrm{ih}}x=T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)$$
8	7	eqeq1d	$$⊢x=y{+}_{ℎ}z\to \left(T\left(x\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)=0\right)$$
9	8	rspccva	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge y{+}_{ℎ}z\in \mathscr{H}\right)\to T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)=0$$
10	4 9	sylan2	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)=0$$
11		hvsubcl	$$⊢\left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to y{-}_{ℎ}z\in \mathscr{H}$$
12		fveq2	$$⊢x=y{-}_{ℎ}z\to T\left(x\right)=T\left(y{-}_{ℎ}z\right)$$
13		id	$$⊢x=y{-}_{ℎ}z\to x=y{-}_{ℎ}z$$
14	12 13	oveq12d	$$⊢x=y{-}_{ℎ}z\to T\left(x\right){\cdot }_{\mathrm{ih}}x=T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)$$
15	14	eqeq1d	$$⊢x=y{-}_{ℎ}z\to \left(T\left(x\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)=0\right)$$
16	15	rspccva	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge y{-}_{ℎ}z\in \mathscr{H}\right)\to T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)=0$$
17	11 16	sylan2	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)=0$$
18	10 17	oveq12d	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \left(T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)\right)-\left(T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)\right)=0-0$$
19		0m0e0	$$⊢0-0=0$$
20	18 19	eqtrdi	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \left(T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)\right)-\left(T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)\right)=0$$
21		ax-icn	$$⊢\mathrm{i}\in ℂ$$
22		hvmulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge z\in \mathscr{H}\right)\to \mathrm{i}{\cdot }_{ℎ}z\in \mathscr{H}$$
23	21 22	mpan	$$⊢z\in \mathscr{H}\to \mathrm{i}{\cdot }_{ℎ}z\in \mathscr{H}$$
24		hvaddcl	$$⊢\left(y\in \mathscr{H}\wedge \mathrm{i}{\cdot }_{ℎ}z\in \mathscr{H}\right)\to y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\in \mathscr{H}$$
25	23 24	sylan2	$$⊢\left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\in \mathscr{H}$$
26		fveq2	$$⊢x=y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\to T\left(x\right)=T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)$$
27		id	$$⊢x=y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\to x=y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)$$
28	26 27	oveq12d	$$⊢x=y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\to T\left(x\right){\cdot }_{\mathrm{ih}}x=T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)$$
29	28	eqeq1d	$$⊢x=y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\to \left(T\left(x\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)=0\right)$$
30	29	rspccva	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\in \mathscr{H}\right)\to T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)=0$$
31	25 30	sylan2	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)=0$$
32		hvsubcl	$$⊢\left(y\in \mathscr{H}\wedge \mathrm{i}{\cdot }_{ℎ}z\in \mathscr{H}\right)\to y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\in \mathscr{H}$$
33	23 32	sylan2	$$⊢\left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\in \mathscr{H}$$
34		fveq2	$$⊢x=y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\to T\left(x\right)=T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)$$
35		id	$$⊢x=y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\to x=y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)$$
36	34 35	oveq12d	$$⊢x=y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\to T\left(x\right){\cdot }_{\mathrm{ih}}x=T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)$$
37	36	eqeq1d	$$⊢x=y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\to \left(T\left(x\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)=0\right)$$
38	37	rspccva	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\in \mathscr{H}\right)\to T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)=0$$
39	33 38	sylan2	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)=0$$
40	31 39	oveq12d	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)=0-0$$
41	40 19	eqtrdi	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)=0$$
42	41	oveq2d	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \mathrm{i}\left(\left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)\right)=\mathrm{i}\cdot 0$$
43		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
44	42 43	eqtrdi	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \mathrm{i}\left(\left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)\right)=0$$
45	20 44	oveq12d	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \left(T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)\right)-\left(T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)\right)+\mathrm{i}\left(\left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)\right)=0+0$$
46		00id	$$⊢0+0=0$$
47	45 46	eqtrdi	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \left(T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)\right)-\left(T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)\right)+\mathrm{i}\left(\left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)\right)=0$$
48	47	oveq1d	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \frac{\left(T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)\right)-\left(T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)\right)+\mathrm{i}\left(\left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)\right)}{4}=\frac{0}{4}$$
49		4cn	$$⊢4\in ℂ$$
50		4ne0	$$⊢4\ne 0$$
51	49 50	div0i	$$⊢\frac{0}{4}=0$$
52	48 51	eqtrdi	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to \frac{\left(T\left(y{+}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}z\right)\right)-\left(T\left(y{-}_{ℎ}z\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}z\right)\right)+\mathrm{i}\left(\left(T\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)-\left(T\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right){\cdot }_{\mathrm{ih}}\left(y{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}z\right)\right)\right)\right)}{4}=0$$
53	3 52	eqtrd	$$⊢\left(\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\wedge \left(y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\right)\to T\left(y\right){\cdot }_{\mathrm{ih}}z=0$$
54	53	ralrimivva	$$⊢\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\to \forall y\in \mathscr{H}\forall z\in \mathscr{H}T\left(y\right){\cdot }_{\mathrm{ih}}z=0$$
55	1	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
56	55	ho01i	$$⊢\forall y\in \mathscr{H}\forall z\in \mathscr{H}T\left(y\right){\cdot }_{\mathrm{ih}}z=0\leftrightarrow T=0_{\mathrm{hop}}$$
57	54 56	sylib	$$⊢\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\to T=0_{\mathrm{hop}}$$
58		fveq1	$$⊢T=0_{\mathrm{hop}}\to T\left(x\right)=0_{\mathrm{hop}}\left(x\right)$$
59		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
60	58 59	sylan9eq	$$⊢\left(T=0_{\mathrm{hop}}\wedge x\in \mathscr{H}\right)\to T\left(x\right)=0_{ℎ}$$
61	60	oveq1d	$$⊢\left(T=0_{\mathrm{hop}}\wedge x\in \mathscr{H}\right)\to T\left(x\right){\cdot }_{\mathrm{ih}}x=0_{ℎ}{\cdot }_{\mathrm{ih}}x$$
62		hi01	$$⊢x\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}x=0$$
63	62	adantl	$$⊢\left(T=0_{\mathrm{hop}}\wedge x\in \mathscr{H}\right)\to 0_{ℎ}{\cdot }_{\mathrm{ih}}x=0$$
64	61 63	eqtrd	$$⊢\left(T=0_{\mathrm{hop}}\wedge x\in \mathscr{H}\right)\to T\left(x\right){\cdot }_{\mathrm{ih}}x=0$$
65	64	ralrimiva	$$⊢T=0_{\mathrm{hop}}\to \forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0$$
66	57 65	impbii	$$⊢\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T=0_{\mathrm{hop}}$$