# Metamath Proof Explorer

## Theorem lnconi

Description: Lemma for lnopconi and lnfnconi . (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lncon.1 ${⊢}{T}\in {C}\to {S}\in ℝ$
lncon.2 ${⊢}\left({T}\in {C}\wedge {y}\in ℋ\right)\to {N}\left({T}\left({y}\right)\right)\le {S}{norm}_{ℎ}\left({y}\right)$
lncon.3 ${⊢}{T}\in {C}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
lncon.4 ${⊢}{y}\in ℋ\to {N}\left({T}\left({y}\right)\right)\in ℝ$
lncon.5 ${⊢}\left({w}\in ℋ\wedge {x}\in ℋ\right)\to {T}\left({w}{-}_{ℎ}{x}\right)={T}\left({w}\right){M}{T}\left({x}\right)$
Assertion lnconi ${⊢}{T}\in {C}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)$

### Proof

Step Hyp Ref Expression
1 lncon.1 ${⊢}{T}\in {C}\to {S}\in ℝ$
2 lncon.2 ${⊢}\left({T}\in {C}\wedge {y}\in ℋ\right)\to {N}\left({T}\left({y}\right)\right)\le {S}{norm}_{ℎ}\left({y}\right)$
3 lncon.3 ${⊢}{T}\in {C}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
4 lncon.4 ${⊢}{y}\in ℋ\to {N}\left({T}\left({y}\right)\right)\in ℝ$
5 lncon.5 ${⊢}\left({w}\in ℋ\wedge {x}\in ℋ\right)\to {T}\left({w}{-}_{ℎ}{x}\right)={T}\left({w}\right){M}{T}\left({x}\right)$
6 2 ralrimiva ${⊢}{T}\in {C}\to \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {S}{norm}_{ℎ}\left({y}\right)$
7 oveq1 ${⊢}{x}={S}\to {x}{norm}_{ℎ}\left({y}\right)={S}{norm}_{ℎ}\left({y}\right)$
8 7 breq2d ${⊢}{x}={S}\to \left({N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)↔{N}\left({T}\left({y}\right)\right)\le {S}{norm}_{ℎ}\left({y}\right)\right)$
9 8 ralbidv ${⊢}{x}={S}\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {S}{norm}_{ℎ}\left({y}\right)\right)$
10 9 rspcev ${⊢}\left({S}\in ℝ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {S}{norm}_{ℎ}\left({y}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)$
11 1 6 10 syl2anc ${⊢}{T}\in {C}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)$
12 arch ${⊢}{x}\in ℝ\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{n}$
13 12 adantr ${⊢}\left({x}\in ℝ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{n}$
14 nnre ${⊢}{n}\in ℕ\to {n}\in ℝ$
15 simplll ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to {x}\in ℝ$
16 simpllr ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to {n}\in ℝ$
17 normcl ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({y}\right)\in ℝ$
18 17 adantl ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({y}\right)\in ℝ$
19 normge0 ${⊢}{y}\in ℋ\to 0\le {norm}_{ℎ}\left({y}\right)$
20 19 adantl ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to 0\le {norm}_{ℎ}\left({y}\right)$
21 ltle ${⊢}\left({x}\in ℝ\wedge {n}\in ℝ\right)\to \left({x}<{n}\to {x}\le {n}\right)$
22 21 imp ${⊢}\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\to {x}\le {n}$
23 22 adantr ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to {x}\le {n}$
24 15 16 18 20 23 lemul1ad ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to {x}{norm}_{ℎ}\left({y}\right)\le {n}{norm}_{ℎ}\left({y}\right)$
25 4 adantl ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to {N}\left({T}\left({y}\right)\right)\in ℝ$
26 simpll ${⊢}\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\to {x}\in ℝ$
27 remulcl ${⊢}\left({x}\in ℝ\wedge {norm}_{ℎ}\left({y}\right)\in ℝ\right)\to {x}{norm}_{ℎ}\left({y}\right)\in ℝ$
28 26 17 27 syl2an ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to {x}{norm}_{ℎ}\left({y}\right)\in ℝ$
29 simplr ${⊢}\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\to {n}\in ℝ$
30 remulcl ${⊢}\left({n}\in ℝ\wedge {norm}_{ℎ}\left({y}\right)\in ℝ\right)\to {n}{norm}_{ℎ}\left({y}\right)\in ℝ$
31 29 17 30 syl2an ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to {n}{norm}_{ℎ}\left({y}\right)\in ℝ$
32 letr ${⊢}\left({N}\left({T}\left({y}\right)\right)\in ℝ\wedge {x}{norm}_{ℎ}\left({y}\right)\in ℝ\wedge {n}{norm}_{ℎ}\left({y}\right)\in ℝ\right)\to \left(\left({N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\wedge {x}{norm}_{ℎ}\left({y}\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\to {N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)$
33 25 28 31 32 syl3anc ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to \left(\left({N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\wedge {x}{norm}_{ℎ}\left({y}\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\to {N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)$
34 24 33 mpan2d ${⊢}\left(\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\wedge {y}\in ℋ\right)\to \left({N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\to {N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)$
35 34 ralimdva ${⊢}\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge {x}<{n}\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\to \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)$
36 35 impancom ${⊢}\left(\left({x}\in ℝ\wedge {n}\in ℝ\right)\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)\to \left({x}<{n}\to \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)$
37 36 an32s ${⊢}\left(\left({x}\in ℝ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)\wedge {n}\in ℝ\right)\to \left({x}<{n}\to \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)$
38 14 37 sylan2 ${⊢}\left(\left({x}\in ℝ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)\wedge {n}\in ℕ\right)\to \left({x}<{n}\to \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)$
39 38 reximdva ${⊢}\left({x}\in ℝ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{n}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)$
40 13 39 mpd ${⊢}\left({x}\in ℝ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)$
41 40 rexlimiva ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)$
42 simprr ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\right)\to {z}\in {ℝ}^{+}$
43 simpll ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\right)\to {n}\in ℕ$
44 43 nnrpd ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\right)\to {n}\in {ℝ}^{+}$
45 42 44 rpdivcld ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\right)\to \frac{{z}}{{n}}\in {ℝ}^{+}$
46 simprr ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {w}\in ℋ$
47 simprll ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {x}\in ℋ$
48 hvsubcl ${⊢}\left({w}\in ℋ\wedge {x}\in ℋ\right)\to {w}{-}_{ℎ}{x}\in ℋ$
49 46 47 48 syl2anc ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {w}{-}_{ℎ}{x}\in ℋ$
50 2fveq3 ${⊢}{y}={w}{-}_{ℎ}{x}\to {N}\left({T}\left({y}\right)\right)={N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)$
51 fveq2 ${⊢}{y}={w}{-}_{ℎ}{x}\to {norm}_{ℎ}\left({y}\right)={norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
52 51 oveq2d ${⊢}{y}={w}{-}_{ℎ}{x}\to {n}{norm}_{ℎ}\left({y}\right)={n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
53 50 52 breq12d ${⊢}{y}={w}{-}_{ℎ}{x}\to \left({N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)↔{N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\le {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\right)$
54 53 rspcva ${⊢}\left({w}{-}_{ℎ}{x}\in ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\le {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
55 49 54 sylan ${⊢}\left(\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\le {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
56 55 an32s ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\le {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
57 50 eleq1d ${⊢}{y}={w}{-}_{ℎ}{x}\to \left({N}\left({T}\left({y}\right)\right)\in ℝ↔{N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\in ℝ\right)$
58 57 4 vtoclga ${⊢}{w}{-}_{ℎ}{x}\in ℋ\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\in ℝ$
59 49 58 syl ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\in ℝ$
60 14 adantr ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {n}\in ℝ$
61 normcl ${⊢}{w}{-}_{ℎ}{x}\in ℋ\to {norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\in ℝ$
62 49 61 syl ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\in ℝ$
63 remulcl ${⊢}\left({n}\in ℝ\wedge {norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\in ℝ\right)\to {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\in ℝ$
64 60 62 63 syl2anc ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\in ℝ$
65 simprlr ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {z}\in {ℝ}^{+}$
66 65 rpred ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {z}\in ℝ$
67 lelttr ${⊢}\left({N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\in ℝ\wedge {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\in ℝ\wedge {z}\in ℝ\right)\to \left(\left({N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\le {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\wedge {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\right)\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)<{z}\right)$
68 59 64 66 67 syl3anc ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to \left(\left({N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\le {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\wedge {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\right)\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)<{z}\right)$
69 68 adantlr ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to \left(\left({N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)\le {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\wedge {n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\right)\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)<{z}\right)$
70 56 69 mpand ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to \left({n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)<{z}\right)$
71 nnrp ${⊢}{n}\in ℕ\to {n}\in {ℝ}^{+}$
72 71 rpregt0d ${⊢}{n}\in ℕ\to \left({n}\in ℝ\wedge 0<{n}\right)$
73 72 adantr ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to \left({n}\in ℝ\wedge 0<{n}\right)$
74 ltmuldiv2 ${⊢}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)\in ℝ\wedge {z}\in ℝ\wedge \left({n}\in ℝ\wedge 0<{n}\right)\right)\to \left({n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}↔{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<\frac{{z}}{{n}}\right)$
75 62 66 73 74 syl3anc ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to \left({n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}↔{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<\frac{{z}}{{n}}\right)$
76 75 adantlr ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to \left({n}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}↔{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<\frac{{z}}{{n}}\right)$
77 46 47 5 syl2anc ${⊢}\left({n}\in ℕ\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {T}\left({w}{-}_{ℎ}{x}\right)={T}\left({w}\right){M}{T}\left({x}\right)$
78 77 adantlr ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {T}\left({w}{-}_{ℎ}{x}\right)={T}\left({w}\right){M}{T}\left({x}\right)$
79 78 fveq2d ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to {N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)={N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)$
80 79 breq1d ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to \left({N}\left({T}\left({w}{-}_{ℎ}{x}\right)\right)<{z}↔{N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
81 70 76 80 3imtr3d ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left(\left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\right)\to \left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<\frac{{z}}{{n}}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
82 81 anassrs ${⊢}\left(\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\right)\wedge {w}\in ℋ\right)\to \left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<\frac{{z}}{{n}}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
83 82 ralrimiva ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\right)\to \forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<\frac{{z}}{{n}}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
84 breq2 ${⊢}{y}=\frac{{z}}{{n}}\to \left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}↔{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<\frac{{z}}{{n}}\right)$
85 84 rspceaimv ${⊢}\left(\frac{{z}}{{n}}\in {ℝ}^{+}\wedge \forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<\frac{{z}}{{n}}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
86 45 83 85 syl2anc ${⊢}\left(\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\wedge \left({x}\in ℋ\wedge {z}\in {ℝ}^{+}\right)\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
87 86 ralrimivva ${⊢}\left({n}\in ℕ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
88 87 rexlimiva ${⊢}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}\to {N}\left({T}\left({w}\right){M}{T}\left({x}\right)\right)<{z}\right)$
89 88 3 sylibr ${⊢}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {n}{norm}_{ℎ}\left({y}\right)\to {T}\in {C}$
90 41 89 syl ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\to {T}\in {C}$
91 11 90 impbii ${⊢}{T}\in {C}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)$