Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ∙ 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )