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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
mon1psubm.m ⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
mon1psubm.u ⊢ 𝑈 = ( mulGrp ‘ 𝑃 )
Assertion mon1psubm ( 𝑅 ∈ NzRing → 𝑀 ∈ ( SubMnd ‘ 𝑈 ) )

Proof

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