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−fG×fq
Assertion quotval ⊢F∈Poly⁡S∧G∈Poly⁡S∧G≠0𝑝→FquotG=ιq∈Poly⁡ℂ|R=0𝑝∨deg⁡R<deg⁡G

Proof

Step Hyp Ref Expression
1 quotval.1 ⊢R=F−fG×fq
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×fq=G×fq
7 oveq12 ⊢f=F∧g×fq=G×fq→f−fg×fq=F−fG×fq
8 6 7 sylan2 ⊢f=F∧g=G→f−fg×fq=F−fG×fq
9 8 1 eqtr4di ⊢f=F∧g=G→f−fg×fq=R
10 9 sbceq1d ⊢f=F∧g=G→[˙f−fg×fq/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−fg×fq/r]˙r=0𝑝∨deg⁡r<deg⁡g↔R=0𝑝∨deg⁡R<deg⁡G
23 22 riotabidv ⊢f=F∧g=G→ιq∈Poly⁡ℂ|[˙f−fg×fq/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−fg×fq/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𝑝→FquotG=ιq∈Poly⁡ℂ|R=0𝑝∨deg⁡R<deg⁡G
27 5 26 sylan2br ⊢F∈Poly⁡ℂ∧G∈Poly⁡ℂ∧G≠0𝑝→FquotG=ιq∈Poly⁡ℂ|R=0𝑝∨deg⁡R<deg⁡G
28 27 3impb ⊢F∈Poly⁡ℂ∧G∈Poly⁡ℂ∧G≠0𝑝→FquotG=ιq∈Poly⁡ℂ|R=0𝑝∨deg⁡R<deg⁡G
29 4 28 syl3an2 ⊢F∈Poly⁡ℂ∧G∈Poly⁡S∧G≠0𝑝→FquotG=ιq∈Poly⁡ℂ|R=0𝑝∨deg⁡R<deg⁡G
30 3 29 syl3an1 ⊢F∈Poly⁡S∧G∈Poly⁡S∧G≠0𝑝→FquotG=ιq∈Poly⁡ℂ|R=0𝑝∨deg⁡R<deg⁡G