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 \in NzRing \to M \in 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 \in M \to x \in {Base}_{P}$
6	5	ssriv	$⊢ M \subseteq {Base}_{P}$
7	6	a1i	$⊢ R \in NzRing \to M \subseteq {Base}_{P}$
8		eqid	$⊢ 1_{P} = 1_{P}$
9		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
10	1 8 2 9	mon1pid	$⊢ R \in NzRing \to (1_{P} \in M \land \deg_{1} (R) (1_{P}) = 0)$
11	10	simpld	$⊢ R \in NzRing \to 1_{P} \in M$
12	1	ply1nz	$⊢ R \in NzRing \to P \in NzRing$
13		nzrring	$⊢ P \in NzRing \to P \in Ring$
14	12 13	syl	$⊢ R \in NzRing \to P \in Ring$
15	14	adantr	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to P \in Ring$
16	5	ad2antrl	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to x \in {Base}_{P}$
17		simprr	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to y \in M$
18	6 17	sseldi	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to y \in {Base}_{P}$
19		eqid	$⊢ \cdot_{P} = \cdot_{P}$
20	4 19	ringcl	$⊢ (P \in Ring \land x \in {Base}_{P} \land y \in {Base}_{P}) \to x \cdot_{P} y \in {Base}_{P}$
21	15 16 18 20	syl3anc	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to x \cdot_{P} y \in {Base}_{P}$
22		eqid	$⊢ RLReg (R) = RLReg (R)$
23		eqid	$⊢ 0_{P} = 0_{P}$
24		nzrring	$⊢ R \in NzRing \to R \in Ring$
25	24	adantr	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to R \in Ring$
26	1 23 2	mon1pn0	$⊢ x \in M \to x \neq 0_{P}$
27	26	ad2antrl	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to x \neq 0_{P}$
28		eqid	$⊢ 1_{R} = 1_{R}$
29	9 28 2	mon1pldg	$⊢ x \in M \to {coe}_{1} (x) (\deg_{1} (R) (x)) = 1_{R}$
30	29	ad2antrl	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (x) (\deg_{1} (R) (x)) = 1_{R}$
31		eqid	$⊢ Unit (R) = Unit (R)$
32	22 31	unitrrg	$⊢ R \in Ring \to Unit (R) \subseteq RLReg (R)$
33	24 32	syl	$⊢ R \in NzRing \to Unit (R) \subseteq RLReg (R)$
34	31 28	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
35	24 34	syl	$⊢ R \in NzRing \to 1_{R} \in Unit (R)$
36	33 35	sseldd	$⊢ R \in NzRing \to 1_{R} \in RLReg (R)$
37	36	adantr	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to 1_{R} \in RLReg (R)$
38	30 37	eqeltrd	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (x) (\deg_{1} (R) (x)) \in RLReg (R)$
39	1 23 2	mon1pn0	$⊢ y \in M \to y \neq 0_{P}$
40	39	ad2antll	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to y \neq 0_{P}$
41	9 1 22 4 19 23 25 16 27 38 18 40	deg1mul2	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to \deg_{1} (R) (x \cdot_{P} y) = \deg_{1} (R) (x) + \deg_{1} (R) (y)$
42	9 1 23 4	deg1nn0cl	$⊢ (R \in Ring \land x \in {Base}_{P} \land x \neq 0_{P}) \to \deg_{1} (R) (x) \in ℕ_{0}$
43	25 16 27 42	syl3anc	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to \deg_{1} (R) (x) \in ℕ_{0}$
44	9 1 23 4	deg1nn0cl	$⊢ (R \in Ring \land y \in {Base}_{P} \land y \neq 0_{P}) \to \deg_{1} (R) (y) \in ℕ_{0}$
45	25 18 40 44	syl3anc	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to \deg_{1} (R) (y) \in ℕ_{0}$
46	43 45	nn0addcld	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to \deg_{1} (R) (x) + \deg_{1} (R) (y) \in ℕ_{0}$
47	41 46	eqeltrd	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to \deg_{1} (R) (x \cdot_{P} y) \in ℕ_{0}$
48	9 1 23 4	deg1nn0clb	$⊢ (R \in Ring \land x \cdot_{P} y \in {Base}_{P}) \to (x \cdot_{P} y \neq 0_{P} \leftrightarrow \deg_{1} (R) (x \cdot_{P} y) \in ℕ_{0})$
49	25 21 48	syl2anc	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to (x \cdot_{P} y \neq 0_{P} \leftrightarrow \deg_{1} (R) (x \cdot_{P} y) \in ℕ_{0})$
50	47 49	mpbird	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to x \cdot_{P} y \neq 0_{P}$
51	41	fveq2d	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (x \cdot_{P} y) (\deg_{1} (R) (x \cdot_{P} y)) = {coe}_{1} (x \cdot_{P} y) (\deg_{1} (R) (x) + \deg_{1} (R) (y))$
52		eqid	$⊢ \cdot_{R} = \cdot_{R}$
53	1 19 52 4 9 23 25 16 27 18 40	coe1mul4	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (x \cdot_{P} y) (\deg_{1} (R) (x) + \deg_{1} (R) (y)) = {coe}_{1} (x) (\deg_{1} (R) (x)) \cdot_{R} {coe}_{1} (y) (\deg_{1} (R) (y))$
54	9 28 2	mon1pldg	$⊢ y \in M \to {coe}_{1} (y) (\deg_{1} (R) (y)) = 1_{R}$
55	54	ad2antll	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (y) (\deg_{1} (R) (y)) = 1_{R}$
56	30 55	oveq12d	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (x) (\deg_{1} (R) (x)) \cdot_{R} {coe}_{1} (y) (\deg_{1} (R) (y)) = 1_{R} \cdot_{R} 1_{R}$
57		eqid	$⊢ {Base}_{R} = {Base}_{R}$
58	57 28	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
59	57 52 28	ringlidm	$⊢ (R \in Ring \land 1_{R} \in {Base}_{R}) \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
60	24 58 59	syl2anc2	$⊢ R \in NzRing \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
61	60	adantr	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
62	56 61	eqtrd	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (x) (\deg_{1} (R) (x)) \cdot_{R} {coe}_{1} (y) (\deg_{1} (R) (y)) = 1_{R}$
63	53 62	eqtrd	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (x \cdot_{P} y) (\deg_{1} (R) (x) + \deg_{1} (R) (y)) = 1_{R}$
64	51 63	eqtrd	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to {coe}_{1} (x \cdot_{P} y) (\deg_{1} (R) (x \cdot_{P} y)) = 1_{R}$
65	1 4 23 9 2 28	ismon1p	$⊢ x \cdot_{P} y \in M \leftrightarrow (x \cdot_{P} y \in {Base}_{P} \land x \cdot_{P} y \neq 0_{P} \land {coe}_{1} (x \cdot_{P} y) (\deg_{1} (R) (x \cdot_{P} y)) = 1_{R})$
66	21 50 64 65	syl3anbrc	$⊢ (R \in NzRing \land (x \in M \land y \in M)) \to x \cdot_{P} y \in M$
67	66	ralrimivva	$⊢ R \in NzRing \to \forall x \in M \forall y \in M x \cdot_{P} y \in M$
68	3	ringmgp	$⊢ P \in Ring \to U \in Mnd$
69	14 68	syl	$⊢ R \in NzRing \to U \in Mnd$
70	3 4	mgpbas	$⊢ {Base}_{P} = {Base}_{U}$
71	3 8	ringidval	$⊢ 1_{P} = 0_{U}$
72	3 19	mgpplusg	$⊢ \cdot_{P} = +_{U}$
73	70 71 72	issubm	$⊢ U \in Mnd \to (M \in SubMnd (U) \leftrightarrow (M \subseteq {Base}_{P} \land 1_{P} \in M \land \forall x \in M \forall y \in M x \cdot_{P} y \in M))$
74	69 73	syl	$⊢ R \in NzRing \to (M \in SubMnd (U) \leftrightarrow (M \subseteq {Base}_{P} \land 1_{P} \in M \land \forall x \in M \forall y \in M x \cdot_{P} y \in M))$
75	7 11 67 74	mpbir3and	$⊢ R \in NzRing \to M \in SubMnd (U)$

Metamath Proof Explorer

Theorem mon1psubm

Proof