Metamath Proof Explorer

Theorem ubthlem3

Description: Lemma for ubth . Prove the reverse implication, using nmblolbi . (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 𝑊 ) )
Assertion ubthlem3 ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 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 fveq1 ⊢ ( 𝑢 = 𝑡 → ( 𝑢 ‘ 𝑧 ) = ( 𝑡 ‘ 𝑧 ) )
9 8 fveq2d ⊢ ( 𝑢 = 𝑡 → ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) )
10 9 breq1d ⊢ ( 𝑢 = 𝑡 → ( ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑑 ) )
11 10 cbvralvw ⊢ ( ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑑 )
12 breq2 ⊢ ( 𝑑 = 𝑐 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ) )
13 12 ralbidv ⊢ ( 𝑑 = 𝑐 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ) )
14 11 13 bitrid ⊢ ( 𝑑 = 𝑐 → ( ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ) )
15 14 cbvrexvw ⊢ ( ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 )
16 2fveq3 ⊢ ( 𝑧 = 𝑥 → ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) )
17 16 breq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
18 17 rexralbidv ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
19 15 18 bitrid ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
20 19 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
21 7 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
22 simpr ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 )
23 22 20 sylib ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
24 fveq1 ⊢ ( 𝑢 = 𝑡 → ( 𝑢 ‘ 𝑑 ) = ( 𝑡 ‘ 𝑑 ) )
25 24 fveq2d ⊢ ( 𝑢 = 𝑡 → ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) )
26 25 breq1d ⊢ ( 𝑢 = 𝑡 → ( ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) ≤ 𝑚 ) )
27 26 cbvralvw ⊢ ( ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) ≤ 𝑚 )
28 2fveq3 ⊢ ( 𝑑 = 𝑧 → ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) )
29 28 breq1d ⊢ ( 𝑑 = 𝑧 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ) )
30 29 ralbidv ⊢ ( 𝑑 = 𝑧 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ) )
31 27 30 bitrid ⊢ ( 𝑑 = 𝑧 → ( ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ) )
32 31 cbvrabv ⊢ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 }
33 breq2 ⊢ ( 𝑚 = 𝑘 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 ) )
34 33 ralbidv ⊢ ( 𝑚 = 𝑘 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 ) )
35 34 rabbidv ⊢ ( 𝑚 = 𝑘 → { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
36 32 35 eqtrid ⊢ ( 𝑚 = 𝑘 → { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
37 36 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) = ( 𝑘 ∈ ℕ ↦ { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
38 1 2 3 4 5 6 21 23 37 ubthlem1 ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ∃ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) )
39 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
40 23 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
41 simplrl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → 𝑛 ∈ ℕ )
42 simplrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → 𝑦 ∈ 𝑋 )
43 simprl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → 𝑟 ∈ ℝ+ )
44 simprr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) )
45 1 2 3 4 5 6 39 40 37 41 42 43 44 ubthlem2 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )
46 45 expr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
47 46 rexlimdva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) → ( ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
48 47 rexlimdvva ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
49 38 48 mpd ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )
50 49 ex ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
51 20 50 biimtrrid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
52 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) → 𝑑 ∈ ℝ )
53 bnnv ⊢ ( 𝑈 ∈ CBan → 𝑈 ∈ NrmCVec )
54 5 53 ax-mp ⊢ 𝑈 ∈ NrmCVec
55 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
56 1 55 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ )
57 54 56 mpan ⊢ ( 𝑥 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ )
58 remulcl ⊢ ( ( 𝑑 ∈ ℝ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ) → ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
59 52 57 58 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
60 7 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) )
61 60 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) )
62 61 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) )
63 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
64 eqid ⊢ ( 𝑈 BLnOp 𝑊 ) = ( 𝑈 BLnOp 𝑊 )
65 1 63 64 blof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
66 54 6 65 mp3an12 ⊢ ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
67 62 66 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
68 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → 𝑥 ∈ 𝑋 )
69 67 68 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
70 63 2 nvcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
71 6 70 mpan ⊢ ( ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
72 69 71 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
73 eqid ⊢ ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
74 1 63 73 nmoxr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ* )
75 54 6 74 mp3an12 ⊢ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ* )
76 67 75 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ* )
77 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → 𝑑 ∈ ℝ )
78 1 63 73 nmogtmnf ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) → -∞ < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) )
79 54 6 78 mp3an12 ⊢ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) → -∞ < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) )
80 67 79 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → -∞ < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) )
81 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )
82 xrre ⊢ ( ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ* ∧ 𝑑 ∈ ℝ ) ∧ ( -∞ < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ )
83 76 77 80 81 82 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ )
84 57 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ )
85 remulcl ⊢ ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
86 83 84 85 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
87 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
88 1 55 2 73 64 54 6 nmblolbi ⊢ ( ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
89 62 68 88 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
90 1 55 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) )
91 54 90 mpan ⊢ ( 𝑥 ∈ 𝑋 → 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) )
92 57 91 jca ⊢ ( 𝑥 ∈ 𝑋 → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
93 92 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
94 lemul1a ⊢ ( ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ) ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
95 83 77 93 81 94 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
96 72 86 87 89 95 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
97 96 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
98 97 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
99 brralrspcev ⊢ ( ( ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
100 59 98 99 syl6an ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
101 100 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) → ( ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
102 101 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
103 51 102 impbid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )