Theorem mon1pid

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

	Ref	Expression
Hypotheses	mon1pid.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mon1pid.o	⊢ 1 = ( 1r ‘ 𝑃 )
	mon1pid.m	⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
	mon1pid.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
Assertion	mon1pid	⊢ ( 𝑅 ∈ NzRing → ( 1 ∈ 𝑀 ∧ ( 𝐷 ‘ 1 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		mon1pid.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		mon1pid.o	⊢ 1 = ( 1r ‘ 𝑃 )
3		mon1pid.m	⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
4		mon1pid.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
5	1	ply1nz	⊢ ( 𝑅 ∈ NzRing → 𝑃 ∈ NzRing )
6		nzrring	⊢ ( 𝑃 ∈ NzRing → 𝑃 ∈ Ring )
7		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8	7 2	ringidcl	⊢ ( 𝑃 ∈ Ring → 1 ∈ ( Base ‘ 𝑃 ) )
9	5 6 8	3syl	⊢ ( 𝑅 ∈ NzRing → 1 ∈ ( Base ‘ 𝑃 ) )
10		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
11	2 10	nzrnz	⊢ ( 𝑃 ∈ NzRing → 1 ≠ ( 0g ‘ 𝑃 ) )
12	5 11	syl	⊢ ( 𝑅 ∈ NzRing → 1 ≠ ( 0g ‘ 𝑃 ) )
13		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
14		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
15		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
16	1 14 15 2	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = 1 )
17	13 16	syl	⊢ ( 𝑅 ∈ NzRing → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = 1 )
18	17	fveq2d	⊢ ( 𝑅 ∈ NzRing → ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( coe1 ‘ 1 ) )
19		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20	19 15	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
21		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
22	1 14 19 21	coe1scl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
23	13 20 22	syl2anc2	⊢ ( 𝑅 ∈ NzRing → ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
24	18 23	eqtr3d	⊢ ( 𝑅 ∈ NzRing → ( coe1 ‘ 1 ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
25	17	fveq2d	⊢ ( 𝑅 ∈ NzRing → ( 𝐷 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝐷 ‘ 1 ) )
26	13 20	syl	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27	15 21	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
28	4 1 19 14 21	deg1scl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐷 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = 0 )
29	13 26 27 28	syl3anc	⊢ ( 𝑅 ∈ NzRing → ( 𝐷 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = 0 )
30	25 29	eqtr3d	⊢ ( 𝑅 ∈ NzRing → ( 𝐷 ‘ 1 ) = 0 )
31	24 30	fveq12d	⊢ ( 𝑅 ∈ NzRing → ( ( coe1 ‘ 1 ) ‘ ( 𝐷 ‘ 1 ) ) = ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 0 ) )
32		0nn0	⊢ 0 ∈ ℕ0
33		iftrue	⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
34		eqid	⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
35		fvex	⊢ ( 1r ‘ 𝑅 ) ∈ V
36	33 34 35	fvmpt	⊢ ( 0 ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 0 ) = ( 1r ‘ 𝑅 ) )
37	32 36	ax-mp	⊢ ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ‘ 0 ) = ( 1r ‘ 𝑅 )
38	31 37	eqtrdi	⊢ ( 𝑅 ∈ NzRing → ( ( coe1 ‘ 1 ) ‘ ( 𝐷 ‘ 1 ) ) = ( 1r ‘ 𝑅 ) )
39	1 7 10 4 3 15	ismon1p	⊢ ( 1 ∈ 𝑀 ↔ ( 1 ∈ ( Base ‘ 𝑃 ) ∧ 1 ≠ ( 0g ‘ 𝑃 ) ∧ ( ( coe1 ‘ 1 ) ‘ ( 𝐷 ‘ 1 ) ) = ( 1r ‘ 𝑅 ) ) )
40	9 12 38 39	syl3anbrc	⊢ ( 𝑅 ∈ NzRing → 1 ∈ 𝑀 )
41	40 30	jca	⊢ ( 𝑅 ∈ NzRing → ( 1 ∈ 𝑀 ∧ ( 𝐷 ‘ 1 ) = 0 ) )