Metamath Proof Explorer

Theorem plydivlem3

Description: Lemma for plydivex . Base case of induction. (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 · 𝑞 ) )
plydiv.0 ⊢ ( 𝜑 → ( 𝐹 = 0𝑝 ∨ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 0 ) )
Assertion plydivlem3 ( 𝜑 → ∃ 𝑞 ∈ ( 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 plydiv.0 ⊢ ( 𝜑 → ( 𝐹 = 0𝑝 ∨ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 0 ) )
10 plybss ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
11 ply0 ⊢ ( 𝑆 ⊆ ℂ → 0𝑝 ∈ ( Poly ‘ 𝑆 ) )
12 5 10 11 3syl ⊢ ( 𝜑 → 0𝑝 ∈ ( Poly ‘ 𝑆 ) )
13 cnex ⊢ ℂ ∈ V
14 13 a1i ⊢ ( 𝜑 → ℂ ∈ V )
15 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
16 ffn ⊢ ( 𝐹 : ℂ ⟶ ℂ → 𝐹 Fn ℂ )
17 5 15 16 3syl ⊢ ( 𝜑 → 𝐹 Fn ℂ )
18 plyf ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
19 ffn ⊢ ( 𝐺 : ℂ ⟶ ℂ → 𝐺 Fn ℂ )
20 6 18 19 3syl ⊢ ( 𝜑 → 𝐺 Fn ℂ )
21 plyf ⊢ ( 0𝑝 ∈ ( Poly ‘ 𝑆 ) → 0𝑝 : ℂ ⟶ ℂ )
22 ffn ⊢ ( 0𝑝 : ℂ ⟶ ℂ → 0𝑝 Fn ℂ )
23 12 21 22 3syl ⊢ ( 𝜑 → 0𝑝 Fn ℂ )
24 inidm ⊢ ( ℂ ∩ ℂ ) = ℂ
25 20 23 14 14 24 offn ⊢ ( 𝜑 → ( 𝐺 ∘f · 0𝑝 ) Fn ℂ )
26 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
27 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
28 0pval ⊢ ( 𝑧 ∈ ℂ → ( 0𝑝 ‘ 𝑧 ) = 0 )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0𝑝 ‘ 𝑧 ) = 0 )
30 20 23 14 14 24 27 29 ofval ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝐺 ∘f · 0𝑝 ) ‘ 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) · 0 ) )
31 6 18 syl ⊢ ( 𝜑 → 𝐺 : ℂ ⟶ ℂ )
32 31 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
33 32 mul01d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝐺 ‘ 𝑧 ) · 0 ) = 0 )
34 30 33 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝐺 ∘f · 0𝑝 ) ‘ 𝑧 ) = 0 )
35 5 15 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
36 35 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
37 36 subid1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝐹 ‘ 𝑧 ) − 0 ) = ( 𝐹 ‘ 𝑧 ) )
38 14 17 25 17 26 34 37 offveq ⊢ ( 𝜑 → ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) = 𝐹 )
39 38 eqeq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) = 0𝑝 ↔ 𝐹 = 0𝑝 ) )
40 38 fveq2d ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) = ( deg ‘ 𝐹 ) )
41 dgrcl ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
42 6 41 syl ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℕ0 )
43 42 nn0red ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℝ )
44 43 recnd ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℂ )
45 44 addlidd ⊢ ( 𝜑 → ( 0 + ( deg ‘ 𝐺 ) ) = ( deg ‘ 𝐺 ) )
46 45 eqcomd ⊢ ( 𝜑 → ( deg ‘ 𝐺 ) = ( 0 + ( deg ‘ 𝐺 ) ) )
47 40 46 breq12d ⊢ ( 𝜑 → ( ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) < ( deg ‘ 𝐺 ) ↔ ( deg ‘ 𝐹 ) < ( 0 + ( deg ‘ 𝐺 ) ) ) )
48 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
49 5 48 syl ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
50 49 nn0red ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℝ )
51 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
52 50 43 51 ltsubaddd ⊢ ( 𝜑 → ( ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 0 ↔ ( deg ‘ 𝐹 ) < ( 0 + ( deg ‘ 𝐺 ) ) ) )
53 47 52 bitr4d ⊢ ( 𝜑 → ( ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) < ( deg ‘ 𝐺 ) ↔ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 0 ) )
54 39 53 orbi12d ⊢ ( 𝜑 → ( ( ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) ↔ ( 𝐹 = 0𝑝 ∨ ( ( deg ‘ 𝐹 ) − ( deg ‘ 𝐺 ) ) < 0 ) ) )
55 9 54 mpbird ⊢ ( 𝜑 → ( ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) )
56 oveq2 ⊢ ( 𝑞 = 0𝑝 → ( 𝐺 ∘f · 𝑞 ) = ( 𝐺 ∘f · 0𝑝 ) )
57 56 oveq2d ⊢ ( 𝑞 = 0𝑝 → ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) )
58 8 57 eqtrid ⊢ ( 𝑞 = 0𝑝 → 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) )
59 58 eqeq1d ⊢ ( 𝑞 = 0𝑝 → ( 𝑅 = 0𝑝 ↔ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) = 0𝑝 ) )
60 58 fveq2d ⊢ ( 𝑞 = 0𝑝 → ( deg ‘ 𝑅 ) = ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) )
61 60 breq1d ⊢ ( 𝑞 = 0𝑝 → ( ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ↔ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) )
62 59 61 orbi12d ⊢ ( 𝑞 = 0𝑝 → ( ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ↔ ( ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) ) )
63 62 rspcev ⊢ ( ( 0𝑝 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · 0𝑝 ) ) ) < ( deg ‘ 𝐺 ) ) ) → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
64 12 55 63 syl2anc ⊢ ( 𝜑 → ∃ 𝑞 ∈ ( Poly ‘ 𝑆 ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )