Metamath Proof Explorer

Theorem quotval

Description: Value of the quotient function. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypothesis quotval.1 ⊢ R = F − f G × f q
Assertion quotval ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S ∧ G ≠ 0 𝑝 → F quot G = ι q ∈ Poly ⁡ ℂ | R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G

Proof

Step Hyp Ref Expression
1 quotval.1 ⊢ R = F − f G × f q
2 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
3 2 sseli ⊢ F ∈ Poly ⁡ S → F ∈ Poly ⁡ ℂ
4 2 sseli ⊢ G ∈ Poly ⁡ S → G ∈ Poly ⁡ ℂ
5 eldifsn ⊢ G ∈ Poly ⁡ ℂ ∖ 0 𝑝 ↔ G ∈ Poly ⁡ ℂ ∧ G ≠ 0 𝑝
6 oveq1 ⊢ g = G → g × f q = G × f q
7 oveq12 ⊢ f = F ∧ g × f q = G × f q → f − f g × f q = F − f G × f q
8 6 7 sylan2 ⊢ f = F ∧ g = G → f − f g × f q = F − f G × f q
9 8 1 eqtr4di ⊢ f = F ∧ g = G → f − f g × f q = R
10 9 sbceq1d ⊢ f = F ∧ g = G → [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g ↔ [˙R / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g
11 1 ovexi ⊢ R ∈ V
12 eqeq1 ⊢ r = R → r = 0 𝑝 ↔ R = 0 𝑝
13 fveq2 ⊢ r = R → deg ⁡ r = deg ⁡ R
14 13 breq1d ⊢ r = R → deg ⁡ r < deg ⁡ g ↔ deg ⁡ R < deg ⁡ g
15 12 14 orbi12d ⊢ r = R → r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g ↔ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ g
16 11 15 sbcie ⊢ [˙R / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g ↔ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ g
17 simpr ⊢ f = F ∧ g = G → g = G
18 17 fveq2d ⊢ f = F ∧ g = G → deg ⁡ g = deg ⁡ G
19 18 breq2d ⊢ f = F ∧ g = G → deg ⁡ R < deg ⁡ g ↔ deg ⁡ R < deg ⁡ G
20 19 orbi2d ⊢ f = F ∧ g = G → R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ g ↔ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
21 16 20 bitrid ⊢ f = F ∧ g = G → [˙R / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g ↔ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
22 10 21 bitrd ⊢ f = F ∧ g = G → [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g ↔ R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
23 22 riotabidv ⊢ f = F ∧ g = G → ι q ∈ Poly ⁡ ℂ | [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g = ι q ∈ Poly ⁡ ℂ | R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
24 df-quot ⊢ quot = f ∈ Poly ⁡ ℂ , g ∈ Poly ⁡ ℂ ∖ 0 𝑝 ⟼ ι q ∈ Poly ⁡ ℂ | [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g
25 riotaex ⊢ ι q ∈ Poly ⁡ ℂ | R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G ∈ V
26 23 24 25 ovmpoa ⊢ F ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ ℂ ∖ 0 𝑝 → F quot G = ι q ∈ Poly ⁡ ℂ | R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
27 5 26 sylan2br ⊢ F ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ ℂ ∧ G ≠ 0 𝑝 → F quot G = ι q ∈ Poly ⁡ ℂ | R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
28 27 3impb ⊢ F ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ ℂ ∧ G ≠ 0 𝑝 → F quot G = ι q ∈ Poly ⁡ ℂ | R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
29 4 28 syl3an2 ⊢ F ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ S ∧ G ≠ 0 𝑝 → F quot G = ι q ∈ Poly ⁡ ℂ | R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G
30 3 29 syl3an1 ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S ∧ G ≠ 0 𝑝 → F quot G = ι q ∈ Poly ⁡ ℂ | R = 0 𝑝 ∨ deg ⁡ R < deg ⁡ G