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	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
	plydiv.tm	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
	plydiv.rc	|- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
	plydiv.m1	|- ( ph -> -u 1 e. S )
	plydiv.f	|- ( ph -> F e. ( Poly ` S ) )
	plydiv.g	|- ( ph -> G e. ( Poly ` S ) )
	plydiv.z	|- ( ph -> G =/= 0p )
Assertion	quotcl	|- ( ph -> ( F quot G ) e. ( Poly ` S ) )

Proof

Step	Hyp	Ref	Expression
1		plydiv.pl	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
2		plydiv.tm	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
3		plydiv.rc	|- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
4		plydiv.m1	|- ( ph -> -u 1 e. S )
5		plydiv.f	|- ( ph -> F e. ( Poly ` S ) )
6		plydiv.g	|- ( ph -> G e. ( Poly ` S ) )
7		plydiv.z	|- ( ph -> G =/= 0p )
8		eqid	|- ( F oF - ( G oF x. ( F quot G ) ) ) = ( F oF - ( G oF x. ( F quot G ) ) )
9	1 2 3 4 5 6 7 8	quotlem	|- ( ph -> ( ( F quot G ) e. ( Poly ` S ) /\ ( ( F oF - ( G oF x. ( F quot G ) ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. ( F quot G ) ) ) ) < ( deg ` G ) ) ) )
10	9	simpld	|- ( ph -> ( F quot G ) e. ( Poly ` S ) )