Metamath Proof Explorer

Theorem nmoleub2lem

Description: Lemma for nmoleub2a and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015)

Ref Expression
Hypotheses nmoleub2.n ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
nmoleub2.v ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmoleub2.l ⊢ 𝐿 = ( norm ‘ 𝑆 )
nmoleub2.m ⊢ 𝑀 = ( norm ‘ 𝑇 )
nmoleub2.g ⊢ 𝐺 = ( Scalar ‘ 𝑆 )
nmoleub2.w ⊢ 𝐾 = ( Base ‘ 𝐺 )
nmoleub2.s ⊢ ( 𝜑 → 𝑆 ∈ ( NrmMod ∩ ℂMod ) )
nmoleub2.t ⊢ ( 𝜑 → 𝑇 ∈ ( NrmMod ∩ ℂMod ) )
nmoleub2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
nmoleub2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
nmoleub2.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
nmoleub2lem.5 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 0 ≤ 𝐴 )
nmoleub2lem.6 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) )
nmoleub2lem.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝜓 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
Assertion nmoleub2lem ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmoleub2.n ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmoleub2.v ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmoleub2.l ⊢ 𝐿 = ( norm ‘ 𝑆 )
4 nmoleub2.m ⊢ 𝑀 = ( norm ‘ 𝑇 )
5 nmoleub2.g ⊢ 𝐺 = ( Scalar ‘ 𝑆 )
6 nmoleub2.w ⊢ 𝐾 = ( Base ‘ 𝐺 )
7 nmoleub2.s ⊢ ( 𝜑 → 𝑆 ∈ ( NrmMod ∩ ℂMod ) )
8 nmoleub2.t ⊢ ( 𝜑 → 𝑇 ∈ ( NrmMod ∩ ℂMod ) )
9 nmoleub2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
10 nmoleub2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
11 nmoleub2.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
12 nmoleub2lem.5 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 0 ≤ 𝐴 )
13 nmoleub2lem.6 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) )
14 nmoleub2lem.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝜓 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
15 14 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝜓 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
16 8 elin1d ⊢ ( 𝜑 → 𝑇 ∈ NrmMod )
17 nlmngp ⊢ ( 𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp )
18 16 17 syl ⊢ ( 𝜑 → 𝑇 ∈ NrmGrp )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝑇 ∈ NrmGrp )
20 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
21 2 20 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
22 9 21 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
24 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝑥 ∈ 𝑉 )
25 23 24 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
26 20 4 nmcl ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
27 19 25 26 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
28 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝑅 ∈ ℝ+ )
29 27 28 rerpdivcld ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ∈ ℝ )
30 29 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ∈ ℝ* )
31 7 elin1d ⊢ ( 𝜑 → 𝑆 ∈ NrmMod )
32 nlmngp ⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp )
33 31 32 syl ⊢ ( 𝜑 → 𝑆 ∈ NrmGrp )
34 lmghm ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
35 9 34 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
36 1 nmocl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
37 33 18 35 36 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
39 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝐴 ∈ ℝ* )
40 28 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝑅 ∈ ℝ )
41 rexmul ⊢ ( ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ·e 𝑅 ) = ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) · 𝑅 ) )
42 29 40 41 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ·e 𝑅 ) = ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) · 𝑅 ) )
43 27 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
44 40 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝑅 ∈ ℂ )
45 28 rpne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝑅 ≠ 0 )
46 43 44 45 divcan1d ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) · 𝑅 ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) )
47 42 46 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ·e 𝑅 ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) )
48 27 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ* )
49 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝑆 ∈ NrmGrp )
50 2 3 nmcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
51 49 24 50 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
52 51 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ* )
53 38 52 xmulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑥 ) ) ∈ ℝ* )
54 28 rpxrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝑅 ∈ ℝ* )
55 38 54 xmulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( 𝑁 ‘ 𝐹 ) ·e 𝑅 ) ∈ ℝ* )
56 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
57 1 2 3 4 nmoix ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑥 ) ) )
58 49 19 56 24 57 syl31anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑥 ) ) )
59 1 nmoge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
60 33 18 35 59 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
61 37 60 jca ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝐹 ) ) )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝐹 ) ) )
63 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 )
64 xlemul2a ⊢ ( ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝐹 ) ) ) ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) → ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e 𝑅 ) )
65 52 54 62 63 64 syl31anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e 𝑅 ) )
66 48 53 55 58 65 xrletrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e 𝑅 ) )
67 47 66 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ·e 𝑅 ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e 𝑅 ) )
68 xlemul1 ⊢ ( ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ∈ ℝ* ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ 𝑅 ∈ ℝ+ ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ ( 𝑁 ‘ 𝐹 ) ↔ ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ·e 𝑅 ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e 𝑅 ) ) )
69 30 38 28 68 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ ( 𝑁 ‘ 𝐹 ) ↔ ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ·e 𝑅 ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e 𝑅 ) ) )
70 67 69 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ ( 𝑁 ‘ 𝐹 ) )
71 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
72 30 38 39 70 71 xrletrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 )
73 72 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) )
74 15 73 syld ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) )
75 74 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) → ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) )
76 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
77 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) → 𝑆 ∈ NrmGrp )
78 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) → 𝑇 ∈ NrmGrp )
79 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
80 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
81 12 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) → 0 ≤ 𝐴 )
82 1 2 3 4 76 77 78 79 80 81 13 nmolb2d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
83 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
84 pnfge ⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* → ( 𝑁 ‘ 𝐹 ) ≤ +∞ )
85 83 84 syl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁 ‘ 𝐹 ) ≤ +∞ )
86 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → 𝐴 = +∞ )
87 85 86 breqtrrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
88 10 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 𝐴 ∈ ℝ* )
89 ge0nemnf ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ≠ -∞ )
90 88 12 89 syl2anc ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 𝐴 ≠ -∞ )
91 88 90 jca ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) )
92 xrnemnf ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
93 91 92 sylib ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
94 82 87 93 mpjaodan ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )
95 75 94 impbida ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )