# Metamath Proof Explorer

## Theorem nmcexi

Description: Lemma for nmcopexi and nmcfnexi . The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of Beran p. 99. (Contributed by Mario Carneiro, 17-Nov-2013) (Proof shortened by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcex.1 ${⊢}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)$
nmcex.2 ${⊢}{S}\left({T}\right)=sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
nmcex.3 ${⊢}{x}\in ℋ\to {N}\left({T}\left({x}\right)\right)\in ℝ$
nmcex.4 ${⊢}{N}\left({T}\left({0}_{ℎ}\right)\right)=0$
nmcex.5 ${⊢}\left(\frac{{y}}{2}\in {ℝ}^{+}\wedge {x}\in ℋ\right)\to \left(\frac{{y}}{2}\right){N}\left({T}\left({x}\right)\right)={N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)$
Assertion nmcexi ${⊢}{S}\left({T}\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 nmcex.1 ${⊢}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)$
2 nmcex.2 ${⊢}{S}\left({T}\right)=sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
3 nmcex.3 ${⊢}{x}\in ℋ\to {N}\left({T}\left({x}\right)\right)\in ℝ$
4 nmcex.4 ${⊢}{N}\left({T}\left({0}_{ℎ}\right)\right)=0$
5 nmcex.5 ${⊢}\left(\frac{{y}}{2}\in {ℝ}^{+}\wedge {x}\in ℋ\right)\to \left(\frac{{y}}{2}\right){N}\left({T}\left({x}\right)\right)={N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)$
6 eleq1 ${⊢}{m}={N}\left({T}\left({x}\right)\right)\to \left({m}\in ℝ↔{N}\left({T}\left({x}\right)\right)\in ℝ\right)$
7 3 6 syl5ibrcom ${⊢}{x}\in ℋ\to \left({m}={N}\left({T}\left({x}\right)\right)\to {m}\in ℝ\right)$
8 7 imp ${⊢}\left({x}\in ℋ\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\to {m}\in ℝ$
9 8 adantrl ${⊢}\left({x}\in ℋ\wedge \left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right)\to {m}\in ℝ$
10 9 rexlimiva ${⊢}\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\to {m}\in ℝ$
11 10 abssi ${⊢}\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\subseteq ℝ$
12 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
13 norm0 ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)=0$
14 0le1 ${⊢}0\le 1$
15 13 14 eqbrtri ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)\le 1$
16 4 eqcomi ${⊢}0={N}\left({T}\left({0}_{ℎ}\right)\right)$
17 15 16 pm3.2i ${⊢}\left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge 0={N}\left({T}\left({0}_{ℎ}\right)\right)\right)$
18 fveq2 ${⊢}{x}={0}_{ℎ}\to {norm}_{ℎ}\left({x}\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
19 18 breq1d ${⊢}{x}={0}_{ℎ}\to \left({norm}_{ℎ}\left({x}\right)\le 1↔{norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\right)$
20 2fveq3 ${⊢}{x}={0}_{ℎ}\to {N}\left({T}\left({x}\right)\right)={N}\left({T}\left({0}_{ℎ}\right)\right)$
21 20 eqeq2d ${⊢}{x}={0}_{ℎ}\to \left(0={N}\left({T}\left({x}\right)\right)↔0={N}\left({T}\left({0}_{ℎ}\right)\right)\right)$
22 19 21 anbi12d ${⊢}{x}={0}_{ℎ}\to \left(\left({norm}_{ℎ}\left({x}\right)\le 1\wedge 0={N}\left({T}\left({x}\right)\right)\right)↔\left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge 0={N}\left({T}\left({0}_{ℎ}\right)\right)\right)\right)$
23 22 rspcev ${⊢}\left({0}_{ℎ}\in ℋ\wedge \left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge 0={N}\left({T}\left({0}_{ℎ}\right)\right)\right)\right)\to \exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge 0={N}\left({T}\left({x}\right)\right)\right)$
24 12 17 23 mp2an ${⊢}\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge 0={N}\left({T}\left({x}\right)\right)\right)$
25 c0ex ${⊢}0\in \mathrm{V}$
26 eqeq1 ${⊢}{m}=0\to \left({m}={N}\left({T}\left({x}\right)\right)↔0={N}\left({T}\left({x}\right)\right)\right)$
27 26 anbi2d ${⊢}{m}=0\to \left(\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)↔\left({norm}_{ℎ}\left({x}\right)\le 1\wedge 0={N}\left({T}\left({x}\right)\right)\right)\right)$
28 27 rexbidv ${⊢}{m}=0\to \left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)↔\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge 0={N}\left({T}\left({x}\right)\right)\right)\right)$
29 25 28 elab ${⊢}0\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}↔\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge 0={N}\left({T}\left({x}\right)\right)\right)$
30 24 29 mpbir ${⊢}0\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}$
31 30 ne0ii ${⊢}\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\ne \varnothing$
32 2rp ${⊢}2\in {ℝ}^{+}$
33 rpdivcl ${⊢}\left(2\in {ℝ}^{+}\wedge {y}\in {ℝ}^{+}\right)\to \frac{2}{{y}}\in {ℝ}^{+}$
34 32 33 mpan ${⊢}{y}\in {ℝ}^{+}\to \frac{2}{{y}}\in {ℝ}^{+}$
35 34 rpred ${⊢}{y}\in {ℝ}^{+}\to \frac{2}{{y}}\in ℝ$
36 35 adantr ${⊢}\left({y}\in {ℝ}^{+}\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\to \frac{2}{{y}}\in ℝ$
37 rpre ${⊢}{y}\in {ℝ}^{+}\to {y}\in ℝ$
38 37 adantr ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {y}\in ℝ$
39 38 rehalfcld ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \frac{{y}}{2}\in ℝ$
40 39 recnd ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \frac{{y}}{2}\in ℂ$
41 simprl ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {x}\in ℋ$
42 hvmulcl ${⊢}\left(\frac{{y}}{2}\in ℂ\wedge {x}\in ℋ\right)\to \left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\in ℋ$
43 40 41 42 syl2anc ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\in ℋ$
44 normcl ${⊢}\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\in ℋ\to {norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\in ℝ$
45 43 44 syl ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\in ℝ$
46 simprr ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {norm}_{ℎ}\left({x}\right)\le 1$
47 normcl ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({x}\right)\in ℝ$
48 47 ad2antrl ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {norm}_{ℎ}\left({x}\right)\in ℝ$
49 1red ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to 1\in ℝ$
50 rphalfcl ${⊢}{y}\in {ℝ}^{+}\to \frac{{y}}{2}\in {ℝ}^{+}$
51 50 adantr ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \frac{{y}}{2}\in {ℝ}^{+}$
52 48 49 51 lemul2d ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left({norm}_{ℎ}\left({x}\right)\le 1↔\left(\frac{{y}}{2}\right){norm}_{ℎ}\left({x}\right)\le \left(\frac{{y}}{2}\right)\cdot 1\right)$
53 46 52 mpbid ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\frac{{y}}{2}\right){norm}_{ℎ}\left({x}\right)\le \left(\frac{{y}}{2}\right)\cdot 1$
54 rpcn ${⊢}\frac{{y}}{2}\in {ℝ}^{+}\to \frac{{y}}{2}\in ℂ$
55 norm-iii ${⊢}\left(\frac{{y}}{2}\in ℂ\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)=\left|\frac{{y}}{2}\right|{norm}_{ℎ}\left({x}\right)$
56 54 55 sylan ${⊢}\left(\frac{{y}}{2}\in {ℝ}^{+}\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)=\left|\frac{{y}}{2}\right|{norm}_{ℎ}\left({x}\right)$
57 rpre ${⊢}\frac{{y}}{2}\in {ℝ}^{+}\to \frac{{y}}{2}\in ℝ$
58 rpge0 ${⊢}\frac{{y}}{2}\in {ℝ}^{+}\to 0\le \frac{{y}}{2}$
59 57 58 absidd ${⊢}\frac{{y}}{2}\in {ℝ}^{+}\to \left|\frac{{y}}{2}\right|=\frac{{y}}{2}$
60 59 oveq1d ${⊢}\frac{{y}}{2}\in {ℝ}^{+}\to \left|\frac{{y}}{2}\right|{norm}_{ℎ}\left({x}\right)=\left(\frac{{y}}{2}\right){norm}_{ℎ}\left({x}\right)$
61 60 adantr ${⊢}\left(\frac{{y}}{2}\in {ℝ}^{+}\wedge {x}\in ℋ\right)\to \left|\frac{{y}}{2}\right|{norm}_{ℎ}\left({x}\right)=\left(\frac{{y}}{2}\right){norm}_{ℎ}\left({x}\right)$
62 56 61 eqtr2d ${⊢}\left(\frac{{y}}{2}\in {ℝ}^{+}\wedge {x}\in ℋ\right)\to \left(\frac{{y}}{2}\right){norm}_{ℎ}\left({x}\right)={norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)$
63 51 41 62 syl2anc ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\frac{{y}}{2}\right){norm}_{ℎ}\left({x}\right)={norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)$
64 40 mulid1d ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\frac{{y}}{2}\right)\cdot 1=\frac{{y}}{2}$
65 53 63 64 3brtr3d ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\le \frac{{y}}{2}$
66 rphalflt ${⊢}{y}\in {ℝ}^{+}\to \frac{{y}}{2}<{y}$
67 66 adantr ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \frac{{y}}{2}<{y}$
68 45 39 38 65 67 lelttrd ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)<{y}$
69 fveq2 ${⊢}{z}=\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\to {norm}_{ℎ}\left({z}\right)={norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)$
70 69 breq1d ${⊢}{z}=\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\to \left({norm}_{ℎ}\left({z}\right)<{y}↔{norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)<{y}\right)$
71 2fveq3 ${⊢}{z}=\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\to {N}\left({T}\left({z}\right)\right)={N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)$
72 71 breq1d ${⊢}{z}=\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\to \left({N}\left({T}\left({z}\right)\right)<1↔{N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)<1\right)$
73 70 72 imbi12d ${⊢}{z}=\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\to \left(\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)↔\left({norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)<{y}\to {N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)<1\right)\right)$
74 73 rspcv ${⊢}\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\in ℋ\to \left(\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\to \left({norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)<{y}\to {N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)<1\right)\right)$
75 43 74 syl ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\to \left({norm}_{ℎ}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)<{y}\to {N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)<1\right)\right)$
76 68 75 mpid ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\to {N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)<1\right)$
77 3 ad2antrl ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {N}\left({T}\left({x}\right)\right)\in ℝ$
78 77 49 51 ltmuldiv2d ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\left(\frac{{y}}{2}\right){N}\left({T}\left({x}\right)\right)<1↔{N}\left({T}\left({x}\right)\right)<\frac{1}{\frac{{y}}{2}}\right)$
79 51 rprecred ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \frac{1}{\frac{{y}}{2}}\in ℝ$
80 ltle ${⊢}\left({N}\left({T}\left({x}\right)\right)\in ℝ\wedge \frac{1}{\frac{{y}}{2}}\in ℝ\right)\to \left({N}\left({T}\left({x}\right)\right)<\frac{1}{\frac{{y}}{2}}\to {N}\left({T}\left({x}\right)\right)\le \frac{1}{\frac{{y}}{2}}\right)$
81 77 79 80 syl2anc ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left({N}\left({T}\left({x}\right)\right)<\frac{1}{\frac{{y}}{2}}\to {N}\left({T}\left({x}\right)\right)\le \frac{1}{\frac{{y}}{2}}\right)$
82 78 81 sylbid ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\left(\frac{{y}}{2}\right){N}\left({T}\left({x}\right)\right)<1\to {N}\left({T}\left({x}\right)\right)\le \frac{1}{\frac{{y}}{2}}\right)$
83 51 41 5 syl2anc ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\frac{{y}}{2}\right){N}\left({T}\left({x}\right)\right)={N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)$
84 83 breq1d ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\left(\frac{{y}}{2}\right){N}\left({T}\left({x}\right)\right)<1↔{N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)<1\right)$
85 rpcn ${⊢}{y}\in {ℝ}^{+}\to {y}\in ℂ$
86 rpne0 ${⊢}{y}\in {ℝ}^{+}\to {y}\ne 0$
87 2cn ${⊢}2\in ℂ$
88 2ne0 ${⊢}2\ne 0$
89 recdiv ${⊢}\left(\left({y}\in ℂ\wedge {y}\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{1}{\frac{{y}}{2}}=\frac{2}{{y}}$
90 87 88 89 mpanr12 ${⊢}\left({y}\in ℂ\wedge {y}\ne 0\right)\to \frac{1}{\frac{{y}}{2}}=\frac{2}{{y}}$
91 85 86 90 syl2anc ${⊢}{y}\in {ℝ}^{+}\to \frac{1}{\frac{{y}}{2}}=\frac{2}{{y}}$
92 91 adantr ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \frac{1}{\frac{{y}}{2}}=\frac{2}{{y}}$
93 92 breq2d ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left({N}\left({T}\left({x}\right)\right)\le \frac{1}{\frac{{y}}{2}}↔{N}\left({T}\left({x}\right)\right)\le \frac{2}{{y}}\right)$
94 82 84 93 3imtr3d ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left({N}\left({T}\left(\left(\frac{{y}}{2}\right){\cdot }_{ℎ}{x}\right)\right)<1\to {N}\left({T}\left({x}\right)\right)\le \frac{2}{{y}}\right)$
95 76 94 syld ${⊢}\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to \left(\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\to {N}\left({T}\left({x}\right)\right)\le \frac{2}{{y}}\right)$
96 95 imp ${⊢}\left(\left({y}\in {ℝ}^{+}\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\to {N}\left({T}\left({x}\right)\right)\le \frac{2}{{y}}$
97 96 an32s ${⊢}\left(\left({y}\in {ℝ}^{+}\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\wedge \left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)\to {N}\left({T}\left({x}\right)\right)\le \frac{2}{{y}}$
98 97 anassrs ${⊢}\left(\left(\left({y}\in {ℝ}^{+}\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {N}\left({T}\left({x}\right)\right)\le \frac{2}{{y}}$
99 breq1 ${⊢}{n}={N}\left({T}\left({x}\right)\right)\to \left({n}\le \frac{2}{{y}}↔{N}\left({T}\left({x}\right)\right)\le \frac{2}{{y}}\right)$
100 98 99 syl5ibrcom ${⊢}\left(\left(\left({y}\in {ℝ}^{+}\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left({n}={N}\left({T}\left({x}\right)\right)\to {n}\le \frac{2}{{y}}\right)$
101 100 expimpd ${⊢}\left(\left({y}\in {ℝ}^{+}\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\wedge {x}\in ℋ\right)\to \left(\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le \frac{2}{{y}}\right)$
102 101 rexlimdva ${⊢}\left({y}\in {ℝ}^{+}\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\to \left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le \frac{2}{{y}}\right)$
103 102 alrimiv ${⊢}\left({y}\in {ℝ}^{+}\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\to \forall {n}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le \frac{2}{{y}}\right)$
104 eqeq1 ${⊢}{m}={n}\to \left({m}={N}\left({T}\left({x}\right)\right)↔{n}={N}\left({T}\left({x}\right)\right)\right)$
105 104 anbi2d ${⊢}{m}={n}\to \left(\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)↔\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\right)$
106 105 rexbidv ${⊢}{m}={n}\to \left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)↔\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\right)$
107 106 ralab ${⊢}\forall {n}\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{n}\le {z}↔\forall {n}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le {z}\right)$
108 breq2 ${⊢}{z}=\frac{2}{{y}}\to \left({n}\le {z}↔{n}\le \frac{2}{{y}}\right)$
109 108 imbi2d ${⊢}{z}=\frac{2}{{y}}\to \left(\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le {z}\right)↔\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le \frac{2}{{y}}\right)\right)$
110 109 albidv ${⊢}{z}=\frac{2}{{y}}\to \left(\forall {n}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le {z}\right)↔\forall {n}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le \frac{2}{{y}}\right)\right)$
111 107 110 syl5bb ${⊢}{z}=\frac{2}{{y}}\to \left(\forall {n}\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{n}\le {z}↔\forall {n}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le \frac{2}{{y}}\right)\right)$
112 111 rspcev ${⊢}\left(\frac{2}{{y}}\in ℝ\wedge \forall {n}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {n}={N}\left({T}\left({x}\right)\right)\right)\to {n}\le \frac{2}{{y}}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{n}\le {z}$
113 36 103 112 syl2anc ${⊢}\left({y}\in {ℝ}^{+}\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{n}\le {z}$
114 113 rexlimiva ${⊢}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)<{y}\to {N}\left({T}\left({z}\right)\right)<1\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{n}\le {z}$
115 1 114 ax-mp ${⊢}\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{n}\le {z}$
116 supxrre ${⊢}\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\subseteq ℝ\wedge \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{n}\le {z}\right)\to sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},ℝ,<\right)$
117 11 31 115 116 mp3an ${⊢}sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},ℝ,<\right)$
118 2 117 eqtri ${⊢}{S}\left({T}\right)=sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},ℝ,<\right)$
119 suprcl ${⊢}\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\subseteq ℝ\wedge \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{n}\le {z}\right)\to sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},ℝ,<\right)\in ℝ$
120 11 31 115 119 mp3an ${⊢}sup\left(\left\{{m}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {m}={N}\left({T}\left({x}\right)\right)\right)\right\},ℝ,<\right)\in ℝ$
121 118 120 eqeltri ${⊢}{S}\left({T}\right)\in ℝ$