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 = Poly 1 R
mon1pid.o 1 ˙ = 1 P
mon1pid.m M = Monic 1p R
mon1pid.d D = deg 1 R
Assertion mon1pid R NzRing 1 ˙ M D 1 ˙ = 0

Proof

Step Hyp Ref Expression
1 mon1pid.p P = Poly 1 R
2 mon1pid.o 1 ˙ = 1 P
3 mon1pid.m M = Monic 1p R
4 mon1pid.d D = deg 1 R
5 1 ply1nz R NzRing P NzRing
6 nzrring P NzRing P Ring
7 eqid Base P = Base P
8 7 2 ringidcl P Ring 1 ˙ Base P
9 5 6 8 3syl R NzRing 1 ˙ Base P
10 eqid 0 P = 0 P
11 2 10 nzrnz P NzRing 1 ˙ 0 P
12 5 11 syl R NzRing 1 ˙ 0 P
13 nzrring R NzRing R Ring
14 eqid algSc P = algSc P
15 eqid 1 R = 1 R
16 1 14 15 2 ply1scl1 R Ring algSc P 1 R = 1 ˙
17 13 16 syl R NzRing algSc P 1 R = 1 ˙
18 17 fveq2d R NzRing coe 1 algSc P 1 R = coe 1 1 ˙
19 eqid Base R = Base R
20 19 15 ringidcl R Ring 1 R Base R
21 eqid 0 R = 0 R
22 1 14 19 21 coe1scl R Ring 1 R Base R coe 1 algSc P 1 R = x 0 if x = 0 1 R 0 R
23 13 20 22 syl2anc2 R NzRing coe 1 algSc P 1 R = x 0 if x = 0 1 R 0 R
24 18 23 eqtr3d R NzRing coe 1 1 ˙ = x 0 if x = 0 1 R 0 R
25 17 fveq2d R NzRing D algSc P 1 R = D 1 ˙
26 13 20 syl R NzRing 1 R Base R
27 15 21 nzrnz R NzRing 1 R 0 R
28 4 1 19 14 21 deg1scl R Ring 1 R Base R 1 R 0 R D algSc P 1 R = 0
29 13 26 27 28 syl3anc R NzRing D algSc P 1 R = 0
30 25 29 eqtr3d R NzRing D 1 ˙ = 0
31 24 30 fveq12d R NzRing coe 1 1 ˙ D 1 ˙ = x 0 if x = 0 1 R 0 R 0
32 0nn0 0 0
33 iftrue x = 0 if x = 0 1 R 0 R = 1 R
34 eqid x 0 if x = 0 1 R 0 R = x 0 if x = 0 1 R 0 R
35 fvex 1 R V
36 33 34 35 fvmpt 0 0 x 0 if x = 0 1 R 0 R 0 = 1 R
37 32 36 ax-mp x 0 if x = 0 1 R 0 R 0 = 1 R
38 31 37 eqtrdi R NzRing coe 1 1 ˙ D 1 ˙ = 1 R
39 1 7 10 4 3 15 ismon1p 1 ˙ M 1 ˙ Base P 1 ˙ 0 P coe 1 1 ˙ D 1 ˙ = 1 R
40 9 12 38 39 syl3anbrc R NzRing 1 ˙ M
41 40 30 jca R NzRing 1 ˙ M D 1 ˙ = 0