Metamath Proof Explorer

Theorem quotlem

Description: Lemma for properties of the polynomial quotient function. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses plydiv.pl ⊢ φ ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
plydiv.tm ⊢ φ ∧ x ∈ S ∧ y ∈ S → x ⁢ y ∈ S
plydiv.rc ⊢ φ ∧ x ∈ S ∧ x ≠ 0 → 1 x ∈ S
plydiv.m1 ⊢ φ → − 1 ∈ S
plydiv.f ⊢ φ → F ∈ Poly ⁡ S
plydiv.g ⊢ φ → G ∈ Poly ⁡ S
plydiv.z ⊢ φ → G ≠ 0 𝑝
quotlem.8 ⊢ R = F − f G × f F quot G
Assertion quotlem ⊢ φ → F quot G ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G

Proof

Step Hyp Ref Expression
1 plydiv.pl ⊢ φ ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
2 plydiv.tm ⊢ φ ∧ x ∈ S ∧ y ∈ S → x ⁢ y ∈ S
3 plydiv.rc ⊢ φ ∧ x ∈ S ∧ x ≠ 0 → 1 x ∈ S
4 plydiv.m1 ⊢ φ → − 1 ∈ S
5 plydiv.f ⊢ φ → F ∈ Poly ⁡ S
6 plydiv.g ⊢ φ → G ∈ Poly ⁡ S
7 plydiv.z ⊢ φ → G ≠ 0 𝑝
8 quotlem.8 ⊢ R = F − f G × f F quot G
9 eqid ⊢ F − f G × f q = F − f G × f q
10 9 quotval ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S ∧ G ≠ 0 𝑝 → F quot G = ι q ∈ Poly ⁡ ℂ | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
11 5 6 7 10 syl3anc ⊢ φ → F quot G = ι q ∈ Poly ⁡ ℂ | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
12 1 2 3 4 5 6 7 9 plydivalg ⊢ φ → ∃! q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
13 reurex ⊢ ∃! q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G → ∃ q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
14 12 13 syl ⊢ φ → ∃ q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
15 addcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
16 15 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
17 mulcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x ⁢ y ∈ ℂ
18 17 adantl ⊢ φ ∧ x ∈ ℂ ∧ y ∈ ℂ → x ⁢ y ∈ ℂ
19 reccl ⊢ x ∈ ℂ ∧ x ≠ 0 → 1 x ∈ ℂ
20 19 adantl ⊢ φ ∧ x ∈ ℂ ∧ x ≠ 0 → 1 x ∈ ℂ
21 neg1cn ⊢ − 1 ∈ ℂ
22 21 a1i ⊢ φ → − 1 ∈ ℂ
23 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
24 23 5 sseldi ⊢ φ → F ∈ Poly ⁡ ℂ
25 23 6 sseldi ⊢ φ → G ∈ Poly ⁡ ℂ
26 16 18 20 22 24 25 7 9 plydivalg ⊢ φ → ∃! q ∈ Poly ⁡ ℂ F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
27 id ⊢ F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G → F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
28 27 rgenw ⊢ ∀ q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G → F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
29 riotass2 ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ ∧ ∀ q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G → F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G ∧ ∃ q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G ∧ ∃! q ∈ Poly ⁡ ℂ F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G → ι q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G = ι q ∈ Poly ⁡ ℂ | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
30 23 28 29 mpanl12 ⊢ ∃ q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G ∧ ∃! q ∈ Poly ⁡ ℂ F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G → ι q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G = ι q ∈ Poly ⁡ ℂ | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
31 14 26 30 syl2anc ⊢ φ → ι q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G = ι q ∈ Poly ⁡ ℂ | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
32 11 31 eqtr4d ⊢ φ → F quot G = ι q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
33 riotacl2 ⊢ ∃! q ∈ Poly ⁡ S F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G → ι q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G ∈ q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
34 12 33 syl ⊢ φ → ι q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G ∈ q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
35 32 34 eqeltrd ⊢ φ → F quot G ∈ q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G
36 oveq2 ⊢ q = F quot G → G × f q = G × f F quot G
37 36 oveq2d ⊢ q = F quot G → F − f G × f q = F − f G × f F quot G
38 37 8 eqtr4di ⊢ q = F quot G → F − f G × f q = R
39 38 eqeq1d ⊢ q = F quot G → F − f G × f q = 0 𝑝 ↔ R = 0 𝑝
40 38 fveq2d ⊢ q = F quot G → deg ⁡ F − f G × f q = deg ⁡ R
41 40 breq1d ⊢ q = F quot G → deg ⁡ F − f G × f q < deg ⁡ G ↔ deg ⁡ R < deg ⁡ G
42 39 41 orbi12d ⊢ q = F quot G → F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G ↔ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
43 42 elrab ⊢ F quot G ∈ q ∈ Poly ⁡ S | F − f G × f q = 0 𝑝 ∨ deg ⁡ F − f G × f q < deg ⁡ G ↔ F quot G ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
44 35 43 sylib ⊢ φ → F quot G ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G