Metamath Proof Explorer

Theorem nmlnop0iALT

Description: A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis nmlnop0.1 ${⊢}{T}\in \mathrm{LinOp}$
Assertion nmlnop0iALT ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0↔{T}={0}_{\mathrm{hop}}$

Proof

Step Hyp Ref Expression
1 nmlnop0.1 ${⊢}{T}\in \mathrm{LinOp}$
2 normcl ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({x}\right)\in ℝ$
3 2 recnd ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({x}\right)\in ℂ$
4 3 adantr ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({x}\right)\in ℂ$
5 norm-i ${⊢}{x}\in ℋ\to \left({norm}_{ℎ}\left({x}\right)=0↔{x}={0}_{ℎ}\right)$
6 fveq2 ${⊢}{x}={0}_{ℎ}\to {T}\left({x}\right)={T}\left({0}_{ℎ}\right)$
7 1 lnop0i ${⊢}{T}\left({0}_{ℎ}\right)={0}_{ℎ}$
8 6 7 syl6eq ${⊢}{x}={0}_{ℎ}\to {T}\left({x}\right)={0}_{ℎ}$
9 5 8 syl6bi ${⊢}{x}\in ℋ\to \left({norm}_{ℎ}\left({x}\right)=0\to {T}\left({x}\right)={0}_{ℎ}\right)$
10 9 necon3d ${⊢}{x}\in ℋ\to \left({T}\left({x}\right)\ne {0}_{ℎ}\to {norm}_{ℎ}\left({x}\right)\ne 0\right)$
11 10 imp ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left({x}\right)\ne 0$
12 4 11 recne0d ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left({x}\right)}\ne 0$
13 simpr ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {T}\left({x}\right)\ne {0}_{ℎ}$
14 4 11 reccld ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ$
15 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
16 15 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
17 16 adantr ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {T}\left({x}\right)\in ℋ$
18 hvmul0or ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\wedge {T}\left({x}\right)\in ℋ\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)={0}_{ℎ}↔\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}=0\vee {T}\left({x}\right)={0}_{ℎ}\right)\right)$
19 14 17 18 syl2anc ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)={0}_{ℎ}↔\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}=0\vee {T}\left({x}\right)={0}_{ℎ}\right)\right)$
20 19 necon3abid ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\ne {0}_{ℎ}↔¬\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}=0\vee {T}\left({x}\right)={0}_{ℎ}\right)\right)$
21 neanior ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\ne 0\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)↔¬\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}=0\vee {T}\left({x}\right)={0}_{ℎ}\right)$
22 20 21 syl6bbr ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\ne {0}_{ℎ}↔\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\ne 0\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\right)$
23 12 13 22 mpbir2and ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\ne {0}_{ℎ}$
24 hvmulcl ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\wedge {T}\left({x}\right)\in ℋ\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\in ℋ$
25 14 17 24 syl2anc ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\in ℋ$
26 normgt0 ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\in ℋ\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\right)$
27 25 26 syl ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\right)$
28 23 27 mpbid ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to 0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)$
29 28 ex ${⊢}{x}\in ℋ\to \left({T}\left({x}\right)\ne {0}_{ℎ}\to 0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\right)$
30 29 adantl ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\to \left({T}\left({x}\right)\ne {0}_{ℎ}\to 0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\right)$
31 nmopsetretHIL ${⊢}{T}:ℋ⟶ℋ\to \left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\}\subseteq ℝ$
32 15 31 ax-mp ${⊢}\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\}\subseteq ℝ$
33 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
34 32 33 sstri ${⊢}\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\}\subseteq {ℝ}^{*}$
35 simpl ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {x}\in ℋ$
36 hvmulcl ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\wedge {x}\in ℋ\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in ℋ$
37 14 35 36 syl2anc ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in ℋ$
38 8 necon3i ${⊢}{T}\left({x}\right)\ne {0}_{ℎ}\to {x}\ne {0}_{ℎ}$
39 norm1 ${⊢}\left({x}\in ℋ\wedge {x}\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=1$
40 38 39 sylan2 ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=1$
41 1re ${⊢}1\in ℝ$
42 40 41 syl6eqel ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\in ℝ$
43 eqle ${⊢}\left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\in ℝ\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=1\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\le 1$
44 42 40 43 syl2anc ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\le 1$
45 1 lnopmuli ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\in ℂ\wedge {x}\in ℋ\right)\to {T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)$
46 14 35 45 syl2anc ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)$
47 46 eqcomd ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)={T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)$
48 47 fveq2d ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\right)$
49 fveq2 ${⊢}{z}=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\to {norm}_{ℎ}\left({z}\right)={norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)$
50 49 breq1d ${⊢}{z}=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\to \left({norm}_{ℎ}\left({z}\right)\le 1↔{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\le 1\right)$
51 fveq2 ${⊢}{z}=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\to {T}\left({z}\right)={T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)$
52 51 fveq2d ${⊢}{z}=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\to {norm}_{ℎ}\left({T}\left({z}\right)\right)={norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\right)$
53 52 eqeq2d ${⊢}{z}=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\to \left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({z}\right)\right)↔{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\right)\right)$
54 50 53 anbi12d ${⊢}{z}=\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\to \left(\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)↔\left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\le 1\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\right)\right)\right)$
55 54 rspcev ${⊢}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\in ℋ\wedge \left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\le 1\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{x}\right)\right)\right)\right)\to \exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)$
56 37 44 48 55 syl12anc ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)$
57 fvex ${⊢}{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\in \mathrm{V}$
58 eqeq1 ${⊢}{y}={norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\to \left({y}={norm}_{ℎ}\left({T}\left({z}\right)\right)↔{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)$
59 58 anbi2d ${⊢}{y}={norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\to \left(\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)↔\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right)$
60 59 rexbidv ${⊢}{y}={norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\to \left(\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)↔\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right)$
61 57 60 elab ${⊢}{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\in \left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\}↔\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)$
62 56 61 sylibr ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\in \left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\}$
63 supxrub ${⊢}\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\}\subseteq {ℝ}^{*}\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\in \left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\le sup\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
64 34 62 63 sylancr ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\le sup\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
65 64 adantll ${⊢}\left(\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\le sup\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
66 nmopval ${⊢}{T}:ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({T}\right)=sup\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
67 15 66 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=sup\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
68 67 eqeq1i ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0↔sup\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)=0$
69 68 biimpi ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0\to sup\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)=0$
70 69 ad2antrr ${⊢}\left(\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to sup\left(\left\{{y}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)=0$
71 65 70 breqtrd ${⊢}\left(\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\le 0$
72 normcl ${⊢}\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\in ℋ\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\in ℝ$
73 25 72 syl ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\in ℝ$
74 0re ${⊢}0\in ℝ$
75 lenlt ${⊢}\left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\in ℝ\wedge 0\in ℝ\right)\to \left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\le 0↔¬0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\right)$
76 73 74 75 sylancl ${⊢}\left({x}\in ℋ\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\le 0↔¬0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\right)$
77 76 adantll ${⊢}\left(\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to \left({norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\le 0↔¬0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\right)$
78 71 77 mpbid ${⊢}\left(\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\wedge {T}\left({x}\right)\ne {0}_{ℎ}\right)\to ¬0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)$
79 78 ex ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\to \left({T}\left({x}\right)\ne {0}_{ℎ}\to ¬0<{norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left({x}\right)}\right){\cdot }_{ℎ}{T}\left({x}\right)\right)\right)$
80 30 79 pm2.65d ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\to ¬{T}\left({x}\right)\ne {0}_{ℎ}$
81 nne ${⊢}¬{T}\left({x}\right)\ne {0}_{ℎ}↔{T}\left({x}\right)={0}_{ℎ}$
82 80 81 sylib ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\to {T}\left({x}\right)={0}_{ℎ}$
83 ho0val ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
84 83 adantl ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
85 82 84 eqtr4d ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)=0\wedge {x}\in ℋ\right)\to {T}\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
86 85 ralrimiva ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
87 ffn ${⊢}{T}:ℋ⟶ℋ\to {T}Fnℋ$
88 15 87 ax-mp ${⊢}{T}Fnℋ$
89 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
90 ffn ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ\to {0}_{\mathrm{hop}}Fnℋ$
91 89 90 ax-mp ${⊢}{0}_{\mathrm{hop}}Fnℋ$
92 eqfnfv ${⊢}\left({T}Fnℋ\wedge {0}_{\mathrm{hop}}Fnℋ\right)\to \left({T}={0}_{\mathrm{hop}}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)\right)$
93 88 91 92 mp2an ${⊢}{T}={0}_{\mathrm{hop}}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
94 86 93 sylibr ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0\to {T}={0}_{\mathrm{hop}}$
95 fveq2 ${⊢}{T}={0}_{\mathrm{hop}}\to {norm}_{\mathrm{op}}\left({T}\right)={norm}_{\mathrm{op}}\left({0}_{\mathrm{hop}}\right)$
96 nmop0 ${⊢}{norm}_{\mathrm{op}}\left({0}_{\mathrm{hop}}\right)=0$
97 95 96 syl6eq ${⊢}{T}={0}_{\mathrm{hop}}\to {norm}_{\mathrm{op}}\left({T}\right)=0$
98 94 97 impbii ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0↔{T}={0}_{\mathrm{hop}}$