Metamath Proof Explorer

Theorem plydivalg

Description: The division algorithm on polynomials over a subfield S of the complex numbers. If F and G =/= 0 are polynomials over S , then there is a unique quotient polynomial q such that the remainder F - G x. q is either zero or has degree less than G . (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 𝑝
plydiv.r ⊢ R = F − f G × f q
Assertion plydivalg ⊢ φ → ∃! q ∈ 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 plydiv.r ⊢ R = F − f G × f q
9 1 2 3 4 5 6 7 8 plydivex ⊢ φ → ∃ q ∈ Poly ⁡ S R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
10 simpll ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → φ
11 10 1 sylan ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
12 10 2 sylan ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G ∧ x ∈ S ∧ y ∈ S → x ⁢ y ∈ S
13 10 3 sylan ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G ∧ x ∈ S ∧ x ≠ 0 → 1 x ∈ S
14 10 4 syl ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → − 1 ∈ S
15 10 5 syl ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → F ∈ Poly ⁡ S
16 10 6 syl ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → G ∈ Poly ⁡ S
17 10 7 syl ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → G ≠ 0 𝑝
18 eqid ⊢ F − f G × f p = F − f G × f p
19 simplrr ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → p ∈ Poly ⁡ S
20 simprr ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G
21 simplrl ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → q ∈ Poly ⁡ S
22 simprl ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
23 11 12 13 14 15 16 17 18 19 20 8 21 22 plydiveu ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S ∧ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → q = p
24 23 ex ⊢ φ ∧ q ∈ Poly ⁡ S ∧ p ∈ Poly ⁡ S → R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → q = p
25 24 ralrimivva ⊢ φ → ∀ q ∈ Poly ⁡ S ∀ p ∈ Poly ⁡ S R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → q = p
26 oveq2 ⊢ q = p → G × f q = G × f p
27 26 oveq2d ⊢ q = p → F − f G × f q = F − f G × f p
28 8 27 syl5eq ⊢ q = p → R = F − f G × f p
29 28 eqeq1d ⊢ q = p → R = 0 𝑝 ↔ F − f G × f p = 0 𝑝
30 28 fveq2d ⊢ q = p → deg ⁡ R = deg ⁡ F − f G × f p
31 30 breq1d ⊢ q = p → deg ⁡ R < deg ⁡ G ↔ deg ⁡ F − f G × f p < deg ⁡ G
32 29 31 orbi12d ⊢ q = p → R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ↔ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G
33 32 reu4 ⊢ ∃! q ∈ Poly ⁡ S R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ↔ ∃ q ∈ Poly ⁡ S R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ ∀ q ∈ Poly ⁡ S ∀ p ∈ Poly ⁡ S R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∧ F − f G × f p = 0 𝑝 ∨ deg ⁡ F − f G × f p < deg ⁡ G → q = p
34 9 25 33 sylanbrc ⊢ φ → ∃! q ∈ Poly ⁡ S R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G