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

Metamath Proof Explorer

Theorem 0ringmon1p

Description: There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025)

Ref Expression
Hypotheses 0ringmon1p.1 ⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
0ringmon1p.2 ⊢ 𝐵 = ( Base ‘ 𝑅 )
0ringmon1p.3 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
0ringmon1p.4 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
Assertion 0ringmon1p ( 𝜑 → 𝑀 = ∅ )

Proof

Step Hyp Ref Expression
1 0ringmon1p.1 ⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
2 0ringmon1p.2 ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 0ringmon1p.3 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 0ringmon1p.4 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
5 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
6 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
7 eqid ⊢ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ 𝑅 ) )
8 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 5 6 7 8 1 9 ismon1p ⊢ ( 𝑝 ∈ 𝑀 ↔ ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1r ‘ 𝑅 ) ) )
11 10 biimpi ⊢ ( 𝑝 ∈ 𝑀 → ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1r ‘ 𝑅 ) ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1r ‘ 𝑅 ) ) )
13 12 simp3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1r ‘ 𝑅 ) )
14 3 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → 𝑅 ∈ Ring )
15 12 simp1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
16 12 simp2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
17 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18 eqid ⊢ ( coe1 ‘ 𝑝 ) = ( coe1 ‘ 𝑝 )
19 8 5 7 6 17 18 deg1ldg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝑅 ) )
20 14 15 16 19 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝑅 ) )
21 2 17 9 0ring01eq ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
22 3 4 21 syl2anc ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
24 20 23 neeqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) ≠ ( 1r ‘ 𝑅 ) )
25 24 neneqd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ¬ ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1r ‘ 𝑅 ) )
26 13 25 pm2.65da ⊢ ( 𝜑 → ¬ 𝑝 ∈ 𝑀 )
27 26 eq0rdv ⊢ ( 𝜑 → 𝑀 = ∅ )