This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )