Metamath Proof Explorer

Theorem plydivex

Description: Lemma for plydivalg . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plydiv.pl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
plydiv.tm ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
plydiv.rc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
plydiv.m1 ⊢ ( 𝜑 → - 1 ∈ 𝑆 )
plydiv.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
plydiv.g ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
plydiv.z ⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
plydiv.r ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
Assertion plydivex ( 𝜑 → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 plydiv.pl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 plydiv.tm ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
3 plydiv.rc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
4 plydiv.m1 ⊢ ( 𝜑 → - 1 ∈ 𝑆 )
5 plydiv.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6 plydiv.g ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
7 plydiv.z ⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
8 plydiv.r ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
9 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
10 5 9 syl ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
11 10 nn0red ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℝ )
12 dgrcl ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
13 6 12 syl ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℕ0 )
14 13 nn0red ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℝ )
15 11 14 resubcld ⊢ ( 𝜑 → ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) ∈ ℝ )
16 arch ⊢ ( ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) ∈ ℝ → ∃ 𝑑 ∈ ℕ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 )
17 15 16 syl ⊢ ( 𝜑 → ∃ 𝑑 ∈ ℕ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 )
18 olc ⊢ ( ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 → ( 𝐹 = 0𝑝 ∨ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) )
19 eqeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 = 0𝑝 ↔ 𝐹 = 0𝑝 ) )
20 fveq2 ⊢ ( 𝑓 = 𝐹 → ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) )
21 20 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) )
22 21 breq1d ⊢ ( 𝑓 = 𝐹 → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ↔ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) )
23 19 22 orbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ↔ ( 𝐹 = 0𝑝 ∨ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ) )
24 oveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) ) )
25 24 8 eqtr4di ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 𝑅 )
26 25 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ↔ 𝑅 = 0𝑝 ) )
27 25 fveq2d ⊢ ( 𝑓 = 𝐹 → ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) = ( deg ‘ 𝑅 ) )
28 27 breq1d ⊢ ( 𝑓 = 𝐹 → ( ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ↔ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
29 26 28 orbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
30 29 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ↔ ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
31 23 30 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( 𝐹 = 0𝑝 ∨ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) ) )
32 nnnn0 ⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℕ0 )
33 breq2 ⊢ ( 𝑥 = 0 → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ↔ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) )
34 33 orbi2d ⊢ ( 𝑥 = 0 → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) ↔ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) )
35 34 imbi1d ⊢ ( 𝑥 = 0 → ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
36 35 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
37 36 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
38 breq2 ⊢ ( 𝑥 = 𝑑 → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ↔ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) )
39 38 orbi2d ⊢ ( 𝑥 = 𝑑 → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) ↔ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ) )
40 39 imbi1d ⊢ ( 𝑥 = 𝑑 → ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
41 40 ralbidv ⊢ ( 𝑥 = 𝑑 → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
42 41 imbi2d ⊢ ( 𝑥 = 𝑑 → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
43 breq2 ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ↔ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) )
44 43 orbi2d ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) ↔ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) ) )
45 44 imbi1d ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
46 45 ralbidv ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
47 46 imbi2d ⊢ ( 𝑥 = ( 𝑑 + 1 ) → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑥 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
48 1 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
49 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
50 3 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
51 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) → - 1 ∈ 𝑆 )
52 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) → 𝑓 ∈ ( Poly ‘ 𝑆 ) )
53 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
54 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) → 𝐺 ≠ 0𝑝 )
55 eqid ⊢ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) )
56 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) → ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) )
57 48 49 50 51 52 53 54 55 56 plydivlem3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) )
58 57 expr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
59 58 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 0 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
60 eqeq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 = 0𝑝 ↔ 𝑔 = 0𝑝 ) )
61 fveq2 ⊢ ( 𝑓 = 𝑔 → ( deg ‘ 𝑓 ) = ( deg ‘ 𝑔 ) )
62 61 oveq1d ⊢ ( 𝑓 = 𝑔 → ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) )
63 62 breq1d ⊢ ( 𝑓 = 𝑔 → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ↔ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) )
64 60 63 orbi12d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ↔ ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ) )
65 oveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) )
66 65 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ↔ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ) )
67 65 fveq2d ⊢ ( 𝑓 = 𝑔 → ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) = ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) )
68 67 breq1d ⊢ ( 𝑓 = 𝑔 → ( ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ↔ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) )
69 66 68 orbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ↔ ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
70 69 rexbidv ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ↔ ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
71 64 70 imbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
72 71 cbvralvw ⊢ ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
73 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → 𝜑 )
74 73 1 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
75 73 2 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
76 73 3 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
77 73 4 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → - 1 ∈ 𝑆 )
78 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → 𝑓 ∈ ( Poly ‘ 𝑆 ) )
79 73 6 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
80 73 7 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → 𝐺 ≠ 0𝑝 )
81 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → 𝑑 ∈ ℕ0 )
82 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 )
83 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → 𝑓 ≠ 0𝑝 )
84 eqid ⊢ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) = ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) )
85 oveq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ↑ 𝑑 ) = ( 𝑧 ↑ 𝑑 ) )
86 85 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) / ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ) · ( 𝑤 ↑ 𝑑 ) ) = ( ( ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) / ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ) · ( 𝑧 ↑ 𝑑 ) ) )
87 86 cbvmptv ⊢ ( 𝑤 ∈ ℂ ↦ ( ( ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) / ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ) · ( 𝑤 ↑ 𝑑 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) / ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ) · ( 𝑧 ↑ 𝑑 ) ) )
88 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
89 oveq2 ⊢ ( 𝑞 = 𝑝 → ( 𝐺 ∘f · 𝑞 ) = ( 𝐺 ∘f · 𝑝 ) )
90 89 oveq2d ⊢ ( 𝑞 = 𝑝 → ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) )
91 90 eqeq1d ⊢ ( 𝑞 = 𝑝 → ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ↔ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ) )
92 90 fveq2d ⊢ ( 𝑞 = 𝑝 → ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) = ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) )
93 92 breq1d ⊢ ( 𝑞 = 𝑝 → ( ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ↔ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) )
94 91 93 orbi12d ⊢ ( 𝑞 = 𝑝 → ( ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ↔ ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
95 94 cbvrexvw ⊢ ( ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) )
96 95 imbi2i ⊢ ( ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
97 96 ralbii ⊢ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
98 88 97 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
99 eqid ⊢ ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝑓 )
100 eqid ⊢ ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 )
101 eqid ⊢ ( deg ‘ 𝑓 ) = ( deg ‘ 𝑓 )
102 eqid ⊢ ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 )
103 74 75 76 77 78 79 80 55 81 82 83 84 87 98 99 100 101 102 plydivlem4 ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) )
104 103 exp32 ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) → ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
105 104 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑔 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 = 0𝑝 ∨ ( ( deg ‘ 𝑔 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑔 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
106 72 105 biimtrid ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
107 106 ancld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
108 dgrcl ⊢ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝑓 ) ∈ ℕ0 )
109 108 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ 𝑓 ) ∈ ℕ0 )
110 109 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ 𝑓 ) ∈ ℤ )
111 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
112 111 12 syl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
113 112 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ 𝐺 ) ∈ ℤ )
114 110 113 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) ∈ ℤ )
115 nn0z ⊢ ( 𝑑 ∈ ℕ0 → 𝑑 ∈ ℤ )
116 115 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → 𝑑 ∈ ℤ )
117 zleltp1 ⊢ ( ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) ∈ ℤ ∧ 𝑑 ∈ ℤ ) → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) ≤ 𝑑 ↔ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) )
118 114 116 117 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) ≤ 𝑑 ↔ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) )
119 114 zred ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) ∈ ℝ )
120 nn0re ⊢ ( 𝑑 ∈ ℕ0 → 𝑑 ∈ ℝ )
121 120 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → 𝑑 ∈ ℝ )
122 119 121 leloed ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) ≤ 𝑑 ↔ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) )
123 118 122 bitr3d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ↔ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) )
124 123 orbi2d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) ↔ ( 𝑓 = 0𝑝 ∨ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) )
125 pm5.63 ⊢ ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ↔ ( 𝑓 = 0𝑝 ∨ ( ¬ 𝑓 = 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) )
126 df-ne ⊢ ( 𝑓 ≠ 0𝑝 ↔ ¬ 𝑓 = 0𝑝 )
127 126 anbi1i ⊢ ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ↔ ( ¬ 𝑓 = 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) )
128 127 orbi2i ⊢ ( ( 𝑓 = 0𝑝 ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ↔ ( 𝑓 = 0𝑝 ∨ ( ¬ 𝑓 = 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) )
129 125 128 bitr4i ⊢ ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ↔ ( 𝑓 = 0𝑝 ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) )
130 129 orbi2i ⊢ ( ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ↔ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( 𝑓 = 0𝑝 ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) )
131 or12 ⊢ ( ( 𝑓 = 0𝑝 ∨ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ↔ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) )
132 or12 ⊢ ( ( 𝑓 = 0𝑝 ∨ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) ↔ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( 𝑓 = 0𝑝 ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) )
133 130 131 132 3bitr4i ⊢ ( ( 𝑓 = 0𝑝 ∨ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ↔ ( 𝑓 = 0𝑝 ∨ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) )
134 orass ⊢ ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ↔ ( 𝑓 = 0𝑝 ∨ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) )
135 133 134 bitr4i ⊢ ( ( 𝑓 = 0𝑝 ∨ ( ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ↔ ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) )
136 124 135 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) ↔ ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) ) )
137 136 imbi1d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
138 jaob ⊢ ( ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) ∨ ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
139 137 138 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
140 139 ralbidva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
141 r19.26 ⊢ ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ↔ ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
142 140 141 bitrdi ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ↔ ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ∧ ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ≠ 0𝑝 ∧ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) = 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
143 107 142 sylibrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
144 143 expcom ⊢ ( 𝑑 ∈ ℕ0 → ( 𝜑 → ( ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
145 144 a2d ⊢ ( 𝑑 ∈ ℕ0 → ( ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) → ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < ( 𝑑 + 1 ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) ) )
146 37 42 47 42 59 145 nn0ind ⊢ ( 𝑑 ∈ ℕ0 → ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
147 32 146 syl ⊢ ( 𝑑 ∈ ℕ → ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) ) )
148 147 impcom ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ∀ 𝑓 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 = 0𝑝 ∨ ( ( deg ‘ 𝑓 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝑓 ∘f − ( 𝐺 ∘f · 𝑞 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
149 5 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
150 31 148 149 rspcdva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( 𝐹 = 0𝑝 ∨ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
151 18 150 syl5 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
152 151 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ ℕ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 𝑑 → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
153 17 152 mpd ⊢ ( 𝜑 → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )