Theorem ply1divex

Description: Lemma for ply1divalg : existence part. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	ply1divalg.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1divalg.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	ply1divalg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1divalg.m	⊢ − = ( -g ‘ 𝑃 )
	ply1divalg.z	⊢ 0 = ( 0g ‘ 𝑃 )
	ply1divalg.t	⊢ ∙ = ( .r ‘ 𝑃 )
	ply1divalg.r1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1divalg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	ply1divalg.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	ply1divalg.g2	⊢ ( 𝜑 → 𝐺 ≠ 0 )
	ply1divex.o	⊢ 1 = ( 1r ‘ 𝑅 )
	ply1divex.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ply1divex.u	⊢ · = ( .r ‘ 𝑅 )
	ply1divex.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐾 )
	ply1divex.g3	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · 𝐼 ) = 1 )
Assertion	ply1divex	⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1divalg.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		ply1divalg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		ply1divalg.m	⊢ − = ( -g ‘ 𝑃 )
5		ply1divalg.z	⊢ 0 = ( 0g ‘ 𝑃 )
6		ply1divalg.t	⊢ ∙ = ( .r ‘ 𝑃 )
7		ply1divalg.r1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		ply1divalg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		ply1divalg.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		ply1divalg.g2	⊢ ( 𝜑 → 𝐺 ≠ 0 )
11		ply1divex.o	⊢ 1 = ( 1r ‘ 𝑅 )
12		ply1divex.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
13		ply1divex.u	⊢ · = ( .r ‘ 𝑅 )
14		ply1divex.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐾 )
15		ply1divex.g3	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · 𝐼 ) = 1 )
16		fveq2	⊢ ( 𝐹 = 0 → ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ 0 ) )
17	16	breq1d	⊢ ( 𝐹 = 0 → ( ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ↔ ( 𝐷 ‘ 0 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
18	17	rexbidv	⊢ ( 𝐹 = 0 → ( ∃ 𝑑 ∈ ℕ0 ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝐷 ‘ 0 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
19		nnssnn0	⊢ ℕ ⊆ ℕ0
20	7	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → 𝑅 ∈ Ring )
21	8	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → 𝐹 ∈ 𝐵 )
22		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → 𝐹 ≠ 0 )
23	2 1 5 3	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
24	20 21 22 23	syl3anc	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
25	24	nn0red	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ )
26	2 1 5 3	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
27	7 9 10 26	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
28	27	nn0red	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℝ )
30	25 29	resubcld	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) ∈ ℝ )
31		arch	⊢ ( ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) ∈ ℝ → ∃ 𝑑 ∈ ℕ ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) < 𝑑 )
32	30 31	syl	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → ∃ 𝑑 ∈ ℕ ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) < 𝑑 )
33		ssrexv	⊢ ( ℕ ⊆ ℕ0 → ( ∃ 𝑑 ∈ ℕ ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) < 𝑑 → ∃ 𝑑 ∈ ℕ0 ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) < 𝑑 ) )
34	19 32 33	mpsyl	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → ∃ 𝑑 ∈ ℕ0 ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) < 𝑑 )
35	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ )
36	28	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℝ )
37		nn0re	⊢ ( 𝑑 ∈ ℕ0 → 𝑑 ∈ ℝ )
38	37	adantl	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑑 ∈ ℝ )
39	35 36 38	ltsubadd2d	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) < 𝑑 ↔ ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
40	39	biimpd	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) < 𝑑 → ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
41	40	reximdva	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑑 ∈ ℕ0 ( ( 𝐷 ‘ 𝐹 ) − ( 𝐷 ‘ 𝐺 ) ) < 𝑑 → ∃ 𝑑 ∈ ℕ0 ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
42	34 41	mpd	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 0 ) → ∃ 𝑑 ∈ ℕ0 ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
43		0nn0	⊢ 0 ∈ ℕ0
44	2 1 5	deg1z	⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ 0 ) = -∞ )
45	7 44	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) = -∞ )
46		0re	⊢ 0 ∈ ℝ
47		readdcl	⊢ ( ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝐷 ‘ 𝐺 ) + 0 ) ∈ ℝ )
48	28 46 47	sylancl	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐺 ) + 0 ) ∈ ℝ )
49	48	mnfltd	⊢ ( 𝜑 → -∞ < ( ( 𝐷 ‘ 𝐺 ) + 0 ) )
50	45 49	eqbrtrd	⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) )
51		oveq2	⊢ ( 𝑑 = 0 → ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) = ( ( 𝐷 ‘ 𝐺 ) + 0 ) )
52	51	breq2d	⊢ ( 𝑑 = 0 → ( ( 𝐷 ‘ 0 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ↔ ( 𝐷 ‘ 0 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) ) )
53	52	rspcev	⊢ ( ( 0 ∈ ℕ0 ∧ ( 𝐷 ‘ 0 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) ) → ∃ 𝑑 ∈ ℕ0 ( 𝐷 ‘ 0 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
54	43 50 53	sylancr	⊢ ( 𝜑 → ∃ 𝑑 ∈ ℕ0 ( 𝐷 ‘ 0 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
55	18 42 54	pm2.61ne	⊢ ( 𝜑 → ∃ 𝑑 ∈ ℕ0 ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
56		fveq2	⊢ ( 𝑓 = 𝐹 → ( 𝐷 ‘ 𝑓 ) = ( 𝐷 ‘ 𝐹 ) )
57	56	breq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ↔ ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
58		fvoveq1	⊢ ( 𝑓 = 𝐹 → ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) = ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) )
59	58	breq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
60	59	rexbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
61	57 60	imbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
62		oveq2	⊢ ( 𝑎 = 0 → ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) = ( ( 𝐷 ‘ 𝐺 ) + 0 ) )
63	62	breq2d	⊢ ( 𝑎 = 0 → ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) ↔ ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) ) )
64	63	imbi1d	⊢ ( 𝑎 = 0 → ( ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
65	64	ralbidv	⊢ ( 𝑎 = 0 → ( ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
66	65	imbi2d	⊢ ( 𝑎 = 0 → ( ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) )
67		oveq2	⊢ ( 𝑎 = 𝑑 → ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) = ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
68	67	breq2d	⊢ ( 𝑎 = 𝑑 → ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) ↔ ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
69	68	imbi1d	⊢ ( 𝑎 = 𝑑 → ( ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
70	69	ralbidv	⊢ ( 𝑎 = 𝑑 → ( ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
71	70	imbi2d	⊢ ( 𝑎 = 𝑑 → ( ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) )
72		oveq2	⊢ ( 𝑎 = ( 𝑑 + 1 ) → ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) = ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) )
73	72	breq2d	⊢ ( 𝑎 = ( 𝑑 + 1 ) → ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) ↔ ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) )
74	73	imbi1d	⊢ ( 𝑎 = ( 𝑑 + 1 ) → ( ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
75	74	ralbidv	⊢ ( 𝑎 = ( 𝑑 + 1 ) → ( ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
76	75	imbi2d	⊢ ( 𝑎 = ( 𝑑 + 1 ) → ( ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑎 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) )
77	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
78	7 77	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
79	3 5	ring0cl	⊢ ( 𝑃 ∈ Ring → 0 ∈ 𝐵 )
80	78 79	syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
81	80	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) ) → 0 ∈ 𝐵 )
82	3 6 5	ringrz	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 ∙ 0 ) = 0 )
83	78 9 82	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∙ 0 ) = 0 )
84	83	oveq2d	⊢ ( 𝜑 → ( 𝑓 − ( 𝐺 ∙ 0 ) ) = ( 𝑓 − 0 ) )
85	84	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑓 − ( 𝐺 ∙ 0 ) ) = ( 𝑓 − 0 ) )
86		ringgrp	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
87	78 86	syl	⊢ ( 𝜑 → 𝑃 ∈ Grp )
88	3 5 4	grpsubid1	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑓 ∈ 𝐵 ) → ( 𝑓 − 0 ) = 𝑓 )
89	87 88	sylan	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝑓 − 0 ) = 𝑓 )
90	85 89	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → 𝑓 = ( 𝑓 − ( 𝐺 ∙ 0 ) ) )
91	90	fveq2d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑓 ) = ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 0 ) ) ) )
92	27	nn0cnd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℂ )
93	92	addridd	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐺 ) + 0 ) = ( 𝐷 ‘ 𝐺 ) )
94	93	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐺 ) + 0 ) = ( 𝐷 ‘ 𝐺 ) )
95	91 94	breq12d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) ↔ ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 0 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
96	95	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) ) → ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 0 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
97		oveq2	⊢ ( 𝑞 = 0 → ( 𝐺 ∙ 𝑞 ) = ( 𝐺 ∙ 0 ) )
98	97	oveq2d	⊢ ( 𝑞 = 0 → ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) = ( 𝑓 − ( 𝐺 ∙ 0 ) ) )
99	98	fveq2d	⊢ ( 𝑞 = 0 → ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) = ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 0 ) ) ) )
100	99	breq1d	⊢ ( 𝑞 = 0 → ( ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 0 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
101	100	rspcev	⊢ ( ( 0 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 0 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
102	81 96 101	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
103	102	ex	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
104	103	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 0 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
105		nn0addcl	⊢ ( ( ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ∈ ℕ0 )
106	27 105	sylan	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ∈ ℕ0 )
107	106	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ∈ ℕ0 )
108	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → 𝑅 ∈ Ring )
109		simprl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → 𝑔 ∈ 𝐵 )
110	2 1 3	deg1cl	⊢ ( 𝑔 ∈ 𝐵 → ( 𝐷 ‘ 𝑔 ) ∈ ( ℕ0 ∪ { -∞ } ) )
111	27	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
112		peano2nn0	⊢ ( 𝑑 ∈ ℕ0 → ( 𝑑 + 1 ) ∈ ℕ0 )
113	112	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑑 + 1 ) ∈ ℕ0 )
114	111 113	nn0addcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ∈ ℕ0 )
115	114	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ∈ ℤ )
116		degltlem1	⊢ ( ( ( 𝐷 ‘ 𝑔 ) ∈ ( ℕ0 ∪ { -∞ } ) ∧ ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ∈ ℤ ) → ( ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ↔ ( 𝐷 ‘ 𝑔 ) ≤ ( ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) − 1 ) ) )
117	110 115 116	syl2an2	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ↔ ( 𝐷 ‘ 𝑔 ) ≤ ( ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) − 1 ) ) )
118	117	biimpd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ( 𝐷 ‘ 𝑔 ) ≤ ( ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) − 1 ) ) )
119	118	impr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( 𝐷 ‘ 𝑔 ) ≤ ( ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) − 1 ) )
120	27	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
121	120	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℂ )
122		nn0cn	⊢ ( 𝑑 ∈ ℕ0 → 𝑑 ∈ ℂ )
123	122	adantl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → 𝑑 ∈ ℂ )
124		peano2cn	⊢ ( 𝑑 ∈ ℂ → ( 𝑑 + 1 ) ∈ ℂ )
125	123 124	syl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( 𝑑 + 1 ) ∈ ℂ )
126		1cnd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → 1 ∈ ℂ )
127	121 125 126	addsubassd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) − 1 ) = ( ( 𝐷 ‘ 𝐺 ) + ( ( 𝑑 + 1 ) − 1 ) ) )
128		ax-1cn	⊢ 1 ∈ ℂ
129		pncan	⊢ ( ( 𝑑 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑑 + 1 ) − 1 ) = 𝑑 )
130	123 128 129	sylancl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑑 + 1 ) − 1 ) = 𝑑 )
131	130	oveq2d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐺 ) + ( ( 𝑑 + 1 ) − 1 ) ) = ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
132	127 131	eqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) − 1 ) = ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
133	132	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) − 1 ) = ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
134	119 133	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( 𝐷 ‘ 𝑔 ) ≤ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
135	78	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑃 ∈ Ring )
136	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
137	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑅 ∈ Ring )
138	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → 𝐼 ∈ 𝐾 )
139		eqid	⊢ ( coe1 ‘ 𝑔 ) = ( coe1 ‘ 𝑔 )
140	139 3 1 12	coe1f	⊢ ( 𝑔 ∈ 𝐵 → ( coe1 ‘ 𝑔 ) : ℕ0 ⟶ 𝐾 )
141	140	adantl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( coe1 ‘ 𝑔 ) : ℕ0 ⟶ 𝐾 )
142		simplr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑑 ∈ ℕ0 )
143	111 142	nn0addcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ∈ ℕ0 )
144	141 143	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ∈ 𝐾 )
145	12 13	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝐾 ∧ ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ∈ 𝐾 ) → ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ∈ 𝐾 )
146	137 138 144 145	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ∈ 𝐾 )
147		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
148		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
149		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
150		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
151	12 1 147 148 149 150 3	ply1tmcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ∈ 𝐾 ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ 𝐵 )
152	137 146 142 151	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ 𝐵 )
153	3 6	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ 𝐵 ) → ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 )
154	135 136 152 153	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 )
155	154	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 )
156	111	nn0red	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℝ )
157	156	leidd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐺 ) ≤ ( 𝐷 ‘ 𝐺 ) )
158	2 12 1 147 148 149 150	deg1tmle	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ∈ 𝐾 ∧ 𝑑 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ≤ 𝑑 )
159	137 146 142 158	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ≤ 𝑑 )
160	1 2 137 3 6 136 152 111 142 157 159	deg1mulle2	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ≤ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
161	160	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( 𝐷 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ≤ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
162		eqid	⊢ ( coe1 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) = ( coe1 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
163		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
164	163 12 1 147 148 149 150 3 6 13 136 137 146 142 111	coe1tmmul2fv	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( coe1 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ‘ ( 𝑑 + ( 𝐷 ‘ 𝐺 ) ) ) = ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ) )
165	111	nn0cnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐺 ) ∈ ℂ )
166	122	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑑 ∈ ℂ )
167	165 166	addcomd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) = ( 𝑑 + ( 𝐷 ‘ 𝐺 ) ) )
168	167	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( coe1 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) = ( ( coe1 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ‘ ( 𝑑 + ( 𝐷 ‘ 𝐺 ) ) ) )
169	15	oveq1d	⊢ ( 𝜑 → ( ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · 𝐼 ) · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) = ( 1 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) )
170	169	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · 𝐼 ) · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) = ( 1 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) )
171		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
172	171 3 1 12	coe1f	⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ 𝐾 )
173	9 172	syl	⊢ ( 𝜑 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ 𝐾 )
174	173	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ 𝐾 )
175	174 111	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝐾 )
176	12 13	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝐾 ∧ 𝐼 ∈ 𝐾 ∧ ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ∈ 𝐾 ) ) → ( ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · 𝐼 ) · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) = ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ) )
177	137 175 138 144 176	syl13anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · 𝐼 ) · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) = ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ) )
178	12 13 11	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ∈ 𝐾 ) → ( 1 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) = ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
179	137 144 178	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 1 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) = ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
180	170 177 179	3eqtr3rd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) = ( ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) · ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ) )
181	164 168 180	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) = ( ( coe1 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
182	181	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) = ( ( coe1 ‘ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
183	2 1 3 4 107 108 109 134 155 161 139 162 182	deg1sublt	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
184	183	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) )
185		fveq2	⊢ ( 𝑓 = ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) → ( 𝐷 ‘ 𝑓 ) = ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
186	185	breq1d	⊢ ( 𝑓 = ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) → ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ↔ ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) )
187		fvoveq1	⊢ ( 𝑓 = ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) → ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) = ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) )
188	187	breq1d	⊢ ( 𝑓 = ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) → ( ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
189	188	rexbidv	⊢ ( 𝑓 = ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) → ( ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
190	186 189	imbi12d	⊢ ( 𝑓 = ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) → ( ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
191		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
192	87	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑃 ∈ Grp )
193		simpr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ 𝐵 )
194	3 4	grpsubcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 ) → ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ∈ 𝐵 )
195	192 193 154 194	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ∈ 𝐵 )
196	195	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ∈ 𝐵 )
197	196	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ∈ 𝐵 )
198	190 191 197	rspcdva	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
199	184 198	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
200	78	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → 𝑃 ∈ Ring )
201		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → 𝑞 ∈ 𝐵 )
202	152	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ 𝐵 )
203		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
204	3 203	ringacl	⊢ ( ( 𝑃 ∈ Ring ∧ 𝑞 ∈ 𝐵 ∧ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ 𝐵 ) → ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 )
205	200 201 202 204	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 )
206	87	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → 𝑃 ∈ Grp )
207		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → 𝑔 ∈ 𝐵 )
208	154	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 )
209	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
210	3 6	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐺 ∙ 𝑞 ) ∈ 𝐵 )
211	200 209 201 210	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝐺 ∙ 𝑞 ) ∈ 𝐵 )
212	3 203 4	grpsubsub4	⊢ ( ( 𝑃 ∈ Grp ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 ∧ ( 𝐺 ∙ 𝑞 ) ∈ 𝐵 ) ) → ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) = ( 𝑔 − ( ( 𝐺 ∙ 𝑞 ) ( +g ‘ 𝑃 ) ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
213	206 207 208 211 212	syl13anc	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) = ( 𝑔 − ( ( 𝐺 ∙ 𝑞 ) ( +g ‘ 𝑃 ) ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
214	3 203 6	ringdi	⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐺 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ 𝐵 ) ) → ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) = ( ( 𝐺 ∙ 𝑞 ) ( +g ‘ 𝑃 ) ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
215	200 209 201 202 214	syl13anc	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) = ( ( 𝐺 ∙ 𝑞 ) ( +g ‘ 𝑃 ) ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
216	215	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) = ( 𝑔 − ( ( 𝐺 ∙ 𝑞 ) ( +g ‘ 𝑃 ) ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
217	213 216	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) = ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
218	217	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) = ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) )
219	218	breq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
220	219	biimpd	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) → ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
221		oveq2	⊢ ( 𝑟 = ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) → ( 𝐺 ∙ 𝑟 ) = ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
222	221	oveq2d	⊢ ( 𝑟 = ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) → ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) = ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
223	222	fveq2d	⊢ ( 𝑟 = ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) → ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) = ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) )
224	223	breq1d	⊢ ( 𝑟 = ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) → ( ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
225	224	rspcev	⊢ ( ( ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ ( 𝑞 ( +g ‘ 𝑃 ) ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
226	205 220 225	syl6an	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
227	226	rexlimdva	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑔 ∈ 𝐵 ) → ( ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
228	227	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
229	228	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ( ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( ( 𝑔 − ( 𝐺 ∙ ( ( 𝐼 · ( ( coe1 ‘ 𝑔 ) ‘ ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
230	199 229	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) ∧ ( 𝑔 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
231	230	expr	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
232	231	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) → ∀ 𝑔 ∈ 𝐵 ( ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
233		fveq2	⊢ ( 𝑔 = 𝑓 → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ 𝑓 ) )
234	233	breq1d	⊢ ( 𝑔 = 𝑓 → ( ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ↔ ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) ) )
235		fvoveq1	⊢ ( 𝑔 = 𝑓 → ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) = ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑟 ) ) ) )
236	235	breq1d	⊢ ( 𝑔 = 𝑓 → ( ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
237	236	rexbidv	⊢ ( 𝑔 = 𝑓 → ( ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
238		oveq2	⊢ ( 𝑟 = 𝑞 → ( 𝐺 ∙ 𝑟 ) = ( 𝐺 ∙ 𝑞 ) )
239	238	oveq2d	⊢ ( 𝑟 = 𝑞 → ( 𝑓 − ( 𝐺 ∙ 𝑟 ) ) = ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) )
240	239	fveq2d	⊢ ( 𝑟 = 𝑞 → ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑟 ) ) ) = ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) )
241	240	breq1d	⊢ ( 𝑟 = 𝑞 → ( ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
242	241	cbvrexvw	⊢ ( ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
243	237 242	bitrdi	⊢ ( 𝑔 = 𝑓 → ( ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
244	234 243	imbi12d	⊢ ( 𝑔 = 𝑓 → ( ( ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
245	244	cbvralvw	⊢ ( ∀ 𝑔 ∈ 𝐵 ( ( 𝐷 ‘ 𝑔 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝐷 ‘ ( 𝑔 − ( 𝐺 ∙ 𝑟 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
246	232 245	sylib	⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ℕ0 ∧ ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
247	246	exp32	⊢ ( 𝜑 → ( 𝑑 ∈ ℕ0 → ( ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) )
248	247	com12	⊢ ( 𝑑 ∈ ℕ0 → ( 𝜑 → ( ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) )
249	248	a2d	⊢ ( 𝑑 ∈ ℕ0 → ( ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) → ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) ) )
250	66 71 76 71 104 249	nn0ind	⊢ ( 𝑑 ∈ ℕ0 → ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
251	250	impcom	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ∀ 𝑓 ∈ 𝐵 ( ( 𝐷 ‘ 𝑓 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
252	8	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → 𝐹 ∈ 𝐵 )
253	61 251 252	rspcdva	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
254	253	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑑 ∈ ℕ0 ( 𝐷 ‘ 𝐹 ) < ( ( 𝐷 ‘ 𝐺 ) + 𝑑 ) → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
255	55 254	mpd	⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )