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

Metamath Proof Explorer

Theorem ismon1p

Description: Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses uc1pval.p 
|- P = ( Poly1 ` R )
uc1pval.b 
|- B = ( Base ` P )
uc1pval.z 
|- .0. = ( 0g ` P )
uc1pval.d 
|- D = ( deg1 ` R )
mon1pval.m 
|- M = ( Monic1p ` R )
mon1pval.o 
|- .1. = ( 1r ` R )
Assertion ismon1p 
|- ( F e. M <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) )

Proof

Step Hyp Ref Expression
1 uc1pval.p 
 |-  P = ( Poly1 ` R )
2 uc1pval.b 
 |-  B = ( Base ` P )
3 uc1pval.z 
 |-  .0. = ( 0g ` P )
4 uc1pval.d 
 |-  D = ( deg1 ` R )
5 mon1pval.m 
 |-  M = ( Monic1p ` R )
6 mon1pval.o 
 |-  .1. = ( 1r ` R )
7 neeq1 
 |-  ( f = F -> ( f =/= .0. <-> F =/= .0. ) )
8 fveq2 
 |-  ( f = F -> ( coe1 ` f ) = ( coe1 ` F ) )
9 fveq2 
 |-  ( f = F -> ( D ` f ) = ( D ` F ) )
10 8 9 fveq12d 
 |-  ( f = F -> ( ( coe1 ` f ) ` ( D ` f ) ) = ( ( coe1 ` F ) ` ( D ` F ) ) )
11 10 eqeq1d 
 |-  ( f = F -> ( ( ( coe1 ` f ) ` ( D ` f ) ) = .1. <-> ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) )
12 7 11 anbi12d 
 |-  ( f = F -> ( ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) <-> ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) ) )
13 1 2 3 4 5 6 mon1pval 
 |-  M = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) }
14 12 13 elrab2 
 |-  ( F e. M <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) ) )
15 3anass 
 |-  ( ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) ) )
16 14 15 bitr4i 
 |-  ( F e. M <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) )