This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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