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→1x∈S
plydiv.m1 ⊢φ→−1∈S
plydiv.f ⊢φ→F∈Poly⁡S
plydiv.g ⊢φ→G∈Poly⁡S
plydiv.z ⊢φ→G≠0𝑝
quotlem.8 ⊢R=F−fG×fFquotG
Assertion quotlem ⊢φ→FquotG∈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→1x∈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−fG×fFquotG
9 eqid ⊢F−fG×fq=F−fG×fq
10 9 quotval ⊢F∈Poly⁡S∧G∈Poly⁡S∧G≠0𝑝→FquotG=ιq∈Poly⁡ℂ|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
11 5 6 7 10 syl3anc ⊢φ→FquotG=ιq∈Poly⁡ℂ|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
12 1 2 3 4 5 6 7 9 plydivalg ⊢φ→∃!q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
13 reurex ⊢∃!q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G→∃q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
14 12 13 syl ⊢φ→∃q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<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→1x∈ℂ
20 19 adantl ⊢φ∧x∈ℂ∧x≠0→1x∈ℂ
21 neg1cn ⊢−1∈ℂ
22 21 a1i ⊢φ→−1∈ℂ
23 plyssc ⊢Poly⁡S⊆Poly⁡ℂ
24 23 5 sselid ⊢φ→F∈Poly⁡ℂ
25 23 6 sselid ⊢φ→G∈Poly⁡ℂ
26 16 18 20 22 24 25 7 9 plydivalg ⊢φ→∃!q∈Poly⁡ℂF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
27 id ⊢F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G→F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
28 27 rgenw ⊢∀q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G→F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
29 riotass2 ⊢Poly⁡S⊆Poly⁡ℂ∧∀q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G→F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G∧∃q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G∧∃!q∈Poly⁡ℂF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G→ιq∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G=ιq∈Poly⁡ℂ|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
30 23 28 29 mpanl12 ⊢∃q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G∧∃!q∈Poly⁡ℂF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G→ιq∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G=ιq∈Poly⁡ℂ|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
31 14 26 30 syl2anc ⊢φ→ιq∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G=ιq∈Poly⁡ℂ|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
32 11 31 eqtr4d ⊢φ→FquotG=ιq∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
33 riotacl2 ⊢∃!q∈Poly⁡SF−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G→ιq∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G∈q∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
34 12 33 syl ⊢φ→ιq∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G∈q∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
35 32 34 eqeltrd ⊢φ→FquotG∈q∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G
36 oveq2 ⊢q=FquotG→G×fq=G×fFquotG
37 36 oveq2d ⊢q=FquotG→F−fG×fq=F−fG×fFquotG
38 37 8 eqtr4di ⊢q=FquotG→F−fG×fq=R
39 38 eqeq1d ⊢q=FquotG→F−fG×fq=0𝑝↔R=0𝑝
40 38 fveq2d ⊢q=FquotG→deg⁡F−fG×fq=deg⁡R
41 40 breq1d ⊢q=FquotG→deg⁡F−fG×fq<deg⁡G↔deg⁡R<deg⁡G
42 39 41 orbi12d ⊢q=FquotG→F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G↔R=0𝑝∨deg⁡R<deg⁡G
43 42 elrab ⊢FquotG∈q∈Poly⁡S|F−fG×fq=0𝑝∨deg⁡F−fG×fq<deg⁡G↔FquotG∈Poly⁡S∧R=0𝑝∨deg⁡R<deg⁡G
44 35 43 sylib ⊢φ→FquotG∈Poly⁡S∧R=0𝑝∨deg⁡R<deg⁡G