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 bilani ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1r ‘ 𝑅 ) ) )
12 11 simp3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1r ‘ 𝑅 ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → 𝑅 ∈ Ring )
14 11 simp1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
15 11 simp2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
16 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17 eqid ⊢ ( coe1 ‘ 𝑝 ) = ( coe1 ‘ 𝑝 )
18 8 5 7 6 16 17 deg1ldg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝑅 ) )
19 13 14 15 18 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝑅 ) )
20 2 16 9 0ring01eq ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
21 3 4 20 syl2anc ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
23 19 22 neeqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) ≠ ( 1r ‘ 𝑅 ) )
24 23 neneqd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑀 ) → ¬ ( ( coe1 ‘ 𝑝 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1r ‘ 𝑅 ) )
25 12 24 pm2.65da ⊢ ( 𝜑 → ¬ 𝑝 ∈ 𝑀 )
26 25 eq0rdv ⊢ ( 𝜑 → 𝑀 = ∅ )