# Metamath Proof Explorer

## Theorem nmoleub2lem3

Description: Lemma for nmoleub2a and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015) (Proof shortened by AV, 29-Sep-2021)

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 ( 𝜑𝑅 ∈ ℝ+ )
nmoleub2a.5 ( 𝜑 → ℚ ⊆ 𝐾 )
nmoleub2lem3.p · = ( ·𝑠𝑆 )
nmoleub2lem3.1 ( 𝜑𝐴 ∈ ℝ )
nmoleub2lem3.2 ( 𝜑 → 0 ≤ 𝐴 )
nmoleub2lem3.3 ( 𝜑𝐵𝑉 )
nmoleub2lem3.4 ( 𝜑𝐵 ≠ ( 0g𝑆 ) )
nmoleub2lem3.5 ( 𝜑 → ( ( 𝑟 · 𝐵 ) ∈ 𝑉 → ( ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
nmoleub2lem3.6 ( 𝜑 → ¬ ( 𝑀 ‘ ( 𝐹𝐵 ) ) ≤ ( 𝐴 · ( 𝐿𝐵 ) ) )
Assertion nmoleub2lem3 ¬ 𝜑

### 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 nmoleub2a.5 ( 𝜑 → ℚ ⊆ 𝐾 )
13 nmoleub2lem3.p · = ( ·𝑠𝑆 )
14 nmoleub2lem3.1 ( 𝜑𝐴 ∈ ℝ )
15 nmoleub2lem3.2 ( 𝜑 → 0 ≤ 𝐴 )
16 nmoleub2lem3.3 ( 𝜑𝐵𝑉 )
17 nmoleub2lem3.4 ( 𝜑𝐵 ≠ ( 0g𝑆 ) )
18 nmoleub2lem3.5 ( 𝜑 → ( ( 𝑟 · 𝐵 ) ∈ 𝑉 → ( ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
19 nmoleub2lem3.6 ( 𝜑 → ¬ ( 𝑀 ‘ ( 𝐹𝐵 ) ) ≤ ( 𝐴 · ( 𝐿𝐵 ) ) )
20 simprl ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟 )
21 qre ( 𝑟 ∈ ℚ → 𝑟 ∈ ℝ )
22 21 ad2antlr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑟 ∈ ℝ )
23 11 rpred ( 𝜑𝑅 ∈ ℝ )
24 14 23 remulcld ( 𝜑 → ( 𝐴 · 𝑅 ) ∈ ℝ )
25 8 elin1d ( 𝜑𝑇 ∈ NrmMod )
26 nlmngp ( 𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp )
27 25 26 syl ( 𝜑𝑇 ∈ NrmGrp )
28 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
29 2 28 lmhmf ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
30 9 29 syl ( 𝜑𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
31 30 16 ffvelrnd ( 𝜑 → ( 𝐹𝐵 ) ∈ ( Base ‘ 𝑇 ) )
32 28 4 nmcl ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹𝐵 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ )
33 27 31 32 syl2anc ( 𝜑 → ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ )
34 0red ( 𝜑 → 0 ∈ ℝ )
35 7 elin1d ( 𝜑𝑆 ∈ NrmMod )
36 nlmngp ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp )
37 35 36 syl ( 𝜑𝑆 ∈ NrmGrp )
38 2 3 nmcl ( ( 𝑆 ∈ NrmGrp ∧ 𝐵𝑉 ) → ( 𝐿𝐵 ) ∈ ℝ )
39 37 16 38 syl2anc ( 𝜑 → ( 𝐿𝐵 ) ∈ ℝ )
40 14 39 remulcld ( 𝜑 → ( 𝐴 · ( 𝐿𝐵 ) ) ∈ ℝ )
41 2 3 nmge0 ( ( 𝑆 ∈ NrmGrp ∧ 𝐵𝑉 ) → 0 ≤ ( 𝐿𝐵 ) )
42 37 16 41 syl2anc ( 𝜑 → 0 ≤ ( 𝐿𝐵 ) )
43 14 39 15 42 mulge0d ( 𝜑 → 0 ≤ ( 𝐴 · ( 𝐿𝐵 ) ) )
44 40 33 ltnled ( 𝜑 → ( ( 𝐴 · ( 𝐿𝐵 ) ) < ( 𝑀 ‘ ( 𝐹𝐵 ) ) ↔ ¬ ( 𝑀 ‘ ( 𝐹𝐵 ) ) ≤ ( 𝐴 · ( 𝐿𝐵 ) ) ) )
45 19 44 mpbird ( 𝜑 → ( 𝐴 · ( 𝐿𝐵 ) ) < ( 𝑀 ‘ ( 𝐹𝐵 ) ) )
46 34 40 33 43 45 lelttrd ( 𝜑 → 0 < ( 𝑀 ‘ ( 𝐹𝐵 ) ) )
47 33 46 elrpd ( 𝜑 → ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ+ )
48 24 47 rerpdivcld ( 𝜑 → ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ∈ ℝ )
49 48 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ∈ ℝ )
50 9 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
51 12 sselda ( ( 𝜑𝑟 ∈ ℚ ) → 𝑟𝐾 )
52 51 adantr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑟𝐾 )
53 16 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝐵𝑉 )
54 eqid ( ·𝑠𝑇 ) = ( ·𝑠𝑇 )
55 5 6 2 13 54 lmhmlin ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑟𝐾𝐵𝑉 ) → ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) = ( 𝑟 ( ·𝑠𝑇 ) ( 𝐹𝐵 ) ) )
56 50 52 53 55 syl3anc ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) = ( 𝑟 ( ·𝑠𝑇 ) ( 𝐹𝐵 ) ) )
57 56 fveq2d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) = ( 𝑀 ‘ ( 𝑟 ( ·𝑠𝑇 ) ( 𝐹𝐵 ) ) ) )
58 25 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑇 ∈ NrmMod )
59 eqid ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
60 5 59 lmhmsca ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = 𝐺 )
61 50 60 syl ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( Scalar ‘ 𝑇 ) = 𝐺 )
62 61 fveq2d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ 𝐺 ) )
63 62 6 syl6eqr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = 𝐾 )
64 52 63 eleqtrrd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
65 31 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝐹𝐵 ) ∈ ( Base ‘ 𝑇 ) )
66 eqid ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
67 eqid ( norm ‘ ( Scalar ‘ 𝑇 ) ) = ( norm ‘ ( Scalar ‘ 𝑇 ) )
68 28 4 54 59 66 67 nmvs ( ( 𝑇 ∈ NrmMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ ( 𝐹𝐵 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝑟 ( ·𝑠𝑇 ) ( 𝐹𝐵 ) ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
69 58 64 65 68 syl3anc ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝑟 ( ·𝑠𝑇 ) ( 𝐹𝐵 ) ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
70 61 fveq2d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( norm ‘ ( Scalar ‘ 𝑇 ) ) = ( norm ‘ 𝐺 ) )
71 70 fveq1d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) = ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) )
72 7 elin2d ( 𝜑𝑆 ∈ ℂMod )
73 72 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑆 ∈ ℂMod )
74 5 6 clmabs ( ( 𝑆 ∈ ℂMod ∧ 𝑟𝐾 ) → ( abs ‘ 𝑟 ) = ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) )
75 73 52 74 syl2anc ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( abs ‘ 𝑟 ) = ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) )
76 0red ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 0 ∈ ℝ )
77 11 rpge0d ( 𝜑 → 0 ≤ 𝑅 )
78 14 23 15 77 mulge0d ( 𝜑 → 0 ≤ ( 𝐴 · 𝑅 ) )
79 divge0 ( ( ( ( 𝐴 · 𝑅 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝑅 ) ) ∧ ( ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ) → 0 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
80 24 78 33 46 79 syl22anc ( 𝜑 → 0 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
81 80 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 0 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
82 76 49 22 81 20 lelttrd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 0 < 𝑟 )
83 76 22 82 ltled ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 0 ≤ 𝑟 )
84 22 83 absidd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( abs ‘ 𝑟 ) = 𝑟 )
85 75 84 eqtr3d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) = 𝑟 )
86 71 85 eqtrd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) = 𝑟 )
87 86 oveq1d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) = ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
88 57 69 87 3eqtrd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) = ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
89 88 oveq1d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) = ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) / 𝑅 ) )
90 2 5 13 6 clmvscl ( ( 𝑆 ∈ ℂMod ∧ 𝑟𝐾𝐵𝑉 ) → ( 𝑟 · 𝐵 ) ∈ 𝑉 )
91 73 52 53 90 syl3anc ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑟 · 𝐵 ) ∈ 𝑉 )
92 35 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑆 ∈ NrmMod )
93 eqid ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
94 2 3 13 5 6 93 nmvs ( ( 𝑆 ∈ NrmMod ∧ 𝑟𝐾𝐵𝑉 ) → ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) = ( ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) · ( 𝐿𝐵 ) ) )
95 92 52 53 94 syl3anc ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) = ( ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) · ( 𝐿𝐵 ) ) )
96 85 oveq1d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) · ( 𝐿𝐵 ) ) = ( 𝑟 · ( 𝐿𝐵 ) ) )
97 95 96 eqtrd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) = ( 𝑟 · ( 𝐿𝐵 ) ) )
98 simprr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) )
99 23 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑅 ∈ ℝ )
100 eqid ( 0g𝑆 ) = ( 0g𝑆 )
101 2 3 100 nmrpcl ( ( 𝑆 ∈ NrmGrp ∧ 𝐵𝑉𝐵 ≠ ( 0g𝑆 ) ) → ( 𝐿𝐵 ) ∈ ℝ+ )
102 37 16 17 101 syl3anc ( 𝜑 → ( 𝐿𝐵 ) ∈ ℝ+ )
103 102 rpregt0d ( 𝜑 → ( ( 𝐿𝐵 ) ∈ ℝ ∧ 0 < ( 𝐿𝐵 ) ) )
104 103 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝐿𝐵 ) ∈ ℝ ∧ 0 < ( 𝐿𝐵 ) ) )
105 ltmuldiv ( ( 𝑟 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ( ( 𝐿𝐵 ) ∈ ℝ ∧ 0 < ( 𝐿𝐵 ) ) ) → ( ( 𝑟 · ( 𝐿𝐵 ) ) < 𝑅𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) )
106 22 99 104 105 syl3anc ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝑟 · ( 𝐿𝐵 ) ) < 𝑅𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) )
107 98 106 mpbird ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑟 · ( 𝐿𝐵 ) ) < 𝑅 )
108 97 107 eqbrtrd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) < 𝑅 )
109 18 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝑟 · 𝐵 ) ∈ 𝑉 → ( ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
110 91 108 109 mp2d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 )
111 89 110 eqbrtrrd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 )
112 33 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ )
113 22 112 remulcld ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ∈ ℝ )
114 14 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝐴 ∈ ℝ )
115 11 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑅 ∈ ℝ+ )
116 113 114 115 ledivmul2d ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 ↔ ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ≤ ( 𝐴 · 𝑅 ) ) )
117 111 116 mpbid ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ≤ ( 𝐴 · 𝑅 ) )
118 114 99 remulcld ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝐴 · 𝑅 ) ∈ ℝ )
119 33 46 jca ( 𝜑 → ( ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
120 119 ad2antrr ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
121 lemuldiv ( ( 𝑟 ∈ ℝ ∧ ( 𝐴 · 𝑅 ) ∈ ℝ ∧ ( ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ) → ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ≤ ( 𝐴 · 𝑅 ) ↔ 𝑟 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ) )
122 22 118 120 121 syl3anc ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ≤ ( 𝐴 · 𝑅 ) ↔ 𝑟 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ) )
123 117 122 mpbid ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → 𝑟 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
124 22 49 123 lensymd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ¬ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟 )
125 20 124 pm2.21dd ( ( ( 𝜑𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝐹𝐵 ) ) ≤ ( 𝐴 · ( 𝐿𝐵 ) ) )
126 23 102 rerpdivcld ( 𝜑 → ( 𝑅 / ( 𝐿𝐵 ) ) ∈ ℝ )
127 14 recnd ( 𝜑𝐴 ∈ ℂ )
128 23 recnd ( 𝜑𝑅 ∈ ℂ )
129 39 recnd ( 𝜑 → ( 𝐿𝐵 ) ∈ ℂ )
130 mulass ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( 𝐿𝐵 ) ∈ ℂ ) → ( ( 𝐴 · 𝑅 ) · ( 𝐿𝐵 ) ) = ( 𝐴 · ( 𝑅 · ( 𝐿𝐵 ) ) ) )
131 mul12 ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( 𝐿𝐵 ) ∈ ℂ ) → ( 𝐴 · ( 𝑅 · ( 𝐿𝐵 ) ) ) = ( 𝑅 · ( 𝐴 · ( 𝐿𝐵 ) ) ) )
132 130 131 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( 𝐿𝐵 ) ∈ ℂ ) → ( ( 𝐴 · 𝑅 ) · ( 𝐿𝐵 ) ) = ( 𝑅 · ( 𝐴 · ( 𝐿𝐵 ) ) ) )
133 127 128 129 132 syl3anc ( 𝜑 → ( ( 𝐴 · 𝑅 ) · ( 𝐿𝐵 ) ) = ( 𝑅 · ( 𝐴 · ( 𝐿𝐵 ) ) ) )
134 40 33 11 45 ltmul2dd ( 𝜑 → ( 𝑅 · ( 𝐴 · ( 𝐿𝐵 ) ) ) < ( 𝑅 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
135 133 134 eqbrtrd ( 𝜑 → ( ( 𝐴 · 𝑅 ) · ( 𝐿𝐵 ) ) < ( 𝑅 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) )
136 lt2mul2div ( ( ( ( 𝐴 · 𝑅 ) ∈ ℝ ∧ ( ( 𝐿𝐵 ) ∈ ℝ ∧ 0 < ( 𝐿𝐵 ) ) ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝑀 ‘ ( 𝐹𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ) ) → ( ( ( 𝐴 · 𝑅 ) · ( 𝐿𝐵 ) ) < ( 𝑅 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ↔ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < ( 𝑅 / ( 𝐿𝐵 ) ) ) )
137 24 103 23 119 136 syl22anc ( 𝜑 → ( ( ( 𝐴 · 𝑅 ) · ( 𝐿𝐵 ) ) < ( 𝑅 · ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ↔ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < ( 𝑅 / ( 𝐿𝐵 ) ) ) )
138 135 137 mpbid ( 𝜑 → ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < ( 𝑅 / ( 𝐿𝐵 ) ) )
139 qbtwnre ( ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) ∈ ℝ ∧ ( 𝑅 / ( 𝐿𝐵 ) ) ∈ ℝ ∧ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < ( 𝑅 / ( 𝐿𝐵 ) ) ) → ∃ 𝑟 ∈ ℚ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) )
140 48 126 138 139 syl3anc ( 𝜑 → ∃ 𝑟 ∈ ℚ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹𝐵 ) ) ) < 𝑟𝑟 < ( 𝑅 / ( 𝐿𝐵 ) ) ) )
141 125 140 r19.29a ( 𝜑 → ( 𝑀 ‘ ( 𝐹𝐵 ) ) ≤ ( 𝐴 · ( 𝐿𝐵 ) ) )
142 141 19 pm2.65i ¬ 𝜑