Theorem quotval 23795

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

Hypothesis

Ref	Expression
quotval.1	⊢ 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓 · 𝑞))

Assertion

Ref	Expression
quotval	⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))

Distinct variable groups:   𝐹,𝑞   𝐺,𝑞

Allowed substitution hints:   𝑅(𝑞)   𝑆(𝑞)

Proof of Theorem quotval

Dummy variables 𝑓 𝑔 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		plyssc 23704	. . 3 ⊢ (Poly‘𝑆) ⊆ (Poly‘ℂ)
2	1	sseli 3563	. 2 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ (Poly‘ℂ))
3	1	sseli 3563	. . 3 ⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺 ∈ (Poly‘ℂ))
4		eldifsn 4259	. . . . 5 ⊢ (𝐺 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↔ (𝐺 ∈ (Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝))
5		oveq1 6533	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝑔 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · 𝑞))
6		oveq12 6535	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ (𝑔 ∘𝑓 · 𝑞) = (𝐺 ∘𝑓 · 𝑞)) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓 · 𝑞)) = (𝐹 ∘𝑓 − (𝐺 ∘𝑓 · 𝑞)))
7	5, 6	sylan2 489	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓 · 𝑞)) = (𝐹 ∘𝑓 − (𝐺 ∘𝑓 · 𝑞)))
8		quotval.1	. . . . . . . . . 10 ⊢ 𝑅 = (𝐹 ∘𝑓 − (𝐺 ∘𝑓 · 𝑞))
9	7, 8	syl6eqr 2661	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∘𝑓 − (𝑔 ∘𝑓 · 𝑞)) = 𝑅)
10	9	sbceq1d 3406	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘𝑓 − (𝑔 ∘𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)) ↔ [𝑅 / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
11		ovex 6554	. . . . . . . . . . 11 ⊢ (𝐹 ∘𝑓 − (𝐺 ∘𝑓 · 𝑞)) ∈ V
12	8, 11	eqeltri 2683	. . . . . . . . . 10 ⊢ 𝑅 ∈ V
13		eqeq1 2613	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑅 → (𝑟 = 0𝑝 ↔ 𝑅 = 0𝑝))
14		fveq2 6087	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑅 → (deg‘𝑟) = (deg‘𝑅))
15	14	breq1d 4587	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑅 → ((deg‘𝑟) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝑔)))
16	13, 15	orbi12d 741	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → ((𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)) ↔ (𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝑔))))
17	12, 16	sbcie 3436	. . . . . . . . 9 ⊢ ([𝑅 / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)) ↔ (𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝑔)))
18		simpr 475	. . . . . . . . . . . 12 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
19	18	fveq2d 6091	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (deg‘𝑔) = (deg‘𝐺))
20	19	breq2d 4589	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((deg‘𝑅) < (deg‘𝑔) ↔ (deg‘𝑅) < (deg‘𝐺)))
21	20	orbi2d 733	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝑔)) ↔ (𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
22	17, 21	syl5bb 270	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([𝑅 / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)) ↔ (𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
23	10, 22	bitrd 266	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ([(𝑓 ∘𝑓 − (𝑔 ∘𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)) ↔ (𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
24	23	riotabidv 6490	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘𝑓 − (𝑔 ∘𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
25		df-quot 23794	. . . . . 6 ⊢ quot = (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘𝑓 − (𝑔 ∘𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
26		riotaex 6492	. . . . . 6 ⊢ (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))) ∈ V
27	24, 25, 26	ovmpt2a 6666	. . . . 5 ⊢ ((𝐹 ∈ (Poly‘ℂ) ∧ 𝐺 ∈ ((Poly‘ℂ) ∖ {0𝑝})) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
28	4, 27	sylan2br 491	. . . 4 ⊢ ((𝐹 ∈ (Poly‘ℂ) ∧ (𝐺 ∈ (Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝)) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
29	28	3impb 1251	. . 3 ⊢ ((𝐹 ∈ (Poly‘ℂ) ∧ 𝐺 ∈ (Poly‘ℂ) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
30	3, 29	syl3an2 1351	. 2 ⊢ ((𝐹 ∈ (Poly‘ℂ) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
31	2, 30	syl3an1 1350	1 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))

Syntax hints:   → wi 4   ∨ wo 381   ∧ wa 382   ∧ w3a 1030   = wceq 1474   ∈ wcel 1976   ≠ wne 2779  Vcvv 3172  [wsbc 3401   ∖ cdif 3536  {csn 4124   class class class wbr 4577  ‘cfv 5789  ℩crio 6487  (class class class)co 6526   ∘_𝑓 cof 6770  ℂcc 9790   · cmul 9797   < clt 9930   − cmin 10117  0_𝑝c0p 23186  Polycply 23688  degcdgr 23691   quot cquot 23793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-map 7723  df-nn 10870  df-n0 11142  df-ply 23692  df-quot 23794

This theorem is referenced by:  quotlem  23803