Metamath Proof Explorer


Theorem mon1psubm

Description: Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses mon1psubm.p P = Poly 1 R
mon1psubm.m M = Monic 1p R
mon1psubm.u U = mulGrp P
Assertion mon1psubm R NzRing M SubMnd U

Proof

Step Hyp Ref Expression
1 mon1psubm.p P = Poly 1 R
2 mon1psubm.m M = Monic 1p R
3 mon1psubm.u U = mulGrp P
4 eqid Base P = Base P
5 1 4 2 mon1pcl x M x Base P
6 5 ssriv M Base P
7 6 a1i R NzRing M Base P
8 eqid 1 P = 1 P
9 eqid deg 1 R = deg 1 R
10 1 8 2 9 mon1pid R NzRing 1 P M deg 1 R 1 P = 0
11 10 simpld R NzRing 1 P M
12 1 ply1nz R NzRing P NzRing
13 nzrring P NzRing P Ring
14 12 13 syl R NzRing P Ring
15 14 adantr R NzRing x M y M P Ring
16 5 ad2antrl R NzRing x M y M x Base P
17 simprr R NzRing x M y M y M
18 6 17 sselid R NzRing x M y M y Base P
19 eqid P = P
20 4 19 ringcl P Ring x Base P y Base P x P y Base P
21 15 16 18 20 syl3anc R NzRing x M y M x P y Base P
22 eqid RLReg R = RLReg R
23 eqid 0 P = 0 P
24 nzrring R NzRing R Ring
25 24 adantr R NzRing x M y M R Ring
26 1 23 2 mon1pn0 x M x 0 P
27 26 ad2antrl R NzRing x M y M x 0 P
28 eqid 1 R = 1 R
29 9 28 2 mon1pldg x M coe 1 x deg 1 R x = 1 R
30 29 ad2antrl R NzRing x M y M coe 1 x deg 1 R x = 1 R
31 eqid Unit R = Unit R
32 22 31 unitrrg R Ring Unit R RLReg R
33 24 32 syl R NzRing Unit R RLReg R
34 31 28 1unit R Ring 1 R Unit R
35 24 34 syl R NzRing 1 R Unit R
36 33 35 sseldd R NzRing 1 R RLReg R
37 36 adantr R NzRing x M y M 1 R RLReg R
38 30 37 eqeltrd R NzRing x M y M coe 1 x deg 1 R x RLReg R
39 1 23 2 mon1pn0 y M y 0 P
40 39 ad2antll R NzRing x M y M y 0 P
41 9 1 22 4 19 23 25 16 27 38 18 40 deg1mul2 R NzRing x M y M deg 1 R x P y = deg 1 R x + deg 1 R y
42 9 1 23 4 deg1nn0cl R Ring x Base P x 0 P deg 1 R x 0
43 25 16 27 42 syl3anc R NzRing x M y M deg 1 R x 0
44 9 1 23 4 deg1nn0cl R Ring y Base P y 0 P deg 1 R y 0
45 25 18 40 44 syl3anc R NzRing x M y M deg 1 R y 0
46 43 45 nn0addcld R NzRing x M y M deg 1 R x + deg 1 R y 0
47 41 46 eqeltrd R NzRing x M y M deg 1 R x P y 0
48 9 1 23 4 deg1nn0clb R Ring x P y Base P x P y 0 P deg 1 R x P y 0
49 25 21 48 syl2anc R NzRing x M y M x P y 0 P deg 1 R x P y 0
50 47 49 mpbird R NzRing x M y M x P y 0 P
51 41 fveq2d R NzRing x M y M coe 1 x P y deg 1 R x P y = coe 1 x P y deg 1 R x + deg 1 R y
52 eqid R = R
53 1 19 52 4 9 23 25 16 27 18 40 coe1mul4 R NzRing x M y M coe 1 x P y deg 1 R x + deg 1 R y = coe 1 x deg 1 R x R coe 1 y deg 1 R y
54 9 28 2 mon1pldg y M coe 1 y deg 1 R y = 1 R
55 54 ad2antll R NzRing x M y M coe 1 y deg 1 R y = 1 R
56 30 55 oveq12d R NzRing x M y M coe 1 x deg 1 R x R coe 1 y deg 1 R y = 1 R R 1 R
57 eqid Base R = Base R
58 57 28 ringidcl R Ring 1 R Base R
59 57 52 28 ringlidm R Ring 1 R Base R 1 R R 1 R = 1 R
60 24 58 59 syl2anc2 R NzRing 1 R R 1 R = 1 R
61 60 adantr R NzRing x M y M 1 R R 1 R = 1 R
62 56 61 eqtrd R NzRing x M y M coe 1 x deg 1 R x R coe 1 y deg 1 R y = 1 R
63 53 62 eqtrd R NzRing x M y M coe 1 x P y deg 1 R x + deg 1 R y = 1 R
64 51 63 eqtrd R NzRing x M y M coe 1 x P y deg 1 R x P y = 1 R
65 1 4 23 9 2 28 ismon1p x P y M x P y Base P x P y 0 P coe 1 x P y deg 1 R x P y = 1 R
66 21 50 64 65 syl3anbrc R NzRing x M y M x P y M
67 66 ralrimivva R NzRing x M y M x P y M
68 3 ringmgp P Ring U Mnd
69 14 68 syl R NzRing U Mnd
70 3 4 mgpbas Base P = Base U
71 3 8 ringidval 1 P = 0 U
72 3 19 mgpplusg P = + U
73 70 71 72 issubm U Mnd M SubMnd U M Base P 1 P M x M y M x P y M
74 69 73 syl R NzRing M SubMnd U M Base P 1 P M x M y M x P y M
75 7 11 67 74 mpbir3and R NzRing M SubMnd U