# Metamath Proof Explorer

## 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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0↔{T}={0}_{\mathrm{hop}}$

### Proof

Step Hyp Ref Expression
1 lnopeq0.1 ${⊢}{T}\in \mathrm{LinOp}$
2 1 lnopeq0lem2 ${⊢}\left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\wedge {z}\in ℋ\right)\to {y}{+}_{ℎ}{z}\in ℋ$
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↔{T}\left({y}{+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}\left({y}{+}_{ℎ}{z}\right)=0\right)$
9 8 rspccva ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge {y}{+}_{ℎ}{z}\in ℋ\right)\to {T}\left({y}{+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}\left({y}{+}_{ℎ}{z}\right)=0$
10 4 9 sylan2 ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\right)\right)\to {T}\left({y}{+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}\left({y}{+}_{ℎ}{z}\right)=0$
11 hvsubcl ${⊢}\left({y}\in ℋ\wedge {z}\in ℋ\right)\to {y}{-}_{ℎ}{z}\in ℋ$
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↔{T}\left({y}{-}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}\left({y}{-}_{ℎ}{z}\right)=0\right)$
16 15 rspccva ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge {y}{-}_{ℎ}{z}\in ℋ\right)\to {T}\left({y}{-}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}\left({y}{-}_{ℎ}{z}\right)=0$
17 11 16 sylan2 ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\right)\right)\to {T}\left({y}{-}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}\left({y}{-}_{ℎ}{z}\right)=0$
18 10 17 oveq12d ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 syl6eq ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\right)\to \mathrm{i}{\cdot }_{ℎ}{z}\in ℋ$
23 21 22 mpan ${⊢}{z}\in ℋ\to \mathrm{i}{\cdot }_{ℎ}{z}\in ℋ$
24 hvaddcl ${⊢}\left({y}\in ℋ\wedge \mathrm{i}{\cdot }_{ℎ}{z}\in ℋ\right)\to {y}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{z}\right)\in ℋ$
25 23 24 sylan2 ${⊢}\left({y}\in ℋ\wedge {z}\in ℋ\right)\to {y}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{z}\right)\in ℋ$
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↔{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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge {y}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{z}\right)\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\wedge \mathrm{i}{\cdot }_{ℎ}{z}\in ℋ\right)\to {y}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{z}\right)\in ℋ$
33 23 32 sylan2 ${⊢}\left({y}\in ℋ\wedge {z}\in ℋ\right)\to {y}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{z}\right)\in ℋ$
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↔{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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge {y}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{z}\right)\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 syl6eq ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 syl6eq ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 syl6eq ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 syl6eq ${⊢}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\wedge \left({y}\in ℋ\wedge {z}\in ℋ\right)\right)\to {T}\left({y}\right){\cdot }_{\mathrm{ih}}{z}=0$
54 53 ralrimivva ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\to \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right){\cdot }_{\mathrm{ih}}{z}=0$
55 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
56 55 ho01i ${⊢}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right){\cdot }_{\mathrm{ih}}{z}=0↔{T}={0}_{\mathrm{hop}}$
57 54 56 sylib ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{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 ℋ\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
60 58 59 sylan9eq ${⊢}\left({T}={0}_{\mathrm{hop}}\wedge {x}\in ℋ\right)\to {T}\left({x}\right)={0}_{ℎ}$
61 60 oveq1d ${⊢}\left({T}={0}_{\mathrm{hop}}\wedge {x}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={0}_{ℎ}{\cdot }_{\mathrm{ih}}{x}$
62 hi01 ${⊢}{x}\in ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{x}=0$
63 62 adantl ${⊢}\left({T}={0}_{\mathrm{hop}}\wedge {x}\in ℋ\right)\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{x}=0$
64 61 63 eqtrd ${⊢}\left({T}={0}_{\mathrm{hop}}\wedge {x}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0$
65 64 ralrimiva ${⊢}{T}={0}_{\mathrm{hop}}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0$
66 57 65 impbii ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0↔{T}={0}_{\mathrm{hop}}$