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

Metamath Proof Explorer

Theorem q1pcl

Description: Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses q1pcl.q 
|- Q = ( quot1p ` R )
q1pcl.p 
|- P = ( Poly1 ` R )
q1pcl.b 
|- B = ( Base ` P )
q1pcl.c 
|- C = ( Unic1p ` R )
Assertion q1pcl 
|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) e. B )

Proof

Step Hyp Ref Expression
1 q1pcl.q 
 |-  Q = ( quot1p ` R )
2 q1pcl.p 
 |-  P = ( Poly1 ` R )
3 q1pcl.b 
 |-  B = ( Base ` P )
4 q1pcl.c 
 |-  C = ( Unic1p ` R )
5 eqid 
 |-  ( F Q G ) = ( F Q G )
6 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
7 eqid 
 |-  ( -g ` P ) = ( -g ` P )
8 eqid 
 |-  ( .r ` P ) = ( .r ` P )
9 1 2 3 6 7 8 4 q1peqb 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( ( F Q G ) e. B /\ ( ( deg1 ` R ) ` ( F ( -g ` P ) ( ( F Q G ) ( .r ` P ) G ) ) ) < ( ( deg1 ` R ) ` G ) ) <-> ( F Q G ) = ( F Q G ) ) )
10 5 9 mpbiri 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F Q G ) e. B /\ ( ( deg1 ` R ) ` ( F ( -g ` P ) ( ( F Q G ) ( .r ` P ) G ) ) ) < ( ( deg1 ` R ) ` G ) ) )
11 10 simpld 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) e. B )