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 = ( Poly1 ` R )
mon1psubm.m 
|- M = ( Monic1p ` R )
mon1psubm.u 
|- U = ( mulGrp ` P )
Assertion mon1psubm 
|- ( R e. NzRing -> M e. ( SubMnd ` U ) )

Proof

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