Theorem quotcl

Description: The quotient of two polynomials in a field S is also in the field. (Contributed by Mario Carneiro, 26-Jul-2014)

	Ref	Expression
Hypotheses	plydiv.pl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
	plydiv.tm	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
	plydiv.rc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
	plydiv.m1	⊢ ( 𝜑 → - 1 ∈ 𝑆 )
	plydiv.f	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	plydiv.g	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
	plydiv.z	⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
Assertion	quotcl	⊢ ( 𝜑 → ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		plydiv.pl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2		plydiv.tm	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
3		plydiv.rc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
4		plydiv.m1	⊢ ( 𝜑 → - 1 ∈ 𝑆 )
5		plydiv.f	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6		plydiv.g	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
7		plydiv.z	⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
8		eqid	⊢ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) )
9	1 2 3 4 5 6 7 8	quotlem	⊢ ( 𝜑 → ( ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ 𝑆 ) ∧ ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) ) < ( deg ‘ 𝐺 ) ) ) )
10	9	simpld	⊢ ( 𝜑 → ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )