Theorem nmoleub2lem2

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	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
	nmoleub2a.5	⊢ ( 𝜑 → ℚ ⊆ 𝐾 )
	nmoleub2lem2.6	⊢ ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
	nmoleub2lem2.7	⊢ ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 ) )
Assertion	nmoleub2lem2	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )

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		nmoleub2lem2.6	⊢ ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
14		nmoleub2lem2.7	⊢ ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 ) )
15		lmghm	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
16		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
17		eqid	⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
18	16 17	ghmid	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
19	9 15 18	3syl	⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
20	19	fveq2d	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) = ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) )
21	8	elin1d	⊢ ( 𝜑 → 𝑇 ∈ NrmMod )
22		nlmngp	⊢ ( 𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp )
23	4 17	nm0	⊢ ( 𝑇 ∈ NrmGrp → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
24	21 22 23	3syl	⊢ ( 𝜑 → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
25	20 24	eqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) = 0 )
26	25	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) = 0 )
27	26	oveq1d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) / 𝑅 ) = ( 0 / 𝑅 ) )
28	11	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 𝑅 ∈ ℝ+ )
29	28	rpcnd	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 𝑅 ∈ ℂ )
30	28	rpne0d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 𝑅 ≠ 0 )
31	29 30	div0d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( 0 / 𝑅 ) = 0 )
32	27 31	eqtrd	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) / 𝑅 ) = 0 )
33	7	elin1d	⊢ ( 𝜑 → 𝑆 ∈ NrmMod )
34		nlmngp	⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp )
35	3 16	nm0	⊢ ( 𝑆 ∈ NrmGrp → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) = 0 )
36	33 34 35	3syl	⊢ ( 𝜑 → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) = 0 )
37	36	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) = 0 )
38	28	rpgt0d	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 0 < 𝑅 )
39	37 38	eqbrtrd	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) < 𝑅 )
40		fveq2	⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( 𝐿 ‘ 𝑥 ) = ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) )
41	40	breq1d	⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( ( 𝐿 ‘ 𝑥 ) < 𝑅 ↔ ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) < 𝑅 ) )
42		2fveq3	⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) )
43	42	oveq1d	⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) = ( ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) / 𝑅 ) )
44	43	breq1d	⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ↔ ( ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) / 𝑅 ) ≤ 𝐴 ) )
45	41 44	imbi12d	⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ↔ ( ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
46	33 34	syl	⊢ ( 𝜑 → 𝑆 ∈ NrmGrp )
47	2 3	nmcl	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
48	46 47	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐿 ‘ 𝑥 ) ∈ ℝ )
49	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑅 ∈ ℝ+ )
50	49	rpred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑅 ∈ ℝ )
51	48 50 14	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 ) )
52	51	imim1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) → ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )
53	52	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) → ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )
54	53	imp	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) )
55		ngpgrp	⊢ ( 𝑆 ∈ NrmGrp → 𝑆 ∈ Grp )
56	2 16	grpidcl	⊢ ( 𝑆 ∈ Grp → ( 0g ‘ 𝑆 ) ∈ 𝑉 )
57	46 55 56	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ 𝑉 )
58	57	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( 0g ‘ 𝑆 ) ∈ 𝑉 )
59	45 54 58	rspcdva	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( ( 𝐿 ‘ ( 0g ‘ 𝑆 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) / 𝑅 ) ≤ 𝐴 ) )
60	39 59	mpd	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) ) / 𝑅 ) ≤ 𝐴 )
61	32 60	eqbrtrrd	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) → 0 ≤ 𝐴 )
62		simp-4l	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝜑 )
63	62 7	syl	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝑆 ∈ ( NrmMod ∩ ℂMod ) )
64	62 8	syl	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝑇 ∈ ( NrmMod ∩ ℂMod ) )
65	62 9	syl	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
66	62 10	syl	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝐴 ∈ ℝ* )
67	62 11	syl	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝑅 ∈ ℝ+ )
68	62 12	syl	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → ℚ ⊆ 𝐾 )
69		eqid	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
70		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝐴 ∈ ℝ )
71	61	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 0 ≤ 𝐴 )
72		simplrl	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝑦 ∈ 𝑉 )
73		simplrr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → 𝑦 ≠ ( 0g ‘ 𝑆 ) )
74	54	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) )
75		fveq2	⊢ ( 𝑥 = ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( 𝐿 ‘ 𝑥 ) = ( 𝐿 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) )
76	75	breq1d	⊢ ( 𝑥 = ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( 𝐿 ‘ 𝑥 ) < 𝑅 ↔ ( 𝐿 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) < 𝑅 ) )
77		2fveq3	⊢ ( 𝑥 = ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) )
78	77	oveq1d	⊢ ( 𝑥 = ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) = ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) )
79	78	breq1d	⊢ ( 𝑥 = ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ↔ ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) ≤ 𝐴 ) )
80	76 79	imbi12d	⊢ ( 𝑥 = ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) → ( ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ↔ ( ( 𝐿 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
81	80	rspccv	⊢ ( ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) → ( ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ 𝑉 → ( ( 𝐿 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
82	74 81	syl	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → ( ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ 𝑉 → ( ( 𝐿 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑧 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
83		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) → ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) )
84	1 2 3 4 5 6 63 64 65 66 67 68 69 70 71 72 73 82 83	nmoleub2lem3	⊢ ¬ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) )
85		iman	⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) ↔ ¬ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) ∧ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) ) )
86	84 85	mpbir	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑦 ) ) )
87	48 50 13	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
88	1 2 3 4 5 6 7 8 9 10 11 61 86 87	nmoleub2lem	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) 𝑂 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )