# Metamath Proof Explorer

## Theorem ubthlem2

Description: Lemma for ubth . Given that there is a closed ball B ( P , R ) in AK , for any x e. B ( 0 , 1 ) , we have P + R x. x e. B ( P , R ) and P e. B ( P , R ) , so both of these have norm ( t ( z ) ) <_ K and so norm ( t ( x ) ) <_ ( norm ( t ( P ) ) + norm ( t ( P + R x. x ) ) ) / R <_ ( K + K ) / R , which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ubth.1 $⊢ X = BaseSet ⁡ U$
ubth.2 $⊢ N = norm CV ⁡ W$
ubthlem.3 $⊢ D = IndMet ⁡ U$
ubthlem.4 $⊢ J = MetOpen ⁡ D$
ubthlem.5 $⊢ U ∈ CBan$
ubthlem.6 $⊢ W ∈ NrmCVec$
ubthlem.7 $⊢ φ → T ⊆ U BLnOp W$
ubthlem.8 $⊢ φ → ∀ x ∈ X ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c$
ubthlem.9 $⊢ A = k ∈ ℕ ⟼ z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ k$
ubthlem.10 $⊢ φ → K ∈ ℕ$
ubthlem.11 $⊢ φ → P ∈ X$
ubthlem.12 $⊢ φ → R ∈ ℝ +$
ubthlem.13 $⊢ φ → z ∈ X | P D z ≤ R ⊆ A ⁡ K$
Assertion ubthlem2 $⊢ φ → ∃ d ∈ ℝ ∀ t ∈ T U normOp OLD W ⁡ t ≤ d$

### Proof

Step Hyp Ref Expression
1 ubth.1 $⊢ X = BaseSet ⁡ U$
2 ubth.2 $⊢ N = norm CV ⁡ W$
3 ubthlem.3 $⊢ D = IndMet ⁡ U$
4 ubthlem.4 $⊢ J = MetOpen ⁡ D$
5 ubthlem.5 $⊢ U ∈ CBan$
6 ubthlem.6 $⊢ W ∈ NrmCVec$
7 ubthlem.7 $⊢ φ → T ⊆ U BLnOp W$
8 ubthlem.8 $⊢ φ → ∀ x ∈ X ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c$
9 ubthlem.9 $⊢ A = k ∈ ℕ ⟼ z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ k$
10 ubthlem.10 $⊢ φ → K ∈ ℕ$
11 ubthlem.11 $⊢ φ → P ∈ X$
12 ubthlem.12 $⊢ φ → R ∈ ℝ +$
13 ubthlem.13 $⊢ φ → z ∈ X | P D z ≤ R ⊆ A ⁡ K$
14 10 nnrpd $⊢ φ → K ∈ ℝ +$
15 14 14 rpaddcld $⊢ φ → K + K ∈ ℝ +$
16 15 12 rpdivcld $⊢ φ → K + K R ∈ ℝ +$
17 16 rpred $⊢ φ → K + K R ∈ ℝ$
18 oveq2 $⊢ z = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x → P D z = P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x$
19 18 breq1d $⊢ z = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x → P D z ≤ R ↔ P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ R$
20 eleq1 $⊢ z = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x → z ∈ A ⁡ K ↔ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ A ⁡ K$
21 19 20 imbi12d $⊢ z = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x → P D z ≤ R → z ∈ A ⁡ K ↔ P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ R → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ A ⁡ K$
22 rabss $⊢ z ∈ X | P D z ≤ R ⊆ A ⁡ K ↔ ∀ z ∈ X P D z ≤ R → z ∈ A ⁡ K$
23 13 22 sylib $⊢ φ → ∀ z ∈ X P D z ≤ R → z ∈ A ⁡ K$
24 23 ad2antrr $⊢ φ ∧ t ∈ T ∧ x ∈ X → ∀ z ∈ X P D z ≤ R → z ∈ A ⁡ K$
25 bnnv $⊢ U ∈ CBan → U ∈ NrmCVec$
26 5 25 ax-mp $⊢ U ∈ NrmCVec$
27 26 a1i $⊢ φ ∧ t ∈ T ∧ x ∈ X → U ∈ NrmCVec$
28 11 ad2antrr $⊢ φ ∧ t ∈ T ∧ x ∈ X → P ∈ X$
29 12 ad2antrr $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ∈ ℝ +$
30 29 rpcnd $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ∈ ℂ$
31 simpr $⊢ φ ∧ t ∈ T ∧ x ∈ X → x ∈ X$
32 eqid $⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U$
33 1 32 nvscl $⊢ U ∈ NrmCVec ∧ R ∈ ℂ ∧ x ∈ X → R ⋅ 𝑠OLD ⁡ U x ∈ X$
34 27 30 31 33 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ⋅ 𝑠OLD ⁡ U x ∈ X$
35 eqid $⊢ + v ⁡ U = + v ⁡ U$
36 1 35 nvgcl $⊢ U ∈ NrmCVec ∧ P ∈ X ∧ R ⋅ 𝑠OLD ⁡ U x ∈ X → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X$
37 27 28 34 36 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X$
38 21 24 37 rspcdva $⊢ φ ∧ t ∈ T ∧ x ∈ X → P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ R → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ A ⁡ K$
39 1 3 cbncms $⊢ U ∈ CBan → D ∈ CMet ⁡ X$
40 5 39 ax-mp $⊢ D ∈ CMet ⁡ X$
41 cmetmet $⊢ D ∈ CMet ⁡ X → D ∈ Met ⁡ X$
42 metxmet $⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X$
43 40 41 42 mp2b $⊢ D ∈ ∞Met ⁡ X$
44 43 a1i $⊢ φ ∧ t ∈ T ∧ x ∈ X → D ∈ ∞Met ⁡ X$
45 xmetsym $⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X → P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x D P$
46 44 28 37 45 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x D P$
47 eqid $⊢ - v ⁡ U = - v ⁡ U$
48 eqid $⊢ norm CV ⁡ U = norm CV ⁡ U$
49 1 47 48 3 imsdval $⊢ U ∈ NrmCVec ∧ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X ∧ P ∈ X → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x D P = norm CV ⁡ U ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ U P$
50 27 37 28 49 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x D P = norm CV ⁡ U ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ U P$
51 1 35 47 nvpncan2 $⊢ U ∈ NrmCVec ∧ P ∈ X ∧ R ⋅ 𝑠OLD ⁡ U x ∈ X → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ U P = R ⋅ 𝑠OLD ⁡ U x$
52 27 28 34 51 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ U P = R ⋅ 𝑠OLD ⁡ U x$
53 52 fveq2d $⊢ φ ∧ t ∈ T ∧ x ∈ X → norm CV ⁡ U ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ U P = norm CV ⁡ U ⁡ R ⋅ 𝑠OLD ⁡ U x$
54 46 50 53 3eqtrd $⊢ φ ∧ t ∈ T ∧ x ∈ X → P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x = norm CV ⁡ U ⁡ R ⋅ 𝑠OLD ⁡ U x$
55 29 rprege0d $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ∈ ℝ ∧ 0 ≤ R$
56 1 32 48 nvsge0 $⊢ U ∈ NrmCVec ∧ R ∈ ℝ ∧ 0 ≤ R ∧ x ∈ X → norm CV ⁡ U ⁡ R ⋅ 𝑠OLD ⁡ U x = R ⁢ norm CV ⁡ U ⁡ x$
57 27 55 31 56 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → norm CV ⁡ U ⁡ R ⋅ 𝑠OLD ⁡ U x = R ⁢ norm CV ⁡ U ⁡ x$
58 54 57 eqtrd $⊢ φ ∧ t ∈ T ∧ x ∈ X → P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x = R ⁢ norm CV ⁡ U ⁡ x$
59 30 mulid1d $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ⋅ 1 = R$
60 59 eqcomd $⊢ φ ∧ t ∈ T ∧ x ∈ X → R = R ⋅ 1$
61 58 60 breq12d $⊢ φ ∧ t ∈ T ∧ x ∈ X → P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ R ↔ R ⁢ norm CV ⁡ U ⁡ x ≤ R ⋅ 1$
62 1 48 nvcl $⊢ U ∈ NrmCVec ∧ x ∈ X → norm CV ⁡ U ⁡ x ∈ ℝ$
63 26 62 mpan $⊢ x ∈ X → norm CV ⁡ U ⁡ x ∈ ℝ$
64 63 adantl $⊢ φ ∧ t ∈ T ∧ x ∈ X → norm CV ⁡ U ⁡ x ∈ ℝ$
65 1red $⊢ φ ∧ t ∈ T ∧ x ∈ X → 1 ∈ ℝ$
66 64 65 29 lemul2d $⊢ φ ∧ t ∈ T ∧ x ∈ X → norm CV ⁡ U ⁡ x ≤ 1 ↔ R ⁢ norm CV ⁡ U ⁡ x ≤ R ⋅ 1$
67 61 66 bitr4d $⊢ φ ∧ t ∈ T ∧ x ∈ X → P D P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ R ↔ norm CV ⁡ U ⁡ x ≤ 1$
68 breq2 $⊢ k = K → N ⁡ t ⁡ z ≤ k ↔ N ⁡ t ⁡ z ≤ K$
69 68 ralbidv $⊢ k = K → ∀ t ∈ T N ⁡ t ⁡ z ≤ k ↔ ∀ t ∈ T N ⁡ t ⁡ z ≤ K$
70 69 rabbidv $⊢ k = K → z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ k = z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ K$
71 1 fvexi $⊢ X ∈ V$
72 71 rabex $⊢ z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ K ∈ V$
73 70 9 72 fvmpt $⊢ K ∈ ℕ → A ⁡ K = z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ K$
74 10 73 syl $⊢ φ → A ⁡ K = z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ K$
75 74 eleq2d $⊢ φ → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ A ⁡ K ↔ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ K$
76 2fveq3 $⊢ z = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x → N ⁡ t ⁡ z = N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x$
77 76 breq1d $⊢ z = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x → N ⁡ t ⁡ z ≤ K ↔ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
78 77 ralbidv $⊢ z = P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x → ∀ t ∈ T N ⁡ t ⁡ z ≤ K ↔ ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
79 78 elrab $⊢ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ K ↔ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X ∧ ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
80 75 79 bitrdi $⊢ φ → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ A ⁡ K ↔ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X ∧ ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
81 80 ad2antrr $⊢ φ ∧ t ∈ T ∧ x ∈ X → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ A ⁡ K ↔ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X ∧ ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
82 38 67 81 3imtr3d $⊢ φ ∧ t ∈ T ∧ x ∈ X → norm CV ⁡ U ⁡ x ≤ 1 → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X ∧ ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
83 rsp $⊢ ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K → t ∈ T → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
84 83 com12 $⊢ t ∈ T → ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
85 84 ad2antlr $⊢ φ ∧ t ∈ T ∧ x ∈ X → ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K$
86 xmet0 $⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → P D P = 0$
87 43 11 86 sylancr $⊢ φ → P D P = 0$
88 12 rpge0d $⊢ φ → 0 ≤ R$
89 87 88 eqbrtrd $⊢ φ → P D P ≤ R$
90 oveq2 $⊢ z = P → P D z = P D P$
91 90 breq1d $⊢ z = P → P D z ≤ R ↔ P D P ≤ R$
92 91 elrab $⊢ P ∈ z ∈ X | P D z ≤ R ↔ P ∈ X ∧ P D P ≤ R$
93 11 89 92 sylanbrc $⊢ φ → P ∈ z ∈ X | P D z ≤ R$
94 13 93 sseldd $⊢ φ → P ∈ A ⁡ K$
95 94 74 eleqtrd $⊢ φ → P ∈ z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ K$
96 2fveq3 $⊢ z = P → N ⁡ t ⁡ z = N ⁡ t ⁡ P$
97 96 breq1d $⊢ z = P → N ⁡ t ⁡ z ≤ K ↔ N ⁡ t ⁡ P ≤ K$
98 97 ralbidv $⊢ z = P → ∀ t ∈ T N ⁡ t ⁡ z ≤ K ↔ ∀ t ∈ T N ⁡ t ⁡ P ≤ K$
99 98 elrab $⊢ P ∈ z ∈ X | ∀ t ∈ T N ⁡ t ⁡ z ≤ K ↔ P ∈ X ∧ ∀ t ∈ T N ⁡ t ⁡ P ≤ K$
100 95 99 sylib $⊢ φ → P ∈ X ∧ ∀ t ∈ T N ⁡ t ⁡ P ≤ K$
101 100 simprd $⊢ φ → ∀ t ∈ T N ⁡ t ⁡ P ≤ K$
102 101 r19.21bi $⊢ φ ∧ t ∈ T → N ⁡ t ⁡ P ≤ K$
103 102 adantr $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P ≤ K$
104 7 sselda $⊢ φ ∧ t ∈ T → t ∈ U BLnOp W$
105 eqid $⊢ IndMet ⁡ W = IndMet ⁡ W$
106 eqid $⊢ MetOpen ⁡ IndMet ⁡ W = MetOpen ⁡ IndMet ⁡ W$
107 eqid $⊢ U BLnOp W = U BLnOp W$
108 3 105 4 106 107 26 6 blocn2 $⊢ t ∈ U BLnOp W → t ∈ J Cn MetOpen ⁡ IndMet ⁡ W$
109 4 mopntopon $⊢ D ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X$
110 43 109 ax-mp $⊢ J ∈ TopOn ⁡ X$
111 eqid $⊢ BaseSet ⁡ W = BaseSet ⁡ W$
112 111 105 imsxmet $⊢ W ∈ NrmCVec → IndMet ⁡ W ∈ ∞Met ⁡ BaseSet ⁡ W$
113 106 mopntopon $⊢ IndMet ⁡ W ∈ ∞Met ⁡ BaseSet ⁡ W → MetOpen ⁡ IndMet ⁡ W ∈ TopOn ⁡ BaseSet ⁡ W$
114 6 112 113 mp2b $⊢ MetOpen ⁡ IndMet ⁡ W ∈ TopOn ⁡ BaseSet ⁡ W$
115 iscncl $⊢ J ∈ TopOn ⁡ X ∧ MetOpen ⁡ IndMet ⁡ W ∈ TopOn ⁡ BaseSet ⁡ W → t ∈ J Cn MetOpen ⁡ IndMet ⁡ W ↔ t : X ⟶ BaseSet ⁡ W ∧ ∀ x ∈ Clsd ⁡ MetOpen ⁡ IndMet ⁡ W t -1 x ∈ Clsd ⁡ J$
116 110 114 115 mp2an $⊢ t ∈ J Cn MetOpen ⁡ IndMet ⁡ W ↔ t : X ⟶ BaseSet ⁡ W ∧ ∀ x ∈ Clsd ⁡ MetOpen ⁡ IndMet ⁡ W t -1 x ∈ Clsd ⁡ J$
117 108 116 sylib $⊢ t ∈ U BLnOp W → t : X ⟶ BaseSet ⁡ W ∧ ∀ x ∈ Clsd ⁡ MetOpen ⁡ IndMet ⁡ W t -1 x ∈ Clsd ⁡ J$
118 104 117 syl $⊢ φ ∧ t ∈ T → t : X ⟶ BaseSet ⁡ W ∧ ∀ x ∈ Clsd ⁡ MetOpen ⁡ IndMet ⁡ W t -1 x ∈ Clsd ⁡ J$
119 118 simpld $⊢ φ ∧ t ∈ T → t : X ⟶ BaseSet ⁡ W$
120 119 adantr $⊢ φ ∧ t ∈ T ∧ x ∈ X → t : X ⟶ BaseSet ⁡ W$
121 120 37 ffvelrnd $⊢ φ ∧ t ∈ T ∧ x ∈ X → t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ BaseSet ⁡ W$
122 111 2 nvcl $⊢ W ∈ NrmCVec ∧ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ BaseSet ⁡ W → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ ℝ$
123 6 121 122 sylancr $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ ℝ$
124 120 28 ffvelrnd $⊢ φ ∧ t ∈ T ∧ x ∈ X → t ⁡ P ∈ BaseSet ⁡ W$
125 111 2 nvcl $⊢ W ∈ NrmCVec ∧ t ⁡ P ∈ BaseSet ⁡ W → N ⁡ t ⁡ P ∈ ℝ$
126 6 124 125 sylancr $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P ∈ ℝ$
127 10 nnred $⊢ φ → K ∈ ℝ$
128 127 ad2antrr $⊢ φ ∧ t ∈ T ∧ x ∈ X → K ∈ ℝ$
129 le2add $⊢ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ ℝ ∧ N ⁡ t ⁡ P ∈ ℝ ∧ K ∈ ℝ ∧ K ∈ ℝ → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K ∧ N ⁡ t ⁡ P ≤ K → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ≤ K + K$
130 123 126 128 128 129 syl22anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K ∧ N ⁡ t ⁡ P ≤ K → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ≤ K + K$
131 103 130 mpan2d $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ≤ K + K$
132 52 fveq2d $⊢ φ ∧ t ∈ T ∧ x ∈ X → t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ U P = t ⁡ R ⋅ 𝑠OLD ⁡ U x$
133 6 a1i $⊢ φ ∧ t ∈ T ∧ x ∈ X → W ∈ NrmCVec$
134 eqid $⊢ U LnOp W = U LnOp W$
135 134 107 bloln $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ t ∈ U BLnOp W → t ∈ U LnOp W$
136 26 6 135 mp3an12 $⊢ t ∈ U BLnOp W → t ∈ U LnOp W$
137 104 136 syl $⊢ φ ∧ t ∈ T → t ∈ U LnOp W$
138 137 adantr $⊢ φ ∧ t ∈ T ∧ x ∈ X → t ∈ U LnOp W$
139 eqid $⊢ - v ⁡ W = - v ⁡ W$
140 1 47 139 134 lnosub $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ t ∈ U LnOp W ∧ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X ∧ P ∈ X → t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ U P = t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ W t ⁡ P$
141 27 133 138 37 28 140 syl32anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ U P = t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ W t ⁡ P$
142 eqid $⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W$
143 1 32 142 134 lnomul $⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ t ∈ U LnOp W ∧ R ∈ ℂ ∧ x ∈ X → t ⁡ R ⋅ 𝑠OLD ⁡ U x = R ⋅ 𝑠OLD ⁡ W t ⁡ x$
144 27 133 138 30 31 143 syl32anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → t ⁡ R ⋅ 𝑠OLD ⁡ U x = R ⋅ 𝑠OLD ⁡ W t ⁡ x$
145 132 141 144 3eqtr3d $⊢ φ ∧ t ∈ T ∧ x ∈ X → t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ W t ⁡ P = R ⋅ 𝑠OLD ⁡ W t ⁡ x$
146 145 fveq2d $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ W t ⁡ P = N ⁡ R ⋅ 𝑠OLD ⁡ W t ⁡ x$
147 119 ffvelrnda $⊢ φ ∧ t ∈ T ∧ x ∈ X → t ⁡ x ∈ BaseSet ⁡ W$
148 111 142 2 nvsge0 $⊢ W ∈ NrmCVec ∧ R ∈ ℝ ∧ 0 ≤ R ∧ t ⁡ x ∈ BaseSet ⁡ W → N ⁡ R ⋅ 𝑠OLD ⁡ W t ⁡ x = R ⁢ N ⁡ t ⁡ x$
149 133 55 147 148 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ R ⋅ 𝑠OLD ⁡ W t ⁡ x = R ⁢ N ⁡ t ⁡ x$
150 146 149 eqtrd $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ W t ⁡ P = R ⁢ N ⁡ t ⁡ x$
151 111 139 2 nvmtri $⊢ W ∈ NrmCVec ∧ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ BaseSet ⁡ W ∧ t ⁡ P ∈ BaseSet ⁡ W → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ W t ⁡ P ≤ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P$
152 133 121 124 151 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x - v ⁡ W t ⁡ P ≤ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P$
153 150 152 eqbrtrrd $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ⁢ N ⁡ t ⁡ x ≤ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P$
154 29 rpred $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ∈ ℝ$
155 111 2 nvcl $⊢ W ∈ NrmCVec ∧ t ⁡ x ∈ BaseSet ⁡ W → N ⁡ t ⁡ x ∈ ℝ$
156 6 147 155 sylancr $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ x ∈ ℝ$
157 154 156 remulcld $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ⁢ N ⁡ t ⁡ x ∈ ℝ$
158 123 126 readdcld $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ∈ ℝ$
159 15 rpred $⊢ φ → K + K ∈ ℝ$
160 159 ad2antrr $⊢ φ ∧ t ∈ T ∧ x ∈ X → K + K ∈ ℝ$
161 letr $⊢ R ⁢ N ⁡ t ⁡ x ∈ ℝ ∧ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ∈ ℝ ∧ K + K ∈ ℝ → R ⁢ N ⁡ t ⁡ x ≤ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ∧ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ≤ K + K → R ⁢ N ⁡ t ⁡ x ≤ K + K$
162 157 158 160 161 syl3anc $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ⁢ N ⁡ t ⁡ x ≤ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ∧ N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ≤ K + K → R ⁢ N ⁡ t ⁡ x ≤ K + K$
163 153 162 mpand $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x + N ⁡ t ⁡ P ≤ K + K → R ⁢ N ⁡ t ⁡ x ≤ K + K$
164 131 163 syld $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K → R ⁢ N ⁡ t ⁡ x ≤ K + K$
165 156 160 29 lemuldiv2d $⊢ φ ∧ t ∈ T ∧ x ∈ X → R ⁢ N ⁡ t ⁡ x ≤ K + K ↔ N ⁡ t ⁡ x ≤ K + K R$
166 164 165 sylibd $⊢ φ ∧ t ∈ T ∧ x ∈ X → N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K → N ⁡ t ⁡ x ≤ K + K R$
167 85 166 syld $⊢ φ ∧ t ∈ T ∧ x ∈ X → ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K → N ⁡ t ⁡ x ≤ K + K R$
168 167 adantld $⊢ φ ∧ t ∈ T ∧ x ∈ X → P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ∈ X ∧ ∀ t ∈ T N ⁡ t ⁡ P + v ⁡ U R ⋅ 𝑠OLD ⁡ U x ≤ K → N ⁡ t ⁡ x ≤ K + K R$
169 82 168 syld $⊢ φ ∧ t ∈ T ∧ x ∈ X → norm CV ⁡ U ⁡ x ≤ 1 → N ⁡ t ⁡ x ≤ K + K R$
170 169 ralrimiva $⊢ φ ∧ t ∈ T → ∀ x ∈ X norm CV ⁡ U ⁡ x ≤ 1 → N ⁡ t ⁡ x ≤ K + K R$
171 16 rpxrd $⊢ φ → K + K R ∈ ℝ *$
172 171 adantr $⊢ φ ∧ t ∈ T → K + K R ∈ ℝ *$
173 eqid $⊢ U normOp OLD W = U normOp OLD W$
174 1 111 48 2 173 26 6 nmoubi $⊢ t : X ⟶ BaseSet ⁡ W ∧ K + K R ∈ ℝ * → U normOp OLD W ⁡ t ≤ K + K R ↔ ∀ x ∈ X norm CV ⁡ U ⁡ x ≤ 1 → N ⁡ t ⁡ x ≤ K + K R$
175 119 172 174 syl2anc $⊢ φ ∧ t ∈ T → U normOp OLD W ⁡ t ≤ K + K R ↔ ∀ x ∈ X norm CV ⁡ U ⁡ x ≤ 1 → N ⁡ t ⁡ x ≤ K + K R$
176 170 175 mpbird $⊢ φ ∧ t ∈ T → U normOp OLD W ⁡ t ≤ K + K R$
177 176 ralrimiva $⊢ φ → ∀ t ∈ T U normOp OLD W ⁡ t ≤ K + K R$
178 brralrspcev $⊢ K + K R ∈ ℝ ∧ ∀ t ∈ T U normOp OLD W ⁡ t ≤ K + K R → ∃ d ∈ ℝ ∀ t ∈ T U normOp OLD W ⁡ t ≤ d$
179 17 177 178 syl2anc $⊢ φ → ∃ d ∈ ℝ ∀ t ∈ T U normOp OLD W ⁡ t ≤ d$