This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )