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 ⊒ 𝑋 = ( BaseSet β€˜ π‘ˆ )
ubth.2 ⊒ 𝑁 = ( normCV β€˜ π‘Š )
ubthlem.3 ⊒ 𝐷 = ( IndMet β€˜ π‘ˆ )
ubthlem.4 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
ubthlem.5 ⊒ π‘ˆ ∈ CBan
ubthlem.6 ⊒ π‘Š ∈ NrmCVec
ubthlem.7 ⊒ ( πœ‘ β†’ 𝑇 βŠ† ( π‘ˆ BLnOp π‘Š ) )
ubthlem.8 ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝑋 βˆƒ 𝑐 ∈ ℝ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ 𝑐 )
ubthlem.9 ⊒ 𝐴 = ( π‘˜ ∈ β„• ↦ { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ π‘˜ } )
ubthlem.10 ⊒ ( πœ‘ β†’ 𝐾 ∈ β„• )
ubthlem.11 ⊒ ( πœ‘ β†’ 𝑃 ∈ 𝑋 )
ubthlem.12 ⊒ ( πœ‘ β†’ 𝑅 ∈ ℝ+ )
ubthlem.13 ⊒ ( πœ‘ β†’ { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 } βŠ† ( 𝐴 β€˜ 𝐾 ) )
Assertion ubthlem2 ( πœ‘ β†’ βˆƒ 𝑑 ∈ ℝ βˆ€ 𝑑 ∈ 𝑇 ( ( π‘ˆ normOpOLD π‘Š ) β€˜ 𝑑 ) ≀ 𝑑 )

Proof

Step Hyp Ref Expression
1 ubth.1 ⊒ 𝑋 = ( BaseSet β€˜ π‘ˆ )
2 ubth.2 ⊒ 𝑁 = ( normCV β€˜ π‘Š )
3 ubthlem.3 ⊒ 𝐷 = ( IndMet β€˜ π‘ˆ )
4 ubthlem.4 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
5 ubthlem.5 ⊒ π‘ˆ ∈ CBan
6 ubthlem.6 ⊒ π‘Š ∈ NrmCVec
7 ubthlem.7 ⊒ ( πœ‘ β†’ 𝑇 βŠ† ( π‘ˆ BLnOp π‘Š ) )
8 ubthlem.8 ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝑋 βˆƒ 𝑐 ∈ ℝ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ 𝑐 )
9 ubthlem.9 ⊒ 𝐴 = ( π‘˜ ∈ β„• ↦ { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ π‘˜ } )
10 ubthlem.10 ⊒ ( πœ‘ β†’ 𝐾 ∈ β„• )
11 ubthlem.11 ⊒ ( πœ‘ β†’ 𝑃 ∈ 𝑋 )
12 ubthlem.12 ⊒ ( πœ‘ β†’ 𝑅 ∈ ℝ+ )
13 ubthlem.13 ⊒ ( πœ‘ β†’ { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 } βŠ† ( 𝐴 β€˜ 𝐾 ) )
14 10 nnrpd ⊒ ( πœ‘ β†’ 𝐾 ∈ ℝ+ )
15 14 14 rpaddcld ⊒ ( πœ‘ β†’ ( 𝐾 + 𝐾 ) ∈ ℝ+ )
16 15 12 rpdivcld ⊒ ( πœ‘ β†’ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ+ )
17 16 rpred ⊒ ( πœ‘ β†’ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ )
18 oveq2 ⊒ ( 𝑧 = ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) β†’ ( 𝑃 𝐷 𝑧 ) = ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) )
19 18 breq1d ⊒ ( 𝑧 = ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) β†’ ( ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 ↔ ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ≀ 𝑅 ) )
20 eleq1 ⊒ ( 𝑧 = ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) β†’ ( 𝑧 ∈ ( 𝐴 β€˜ 𝐾 ) ↔ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ ( 𝐴 β€˜ 𝐾 ) ) )
21 19 20 imbi12d ⊒ ( 𝑧 = ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) β†’ ( ( ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 β†’ 𝑧 ∈ ( 𝐴 β€˜ 𝐾 ) ) ↔ ( ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ≀ 𝑅 β†’ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ ( 𝐴 β€˜ 𝐾 ) ) ) )
22 rabss ⊒ ( { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 } βŠ† ( 𝐴 β€˜ 𝐾 ) ↔ βˆ€ 𝑧 ∈ 𝑋 ( ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 β†’ 𝑧 ∈ ( 𝐴 β€˜ 𝐾 ) ) )
23 13 22 sylib ⊒ ( πœ‘ β†’ βˆ€ 𝑧 ∈ 𝑋 ( ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 β†’ 𝑧 ∈ ( 𝐴 β€˜ 𝐾 ) ) )
24 23 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ βˆ€ 𝑧 ∈ 𝑋 ( ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 β†’ 𝑧 ∈ ( 𝐴 β€˜ 𝐾 ) ) )
25 bnnv ⊒ ( π‘ˆ ∈ CBan β†’ π‘ˆ ∈ NrmCVec )
26 5 25 ax-mp ⊒ π‘ˆ ∈ NrmCVec
27 26 a1i ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ π‘ˆ ∈ NrmCVec )
28 11 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑃 ∈ 𝑋 )
29 12 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑅 ∈ ℝ+ )
30 29 rpcnd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑅 ∈ β„‚ )
31 simpr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ π‘₯ ∈ 𝑋 )
32 eqid ⊒ ( ·𝑠OLD β€˜ π‘ˆ ) = ( ·𝑠OLD β€˜ π‘ˆ )
33 1 32 nvscl ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ 𝑅 ∈ β„‚ ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ∈ 𝑋 )
34 27 30 31 33 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ∈ 𝑋 )
35 eqid ⊒ ( +𝑣 β€˜ π‘ˆ ) = ( +𝑣 β€˜ π‘ˆ )
36 1 35 nvgcl ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ∈ 𝑋 ) β†’ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 )
37 27 28 34 36 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 )
38 21 24 37 rspcdva ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ≀ 𝑅 β†’ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ ( 𝐴 β€˜ 𝐾 ) ) )
39 1 3 cbncms ⊒ ( π‘ˆ ∈ CBan β†’ 𝐷 ∈ ( CMet β€˜ 𝑋 ) )
40 5 39 ax-mp ⊒ 𝐷 ∈ ( CMet β€˜ 𝑋 )
41 cmetmet ⊒ ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
42 metxmet ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
43 40 41 42 mp2b ⊒ 𝐷 ∈ ( ∞Met β€˜ 𝑋 )
44 43 a1i ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
45 xmetsym ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 ) β†’ ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) = ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) 𝐷 𝑃 ) )
46 44 28 37 45 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) = ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) 𝐷 𝑃 ) )
47 eqid ⊒ ( βˆ’π‘£ β€˜ π‘ˆ ) = ( βˆ’π‘£ β€˜ π‘ˆ )
48 eqid ⊒ ( normCV β€˜ π‘ˆ ) = ( normCV β€˜ π‘ˆ )
49 1 47 48 3 imsdval ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) β†’ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) 𝐷 𝑃 ) = ( ( normCV β€˜ π‘ˆ ) β€˜ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ( βˆ’π‘£ β€˜ π‘ˆ ) 𝑃 ) ) )
50 27 37 28 49 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) 𝐷 𝑃 ) = ( ( normCV β€˜ π‘ˆ ) β€˜ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ( βˆ’π‘£ β€˜ π‘ˆ ) 𝑃 ) ) )
51 1 35 47 nvpncan2 ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ∈ 𝑋 ) β†’ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ( βˆ’π‘£ β€˜ π‘ˆ ) 𝑃 ) = ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) )
52 27 28 34 51 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ( βˆ’π‘£ β€˜ π‘ˆ ) 𝑃 ) = ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) )
53 52 fveq2d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( normCV β€˜ π‘ˆ ) β€˜ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ( βˆ’π‘£ β€˜ π‘ˆ ) 𝑃 ) ) = ( ( normCV β€˜ π‘ˆ ) β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) )
54 46 50 53 3eqtrd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) = ( ( normCV β€˜ π‘ˆ ) β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) )
55 29 rprege0d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑅 ∈ ℝ ∧ 0 ≀ 𝑅 ) )
56 1 32 48 nvsge0 ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ ( 𝑅 ∈ ℝ ∧ 0 ≀ 𝑅 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( normCV β€˜ π‘ˆ ) β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) = ( 𝑅 Β· ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ) )
57 27 55 31 56 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( normCV β€˜ π‘ˆ ) β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) = ( 𝑅 Β· ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ) )
58 54 57 eqtrd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) = ( 𝑅 Β· ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ) )
59 30 mulridd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑅 Β· 1 ) = 𝑅 )
60 59 eqcomd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑅 = ( 𝑅 Β· 1 ) )
61 58 60 breq12d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ≀ 𝑅 ↔ ( 𝑅 Β· ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ) ≀ ( 𝑅 Β· 1 ) ) )
62 1 48 nvcl ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ∈ ℝ )
63 26 62 mpan ⊒ ( π‘₯ ∈ 𝑋 β†’ ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ∈ ℝ )
64 63 adantl ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ∈ ℝ )
65 1red ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 1 ∈ ℝ )
66 64 65 29 lemul2d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ≀ 1 ↔ ( 𝑅 Β· ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ) ≀ ( 𝑅 Β· 1 ) ) )
67 61 66 bitr4d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑃 𝐷 ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ≀ 𝑅 ↔ ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ≀ 1 ) )
68 breq2 ⊒ ( π‘˜ = 𝐾 β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ π‘˜ ↔ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 ) )
69 68 ralbidv ⊒ ( π‘˜ = 𝐾 β†’ ( βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ π‘˜ ↔ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 ) )
70 69 rabbidv ⊒ ( π‘˜ = 𝐾 β†’ { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ π‘˜ } = { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 } )
71 1 fvexi ⊒ 𝑋 ∈ V
72 71 rabex ⊒ { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 } ∈ V
73 70 9 72 fvmpt ⊒ ( 𝐾 ∈ β„• β†’ ( 𝐴 β€˜ 𝐾 ) = { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 } )
74 10 73 syl ⊒ ( πœ‘ β†’ ( 𝐴 β€˜ 𝐾 ) = { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 } )
75 74 eleq2d ⊒ ( πœ‘ β†’ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ ( 𝐴 β€˜ 𝐾 ) ↔ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 } ) )
76 2fveq3 ⊒ ( 𝑧 = ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) = ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) )
77 76 breq1d ⊒ ( 𝑧 = ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 ↔ ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) )
78 77 ralbidv ⊒ ( 𝑧 = ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) β†’ ( βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 ↔ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) )
79 78 elrab ⊒ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 } ↔ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 ∧ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) )
80 75 79 bitrdi ⊒ ( πœ‘ β†’ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ ( 𝐴 β€˜ 𝐾 ) ↔ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 ∧ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) ) )
81 80 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ ( 𝐴 β€˜ 𝐾 ) ↔ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 ∧ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) ) )
82 38 67 81 3imtr3d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ≀ 1 β†’ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 ∧ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) ) )
83 rsp ⊒ ( βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 β†’ ( 𝑑 ∈ 𝑇 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) )
84 83 com12 ⊒ ( 𝑑 ∈ 𝑇 β†’ ( βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) )
85 84 ad2antlr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) )
86 xmet0 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( 𝑃 𝐷 𝑃 ) = 0 )
87 43 11 86 sylancr ⊒ ( πœ‘ β†’ ( 𝑃 𝐷 𝑃 ) = 0 )
88 12 rpge0d ⊒ ( πœ‘ β†’ 0 ≀ 𝑅 )
89 87 88 eqbrtrd ⊒ ( πœ‘ β†’ ( 𝑃 𝐷 𝑃 ) ≀ 𝑅 )
90 oveq2 ⊒ ( 𝑧 = 𝑃 β†’ ( 𝑃 𝐷 𝑧 ) = ( 𝑃 𝐷 𝑃 ) )
91 90 breq1d ⊒ ( 𝑧 = 𝑃 β†’ ( ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 ↔ ( 𝑃 𝐷 𝑃 ) ≀ 𝑅 ) )
92 91 elrab ⊒ ( 𝑃 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 } ↔ ( 𝑃 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑃 ) ≀ 𝑅 ) )
93 11 89 92 sylanbrc ⊒ ( πœ‘ β†’ 𝑃 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≀ 𝑅 } )
94 13 93 sseldd ⊒ ( πœ‘ β†’ 𝑃 ∈ ( 𝐴 β€˜ 𝐾 ) )
95 94 74 eleqtrd ⊒ ( πœ‘ β†’ 𝑃 ∈ { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 } )
96 2fveq3 ⊒ ( 𝑧 = 𝑃 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) = ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) )
97 96 breq1d ⊒ ( 𝑧 = 𝑃 β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 ↔ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 ) )
98 97 ralbidv ⊒ ( 𝑧 = 𝑃 β†’ ( βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 ↔ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 ) )
99 98 elrab ⊒ ( 𝑃 ∈ { 𝑧 ∈ 𝑋 ∣ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑧 ) ) ≀ 𝐾 } ↔ ( 𝑃 ∈ 𝑋 ∧ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 ) )
100 95 99 sylib ⊒ ( πœ‘ β†’ ( 𝑃 ∈ 𝑋 ∧ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 ) )
101 100 simprd ⊒ ( πœ‘ β†’ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 )
102 101 r19.21bi ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 )
103 102 adantr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 )
104 7 sselda ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ 𝑑 ∈ ( π‘ˆ BLnOp π‘Š ) )
105 eqid ⊒ ( IndMet β€˜ π‘Š ) = ( IndMet β€˜ π‘Š )
106 eqid ⊒ ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) = ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) )
107 eqid ⊒ ( π‘ˆ BLnOp π‘Š ) = ( π‘ˆ BLnOp π‘Š )
108 3 105 4 106 107 26 6 blocn2 ⊒ ( 𝑑 ∈ ( π‘ˆ BLnOp π‘Š ) β†’ 𝑑 ∈ ( 𝐽 Cn ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ) )
109 4 mopntopon ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
110 43 109 ax-mp ⊒ 𝐽 ∈ ( TopOn β€˜ 𝑋 )
111 eqid ⊒ ( BaseSet β€˜ π‘Š ) = ( BaseSet β€˜ π‘Š )
112 111 105 imsxmet ⊒ ( π‘Š ∈ NrmCVec β†’ ( IndMet β€˜ π‘Š ) ∈ ( ∞Met β€˜ ( BaseSet β€˜ π‘Š ) ) )
113 106 mopntopon ⊒ ( ( IndMet β€˜ π‘Š ) ∈ ( ∞Met β€˜ ( BaseSet β€˜ π‘Š ) ) β†’ ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ∈ ( TopOn β€˜ ( BaseSet β€˜ π‘Š ) ) )
114 6 112 113 mp2b ⊒ ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ∈ ( TopOn β€˜ ( BaseSet β€˜ π‘Š ) )
115 iscncl ⊒ ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ∈ ( TopOn β€˜ ( BaseSet β€˜ π‘Š ) ) ) β†’ ( 𝑑 ∈ ( 𝐽 Cn ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ) ↔ ( 𝑑 : 𝑋 ⟢ ( BaseSet β€˜ π‘Š ) ∧ βˆ€ π‘₯ ∈ ( Clsd β€˜ ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ) ( β—‘ 𝑑 β€œ π‘₯ ) ∈ ( Clsd β€˜ 𝐽 ) ) ) )
116 110 114 115 mp2an ⊒ ( 𝑑 ∈ ( 𝐽 Cn ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ) ↔ ( 𝑑 : 𝑋 ⟢ ( BaseSet β€˜ π‘Š ) ∧ βˆ€ π‘₯ ∈ ( Clsd β€˜ ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ) ( β—‘ 𝑑 β€œ π‘₯ ) ∈ ( Clsd β€˜ 𝐽 ) ) )
117 108 116 sylib ⊒ ( 𝑑 ∈ ( π‘ˆ BLnOp π‘Š ) β†’ ( 𝑑 : 𝑋 ⟢ ( BaseSet β€˜ π‘Š ) ∧ βˆ€ π‘₯ ∈ ( Clsd β€˜ ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ) ( β—‘ 𝑑 β€œ π‘₯ ) ∈ ( Clsd β€˜ 𝐽 ) ) )
118 104 117 syl ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ ( 𝑑 : 𝑋 ⟢ ( BaseSet β€˜ π‘Š ) ∧ βˆ€ π‘₯ ∈ ( Clsd β€˜ ( MetOpen β€˜ ( IndMet β€˜ π‘Š ) ) ) ( β—‘ 𝑑 β€œ π‘₯ ) ∈ ( Clsd β€˜ 𝐽 ) ) )
119 118 simpld ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ 𝑑 : 𝑋 ⟢ ( BaseSet β€˜ π‘Š ) )
120 119 adantr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑑 : 𝑋 ⟢ ( BaseSet β€˜ π‘Š ) )
121 120 37 ffvelcdmd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ∈ ( BaseSet β€˜ π‘Š ) )
122 111 2 nvcl ⊒ ( ( π‘Š ∈ NrmCVec ∧ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ∈ ( BaseSet β€˜ π‘Š ) ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ∈ ℝ )
123 6 121 122 sylancr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ∈ ℝ )
124 120 28 ffvelcdmd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑑 β€˜ 𝑃 ) ∈ ( BaseSet β€˜ π‘Š ) )
125 111 2 nvcl ⊒ ( ( π‘Š ∈ NrmCVec ∧ ( 𝑑 β€˜ 𝑃 ) ∈ ( BaseSet β€˜ π‘Š ) ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ∈ ℝ )
126 6 124 125 sylancr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ∈ ℝ )
127 10 nnred ⊒ ( πœ‘ β†’ 𝐾 ∈ ℝ )
128 127 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝐾 ∈ ℝ )
129 le2add ⊒ ( ( ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ∈ ℝ ∧ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ∈ ℝ ) ∧ ( 𝐾 ∈ ℝ ∧ 𝐾 ∈ ℝ ) ) β†’ ( ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ∧ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 ) β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ≀ ( 𝐾 + 𝐾 ) ) )
130 123 126 128 128 129 syl22anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ∧ ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ≀ 𝐾 ) β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ≀ ( 𝐾 + 𝐾 ) ) )
131 103 130 mpan2d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ≀ ( 𝐾 + 𝐾 ) ) )
132 52 fveq2d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑑 β€˜ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ( βˆ’π‘£ β€˜ π‘ˆ ) 𝑃 ) ) = ( 𝑑 β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) )
133 6 a1i ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ π‘Š ∈ NrmCVec )
134 eqid ⊒ ( π‘ˆ LnOp π‘Š ) = ( π‘ˆ LnOp π‘Š )
135 134 107 bloln ⊒ ( ( π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑑 ∈ ( π‘ˆ BLnOp π‘Š ) ) β†’ 𝑑 ∈ ( π‘ˆ LnOp π‘Š ) )
136 26 6 135 mp3an12 ⊒ ( 𝑑 ∈ ( π‘ˆ BLnOp π‘Š ) β†’ 𝑑 ∈ ( π‘ˆ LnOp π‘Š ) )
137 104 136 syl ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ 𝑑 ∈ ( π‘ˆ LnOp π‘Š ) )
138 137 adantr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑑 ∈ ( π‘ˆ LnOp π‘Š ) )
139 eqid ⊒ ( βˆ’π‘£ β€˜ π‘Š ) = ( βˆ’π‘£ β€˜ π‘Š )
140 1 47 139 134 lnosub ⊒ ( ( ( π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑑 ∈ ( π‘ˆ LnOp π‘Š ) ) ∧ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) ) β†’ ( 𝑑 β€˜ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ( βˆ’π‘£ β€˜ π‘ˆ ) 𝑃 ) ) = ( ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ( βˆ’π‘£ β€˜ π‘Š ) ( 𝑑 β€˜ 𝑃 ) ) )
141 27 133 138 37 28 140 syl32anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑑 β€˜ ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ( βˆ’π‘£ β€˜ π‘ˆ ) 𝑃 ) ) = ( ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ( βˆ’π‘£ β€˜ π‘Š ) ( 𝑑 β€˜ 𝑃 ) ) )
142 eqid ⊒ ( ·𝑠OLD β€˜ π‘Š ) = ( ·𝑠OLD β€˜ π‘Š )
143 1 32 142 134 lnomul ⊒ ( ( ( π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑑 ∈ ( π‘ˆ LnOp π‘Š ) ) ∧ ( 𝑅 ∈ β„‚ ∧ π‘₯ ∈ 𝑋 ) ) β†’ ( 𝑑 β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) = ( 𝑅 ( ·𝑠OLD β€˜ π‘Š ) ( 𝑑 β€˜ π‘₯ ) ) )
144 27 133 138 30 31 143 syl32anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑑 β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) = ( 𝑅 ( ·𝑠OLD β€˜ π‘Š ) ( 𝑑 β€˜ π‘₯ ) ) )
145 132 141 144 3eqtr3d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ( βˆ’π‘£ β€˜ π‘Š ) ( 𝑑 β€˜ 𝑃 ) ) = ( 𝑅 ( ·𝑠OLD β€˜ π‘Š ) ( 𝑑 β€˜ π‘₯ ) ) )
146 145 fveq2d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ( βˆ’π‘£ β€˜ π‘Š ) ( 𝑑 β€˜ 𝑃 ) ) ) = ( 𝑁 β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘Š ) ( 𝑑 β€˜ π‘₯ ) ) ) )
147 119 ffvelcdmda ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑑 β€˜ π‘₯ ) ∈ ( BaseSet β€˜ π‘Š ) )
148 111 142 2 nvsge0 ⊒ ( ( π‘Š ∈ NrmCVec ∧ ( 𝑅 ∈ ℝ ∧ 0 ≀ 𝑅 ) ∧ ( 𝑑 β€˜ π‘₯ ) ∈ ( BaseSet β€˜ π‘Š ) ) β†’ ( 𝑁 β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘Š ) ( 𝑑 β€˜ π‘₯ ) ) ) = ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) )
149 133 55 147 148 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 𝑅 ( ·𝑠OLD β€˜ π‘Š ) ( 𝑑 β€˜ π‘₯ ) ) ) = ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) )
150 146 149 eqtrd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ( βˆ’π‘£ β€˜ π‘Š ) ( 𝑑 β€˜ 𝑃 ) ) ) = ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) )
151 111 139 2 nvmtri ⊒ ( ( π‘Š ∈ NrmCVec ∧ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ∈ ( BaseSet β€˜ π‘Š ) ∧ ( 𝑑 β€˜ 𝑃 ) ∈ ( BaseSet β€˜ π‘Š ) ) β†’ ( 𝑁 β€˜ ( ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ( βˆ’π‘£ β€˜ π‘Š ) ( 𝑑 β€˜ 𝑃 ) ) ) ≀ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) )
152 133 121 124 151 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ( βˆ’π‘£ β€˜ π‘Š ) ( 𝑑 β€˜ 𝑃 ) ) ) ≀ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) )
153 150 152 eqbrtrrd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ≀ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) )
154 29 rpred ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑅 ∈ ℝ )
155 111 2 nvcl ⊒ ( ( π‘Š ∈ NrmCVec ∧ ( 𝑑 β€˜ π‘₯ ) ∈ ( BaseSet β€˜ π‘Š ) ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ∈ ℝ )
156 6 147 155 sylancr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ∈ ℝ )
157 154 156 remulcld ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ∈ ℝ )
158 123 126 readdcld ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ∈ ℝ )
159 15 rpred ⊒ ( πœ‘ β†’ ( 𝐾 + 𝐾 ) ∈ ℝ )
160 159 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝐾 + 𝐾 ) ∈ ℝ )
161 letr ⊒ ( ( ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ∈ ℝ ∧ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ∈ ℝ ∧ ( 𝐾 + 𝐾 ) ∈ ℝ ) β†’ ( ( ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ≀ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ∧ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ≀ ( 𝐾 + 𝐾 ) ) β†’ ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ≀ ( 𝐾 + 𝐾 ) ) )
162 157 158 160 161 syl3anc ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ≀ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ∧ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ≀ ( 𝐾 + 𝐾 ) ) β†’ ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ≀ ( 𝐾 + 𝐾 ) ) )
163 153 162 mpand ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) + ( 𝑁 β€˜ ( 𝑑 β€˜ 𝑃 ) ) ) ≀ ( 𝐾 + 𝐾 ) β†’ ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ≀ ( 𝐾 + 𝐾 ) ) )
164 131 163 syld ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 β†’ ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ≀ ( 𝐾 + 𝐾 ) ) )
165 156 160 29 lemuldiv2d ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑅 Β· ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ) ≀ ( 𝐾 + 𝐾 ) ↔ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
166 164 165 sylibd ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
167 85 166 syld ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
168 167 adantld ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ∈ 𝑋 ∧ βˆ€ 𝑑 ∈ 𝑇 ( 𝑁 β€˜ ( 𝑑 β€˜ ( 𝑃 ( +𝑣 β€˜ π‘ˆ ) ( 𝑅 ( ·𝑠OLD β€˜ π‘ˆ ) π‘₯ ) ) ) ) ≀ 𝐾 ) β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
169 82 168 syld ⊒ ( ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ≀ 1 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
170 169 ralrimiva ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ βˆ€ π‘₯ ∈ 𝑋 ( ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ≀ 1 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
171 16 rpxrd ⊒ ( πœ‘ β†’ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ* )
172 171 adantr ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ* )
173 eqid ⊒ ( π‘ˆ normOpOLD π‘Š ) = ( π‘ˆ normOpOLD π‘Š )
174 1 111 48 2 173 26 6 nmoubi ⊒ ( ( 𝑑 : 𝑋 ⟢ ( BaseSet β€˜ π‘Š ) ∧ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ* ) β†’ ( ( ( π‘ˆ normOpOLD π‘Š ) β€˜ 𝑑 ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ↔ βˆ€ π‘₯ ∈ 𝑋 ( ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ≀ 1 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) ) )
175 119 172 174 syl2anc ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ ( ( ( π‘ˆ normOpOLD π‘Š ) β€˜ 𝑑 ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ↔ βˆ€ π‘₯ ∈ 𝑋 ( ( ( normCV β€˜ π‘ˆ ) β€˜ π‘₯ ) ≀ 1 β†’ ( 𝑁 β€˜ ( 𝑑 β€˜ π‘₯ ) ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) ) )
176 170 175 mpbird ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝑇 ) β†’ ( ( π‘ˆ normOpOLD π‘Š ) β€˜ 𝑑 ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) )
177 176 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ 𝑑 ∈ 𝑇 ( ( π‘ˆ normOpOLD π‘Š ) β€˜ 𝑑 ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) )
178 brralrspcev ⊒ ( ( ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ ∧ βˆ€ 𝑑 ∈ 𝑇 ( ( π‘ˆ normOpOLD π‘Š ) β€˜ 𝑑 ) ≀ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) β†’ βˆƒ 𝑑 ∈ ℝ βˆ€ 𝑑 ∈ 𝑇 ( ( π‘ˆ normOpOLD π‘Š ) β€˜ 𝑑 ) ≀ 𝑑 )
179 17 177 178 syl2anc ⊒ ( πœ‘ β†’ βˆƒ 𝑑 ∈ ℝ βˆ€ 𝑑 ∈ 𝑇 ( ( π‘ˆ normOpOLD π‘Š ) β€˜ 𝑑 ) ≀ 𝑑 )