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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 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	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( 𝜓 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )