Metamath Proof Explorer

Theorem mon1pid

Description: Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses mon1pid.p 
|- P = ( Poly1 ` R )
mon1pid.o 
|- .1. = ( 1r ` P )
mon1pid.m 
|- M = ( Monic1p ` R )
mon1pid.d 
|- D = ( deg1 ` R )
Assertion mon1pid 
|- ( R e. NzRing -> ( .1. e. M /\ ( D ` .1. ) = 0 ) )

Proof

Step Hyp Ref Expression
1 mon1pid.p 
 |-  P = ( Poly1 ` R )
2 mon1pid.o 
 |-  .1. = ( 1r ` P )
3 mon1pid.m 
 |-  M = ( Monic1p ` R )
4 mon1pid.d 
 |-  D = ( deg1 ` R )
5 1 ply1nz 
 |-  ( R e. NzRing -> P e. NzRing )
6 nzrring 
 |-  ( P e. NzRing -> P e. Ring )
7 eqid 
 |-  ( Base ` P ) = ( Base ` P )
8 7 2 ringidcl 
 |-  ( P e. Ring -> .1. e. ( Base ` P ) )
9 5 6 8 3syl 
 |-  ( R e. NzRing -> .1. e. ( Base ` P ) )
10 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
11 2 10 nzrnz 
 |-  ( P e. NzRing -> .1. =/= ( 0g ` P ) )
12 5 11 syl 
 |-  ( R e. NzRing -> .1. =/= ( 0g ` P ) )
13 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
14 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
15 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
16 1 14 15 2 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = .1. )
17 13 16 syl 
 |-  ( R e. NzRing -> ( ( algSc ` P ) ` ( 1r ` R ) ) = .1. )
18 17 fveq2d 
 |-  ( R e. NzRing -> ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( coe1 ` .1. ) )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 19 15 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
21 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
22 1 14 19 21 coe1scl 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( x e. NN0 |-> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) ) )
23 13 20 22 syl2anc2 
 |-  ( R e. NzRing -> ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( x e. NN0 |-> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) ) )
24 18 23 eqtr3d 
 |-  ( R e. NzRing -> ( coe1 ` .1. ) = ( x e. NN0 |-> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) ) )
25 17 fveq2d 
 |-  ( R e. NzRing -> ( D ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( D ` .1. ) )
26 13 20 syl 
 |-  ( R e. NzRing -> ( 1r ` R ) e. ( Base ` R ) )
27 15 21 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
28 4 1 19 14 21 deg1scl 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( D ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = 0 )
29 13 26 27 28 syl3anc 
 |-  ( R e. NzRing -> ( D ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = 0 )
30 25 29 eqtr3d 
 |-  ( R e. NzRing -> ( D ` .1. ) = 0 )
31 24 30 fveq12d 
 |-  ( R e. NzRing -> ( ( coe1 ` .1. ) ` ( D ` .1. ) ) = ( ( x e. NN0 |-> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) ) ` 0 ) )
32 0nn0 
 |-  0 e. NN0
33 iftrue 
 |-  ( x = 0 -> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
34 eqid 
 |-  ( x e. NN0 |-> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) ) = ( x e. NN0 |-> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) )
35 fvex 
 |-  ( 1r ` R ) e. _V
36 33 34 35 fvmpt 
 |-  ( 0 e. NN0 -> ( ( x e. NN0 |-> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) ) ` 0 ) = ( 1r ` R ) )
37 32 36 ax-mp 
 |-  ( ( x e. NN0 |-> if ( x = 0 , ( 1r ` R ) , ( 0g ` R ) ) ) ` 0 ) = ( 1r ` R )
38 31 37 eqtrdi 
 |-  ( R e. NzRing -> ( ( coe1 ` .1. ) ` ( D ` .1. ) ) = ( 1r ` R ) )
39 1 7 10 4 3 15 ismon1p 
 |-  ( .1. e. M <-> ( .1. e. ( Base ` P ) /\ .1. =/= ( 0g ` P ) /\ ( ( coe1 ` .1. ) ` ( D ` .1. ) ) = ( 1r ` R ) ) )
40 9 12 38 39 syl3anbrc 
 |-  ( R e. NzRing -> .1. e. M )
41 40 30 jca 
 |-  ( R e. NzRing -> ( .1. e. M /\ ( D ` .1. ) = 0 ) )