Theorem mon1pid

Description: Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	mon1pid.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	mon1pid.o	$$⊢\underset{\dot{}}{1}=1_P$$
	mon1pid.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
	mon1pid.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
Assertion	mon1pid	$$⊢R\in \mathrm{NzRing}\to \left(\underset{\dot{}}{1}\in M\wedge D\left(\underset{\dot{}}{1}\right)=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		mon1pid.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		mon1pid.o	$$⊢\underset{\dot{}}{1}=1_P$$
3		mon1pid.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
4		mon1pid.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
5	1	ply1nz	$$⊢R\in \mathrm{NzRing}\to P\in \mathrm{NzRing}$$
6		nzrring	$$⊢P\in \mathrm{NzRing}\to P\in \mathrm{Ring}$$
7		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
8	7 2	ringidcl	$$⊢P\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_P$$
9	5 6 8	3syl	$$⊢R\in \mathrm{NzRing}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_P$$
10		eqid	$$⊢0_P=0_P$$
11	2 10	nzrnz	$$⊢P\in \mathrm{NzRing}\to \underset{\dot{}}{1}\ne 0_P$$
12	5 11	syl	$$⊢R\in \mathrm{NzRing}\to \underset{\dot{}}{1}\ne 0_P$$
13		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
14		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
15		eqid	$$⊢1_R=1_R$$
16	1 14 15 2	ply1scl1	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left(P\right)\left(1_R\right)=\underset{\dot{}}{1}$$
17	13 16	syl	$$⊢R\in \mathrm{NzRing}\to \mathrm{algSc}\left(P\right)\left(1_R\right)=\underset{\dot{}}{1}$$
18	17	fveq2d	$$⊢R\in \mathrm{NzRing}\to {\mathrm{coe}}_1\left(\mathrm{algSc}\left(P\right)\left(1_R\right)\right)={\mathrm{coe}}_1\left(\underset{\dot{}}{1}\right)$$
19		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
20	19 15	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
21		eqid	$$⊢0_R=0_R$$
22	1 14 19 21	coe1scl	$$⊢\left(R\in \mathrm{Ring}\wedge 1_R\in {\mathrm{Base}}_R\right)\to {\mathrm{coe}}_1\left(\mathrm{algSc}\left(P\right)\left(1_R\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,1_R,0_R\right)\right)$$
23	13 20 22	syl2anc2	$$⊢R\in \mathrm{NzRing}\to {\mathrm{coe}}_1\left(\mathrm{algSc}\left(P\right)\left(1_R\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,1_R,0_R\right)\right)$$
24	18 23	eqtr3d	$$⊢R\in \mathrm{NzRing}\to {\mathrm{coe}}_1\left(\underset{\dot{}}{1}\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,1_R,0_R\right)\right)$$
25	17	fveq2d	$$⊢R\in \mathrm{NzRing}\to D\left(\mathrm{algSc}\left(P\right)\left(1_R\right)\right)=D\left(\underset{\dot{}}{1}\right)$$
26	13 20	syl	$$⊢R\in \mathrm{NzRing}\to 1_R\in {\mathrm{Base}}_R$$
27	15 21	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
28	4 1 19 14 21	deg1scl	$$⊢\left(R\in \mathrm{Ring}\wedge 1_R\in {\mathrm{Base}}_R\wedge 1_R\ne 0_R\right)\to D\left(\mathrm{algSc}\left(P\right)\left(1_R\right)\right)=0$$
29	13 26 27 28	syl3anc	$$⊢R\in \mathrm{NzRing}\to D\left(\mathrm{algSc}\left(P\right)\left(1_R\right)\right)=0$$
30	25 29	eqtr3d	$$⊢R\in \mathrm{NzRing}\to D\left(\underset{\dot{}}{1}\right)=0$$
31	24 30	fveq12d	$$⊢R\in \mathrm{NzRing}\to {\mathrm{coe}}_1\left(\underset{\dot{}}{1}\right)\left(D\left(\underset{\dot{}}{1}\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,1_R,0_R\right)\right)\left(0\right)$$
32		0nn0	$$⊢0\in {\mathbb{N}}_0$$
33		iftrue	$$⊢x=0\to if\left(x=0,1_R,0_R\right)=1_R$$
34		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼if\left(x=0,1_R,0_R\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,1_R,0_R\right)\right)$$
35		fvex	$$⊢1_R\in \mathrm{V}$$
36	33 34 35	fvmpt	$$⊢0\in {\mathbb{N}}_0\to \left(x\in {\mathbb{N}}_0⟼if\left(x=0,1_R,0_R\right)\right)\left(0\right)=1_R$$
37	32 36	ax-mp	$$⊢\left(x\in {\mathbb{N}}_0⟼if\left(x=0,1_R,0_R\right)\right)\left(0\right)=1_R$$
38	31 37	eqtrdi	$$⊢R\in \mathrm{NzRing}\to {\mathrm{coe}}_1\left(\underset{\dot{}}{1}\right)\left(D\left(\underset{\dot{}}{1}\right)\right)=1_R$$
39	1 7 10 4 3 15	ismon1p	$$⊢\underset{\dot{}}{1}\in M\leftrightarrow \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_P\wedge \underset{\dot{}}{1}\ne 0_P\wedge {\mathrm{coe}}_1\left(\underset{\dot{}}{1}\right)\left(D\left(\underset{\dot{}}{1}\right)\right)=1_R\right)$$
40	9 12 38 39	syl3anbrc	$$⊢R\in \mathrm{NzRing}\to \underset{\dot{}}{1}\in M$$
41	40 30	jca	$$⊢R\in \mathrm{NzRing}\to \left(\underset{\dot{}}{1}\in M\wedge D\left(\underset{\dot{}}{1}\right)=0\right)$$