Theorem quotval

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

	Ref	Expression
Hypothesis	quotval.1	⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
Assertion	quotval	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		quotval.1	⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
2		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
3	2	sseli	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
4	2	sseli	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
5		eldifsn	⊢ ( 𝐺 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↔ ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) )
6		oveq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∘f · 𝑞 ) = ( 𝐺 ∘f · 𝑞 ) )
7		oveq12	⊢ ( ( 𝑓 = 𝐹 ∧ ( 𝑔 ∘f · 𝑞 ) = ( 𝐺 ∘f · 𝑞 ) ) → ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) ) )
8	6 7	sylan2	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) ) )
9	8 1	eqtr4di	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) = 𝑅 )
10	9	sbceq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ [ 𝑅 / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) )
11	1	ovexi	⊢ 𝑅 ∈ V
12		eqeq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 = 0𝑝 ↔ 𝑅 = 0𝑝 ) )
13		fveq2	⊢ ( 𝑟 = 𝑅 → ( deg ‘ 𝑟 ) = ( deg ‘ 𝑅 ) )
14	13	breq1d	⊢ ( 𝑟 = 𝑅 → ( ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ↔ ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ) )
15	12 14	orbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ) ) )
16	11 15	sbcie	⊢ ( [ 𝑅 / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ) )
17		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
18	17	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( deg ‘ 𝑔 ) = ( deg ‘ 𝐺 ) )
19	18	breq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ↔ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
20	19	orbi2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
21	16 20	bitrid	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( [ 𝑅 / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
22	10 21	bitrd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
23	22	riotabidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
24		df-quot	⊢ quot = ( 𝑓 ∈ ( Poly ‘ ℂ ) , 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↦ ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) )
25		riotaex	⊢ ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) ∈ V
26	23 24 25	ovmpoa	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
27	5 26	sylan2br	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
28	27	3impb	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
29	4 28	syl3an2	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
30	3 29	syl3an1	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )