Metamath Proof Explorer

Theorem nmoleub

Description: The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of F ( x ) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
nmoi.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmoi.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
nmoi.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
nmoi2.z ⊢ 0 = ( 0g ‘ 𝑆 )
nmoleub.1 ⊢ ( 𝜑 → 𝑆 ∈ NrmGrp )
nmoleub.2 ⊢ ( 𝜑 → 𝑇 ∈ NrmGrp )
nmoleub.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
nmoleub.4 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
nmoleub.5 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
Assertion nmoleub ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmoi.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmoi.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
4 nmoi.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
5 nmoi2.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 nmoleub.1 ⊢ ( 𝜑 → 𝑆 ∈ NrmGrp )
7 nmoleub.2 ⊢ ( 𝜑 → 𝑇 ∈ NrmGrp )
8 nmoleub.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
9 nmoleub.4 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
10 nmoleub.5 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
11 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → 𝑇 ∈ NrmGrp )
12 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
13 2 12 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
14 8 13 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
16 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → 𝑥 ∈ 𝑉 )
17 ffvelrn ⊢ ( ( 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
18 15 16 17 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
19 12 4 nmcl ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
20 11 18 19 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
21 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) → 𝑆 ∈ NrmGrp )
22 2 3 5 nmrpcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ+ )
23 22 3expb ⊢ ( ( 𝑆 ∈ NrmGrp ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ+ )
24 21 23 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ+ )
25 20 24 rerpdivcld ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ )
26 25 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ* )
27 1 nmocl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
28 6 7 8 27 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
29 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
30 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → 𝐴 ∈ ℝ* )
31 6 7 8 3jca ⊢ ( 𝜑 → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) )
33 1 2 3 4 5 nmoi2 ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ 𝐹 ) )
34 32 33 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ 𝐹 ) )
35 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
36 26 29 30 34 35 xrletrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 )
37 36 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) )
38 37 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) → ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) )
39 0le0 ⊢ 0 ≤ 0
40 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → 𝐴 ∈ ℝ )
41 40 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → 𝐴 ∈ ℂ )
42 41 mul01d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( 𝐴 · 0 ) = 0 )
43 39 42 breqtrrid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → 0 ≤ ( 𝐴 · 0 ) )
44 fveq2 ⊢ ( 𝑥 = 0 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 0 ) )
45 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
46 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
47 5 46 ghmid ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑇 ) )
48 45 47 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑇 ) )
49 44 48 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝑇 ) )
50 49 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) )
51 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → 𝑇 ∈ NrmGrp )
52 4 46 nm0 ⊢ ( 𝑇 ∈ NrmGrp → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
53 51 52 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
54 50 53 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) = 0 )
55 fveq2 ⊢ ( 𝑥 = 0 → ( 𝐿 ‘ 𝑥 ) = ( 𝐿 ‘ 0 ) )
56 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) → 𝑆 ∈ NrmGrp )
57 3 5 nm0 ⊢ ( 𝑆 ∈ NrmGrp → ( 𝐿 ‘ 0 ) = 0 )
58 56 57 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐿 ‘ 0 ) = 0 )
59 55 58 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( 𝐿 ‘ 𝑥 ) = 0 )
60 59 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) = ( 𝐴 · 0 ) )
61 43 54 60 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) )
62 61 a1d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 = 0 ) → ( ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) )
63 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → 𝑥 ≠ 0 )
64 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) → 𝑇 ∈ NrmGrp )
65 14 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
66 65 17 sylan ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
67 64 66 19 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
68 67 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
69 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → 𝐴 ∈ ℝ )
70 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑆 ∈ NrmGrp )
71 22 3expa ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ+ )
72 70 71 sylanl1 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ+ )
73 68 69 72 ledivmul2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) )
74 73 biimpd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) )
75 63 74 embantd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → ( ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) )
76 62 75 pm2.61dane ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) )
77 76 ralimdva ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) → ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) )
78 7 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑇 ∈ NrmGrp )
79 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
80 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
81 10 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 0 ≤ 𝐴 )
82 1 2 3 4 nmolb ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) )
83 70 78 79 80 81 82 syl311anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) )
84 77 83 syld ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) )
85 84 imp ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
86 85 an32s ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
87 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
88 pnfge ⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* → ( 𝑁 ‘ 𝐹 ) ≤ +∞ )
89 87 88 syl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁 ‘ 𝐹 ) ≤ +∞ )
90 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → 𝐴 = +∞ )
91 89 90 breqtrrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
92 ge0nemnf ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ≠ -∞ )
93 9 10 92 syl2anc ⊢ ( 𝜑 → 𝐴 ≠ -∞ )
94 9 93 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) )
95 xrnemnf ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
96 94 95 sylib ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
97 96 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
98 86 91 97 mpjaodan ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
99 38 98 impbida ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / ( 𝐿 ‘ 𝑥 ) ) ≤ 𝐴 ) ) )