Metamath Proof Explorer

Theorem nmoleub3

Description: The operator norm is the supremum of the value of a linear operator on the unit sphere. (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 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
nmoleub3.5 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
nmoleub3.6 ⊢ ( 𝜑 → ℝ ⊆ 𝐾 )
Assertion nmoleub3 ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )

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 nmoleub3.5 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
13 nmoleub3.6 ⊢ ( 𝜑 → ℝ ⊆ 𝐾 )
14 12 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 0 ≤ 𝐴 )
15 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
16 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ℝ ⊆ 𝐾 )
17 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑅 ∈ ℝ+ )
18 7 elin1d ⊢ ( 𝜑 → 𝑆 ∈ NrmMod )
19 18 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑆 ∈ NrmMod )
20 nlmngp ⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp )
21 19 20 syl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑆 ∈ NrmGrp )
22 simprl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑦 ∈ 𝑉 )
23 simprr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑦 ≠ ( 0g ‘ 𝑆 ) )
24 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
25 2 3 24 nmrpcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐿 ‘ 𝑦 ) ∈ ℝ+ )
26 21 22 23 25 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐿 ‘ 𝑦 ) ∈ ℝ+ )
27 17 26 rpdivcld ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ ℝ+ )
28 27 rpred ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ ℝ )
29 16 28 sseldd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ 𝐾 )
30 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
31 eqid ⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
32 5 6 2 30 31 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
33 15 29 22 32 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
34 33 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑀 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) )
35 8 elin1d ⊢ ( 𝜑 → 𝑇 ∈ NrmMod )
36 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑇 ∈ NrmMod )
37 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
38 5 37 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = 𝐺 )
39 15 38 syl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( Scalar ‘ 𝑇 ) = 𝐺 )
40 39 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ 𝐺 ) )
41 40 6 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = 𝐾 )
42 29 41 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
43 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
44 2 43 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
45 15 44 syl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
46 45 22 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) )
47 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
48 eqid ⊢ ( norm ‘ ( Scalar ‘ 𝑇 ) ) = ( norm ‘ ( Scalar ‘ 𝑇 ) )
49 43 4 31 37 47 48 nmvs ⊢ ( ( 𝑇 ∈ NrmMod ∧ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
50 36 42 46 49 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
51 39 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( norm ‘ ( Scalar ‘ 𝑇 ) ) = ( norm ‘ 𝐺 ) )
52 51 fveq1d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) )
53 7 elin2d ⊢ ( 𝜑 → 𝑆 ∈ ℂMod )
54 53 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑆 ∈ ℂMod )
55 5 6 clmabs ⊢ ( ( 𝑆 ∈ ℂMod ∧ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ 𝐾 ) → ( abs ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) )
56 54 29 55 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( abs ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) )
57 27 rpge0d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 0 ≤ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) )
58 28 57 absidd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( abs ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) = ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) )
59 56 58 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝐺 ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) = ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) )
60 52 59 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) = ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) )
61 60 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
62 34 50 61 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
63 62 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) = ( ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ) / 𝑅 ) )
64 27 rpcnd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ ℂ )
65 nlmngp ⊢ ( 𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp )
66 36 65 syl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑇 ∈ NrmGrp )
67 43 4 nmcl ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
68 66 46 67 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
69 68 recnd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℂ )
70 17 rpcnd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑅 ∈ ℂ )
71 17 rpne0d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑅 ≠ 0 )
72 64 69 70 71 divassd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ) / 𝑅 ) = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) · ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) / 𝑅 ) ) )
73 26 rpcnd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐿 ‘ 𝑦 ) ∈ ℂ )
74 26 rpne0d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐿 ‘ 𝑦 ) ≠ 0 )
75 69 70 73 71 74 dmdcand ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) · ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) / 𝑅 ) ) = ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) / ( 𝐿 ‘ 𝑦 ) ) )
76 63 72 75 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) = ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) / ( 𝐿 ‘ 𝑦 ) ) )
77 eqid ⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
78 2 3 30 5 6 77 nmvs ⊢ ( ( 𝑆 ∈ NrmMod ∧ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐿 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( ( ( norm ‘ 𝐺 ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) · ( 𝐿 ‘ 𝑦 ) ) )
79 19 29 22 78 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐿 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( ( ( norm ‘ 𝐺 ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) · ( 𝐿 ‘ 𝑦 ) ) )
80 59 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( norm ‘ 𝐺 ) ‘ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ) · ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) · ( 𝐿 ‘ 𝑦 ) ) )
81 70 73 74 divcan1d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) · ( 𝐿 ‘ 𝑦 ) ) = 𝑅 )
82 79 80 81 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐿 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = 𝑅 )
83 fveqeq2 ⊢ ( 𝑥 = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( 𝐿 ‘ 𝑥 ) = 𝑅 ↔ ( 𝐿 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = 𝑅 ) )
84 2fveq3 ⊢ ( 𝑥 = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) )
85 84 oveq1d ⊢ ( 𝑥 = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) = ( ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) )
86 85 breq1d ⊢ ( 𝑥 = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ↔ ( ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) ≤ 𝐴 ) )
87 83 86 imbi12d ⊢ ( 𝑥 = ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ↔ ( ( 𝐿 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
88 simpllr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) )
89 2 5 30 6 clmvscl ⊢ ( ( 𝑆 ∈ ℂMod ∧ ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ 𝑉 )
90 54 29 22 89 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ 𝑉 )
91 87 88 90 rspcdva ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐿 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) ≤ 𝐴 ) )
92 82 91 mpd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( ( 𝑅 / ( 𝐿 ‘ 𝑦 ) ) ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) ≤ 𝐴 )
93 76 92 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) / ( 𝐿 ‘ 𝑦 ) ) ≤ 𝐴 )
94 simplr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐴 ∈ ℝ )
95 68 94 26 ledivmul2d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) / ( 𝐿 ‘ 𝑦 ) ) ≤ 𝐴 ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) )
96 93 95 mpbid ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) )
97 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑅 ∈ ℝ+ )
98 97 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑅 ∈ ℝ )
99 98 leidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑅 ≤ 𝑅 )
100 breq1 ⊢ ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ↔ 𝑅 ≤ 𝑅 ) )
101 99 100 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
102 1 2 3 4 5 6 7 8 9 10 11 14 96 101 nmoleub2lem ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) = 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )