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

Metamath Proof Explorer

Theorem 0ringirng

Description: A zero ring R has no integral elements. (Contributed by Thierry Arnoux, 5-Feb-2025)

Ref Expression
Hypotheses irngval.o ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
irngval.u ⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
irngval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
irngval.0 ⊢ 0 = ( 0g ‘ 𝑅 )
elirng.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
elirng.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
0ringirng.1 ⊢ ( 𝜑 → ¬ 𝑅 ∈ NzRing )
Assertion 0ringirng ( 𝜑 → ( 𝑅 IntgRing 𝑆 ) = ∅ )

Proof

Step Hyp Ref Expression
1 irngval.o ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2 irngval.u ⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
3 irngval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 irngval.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 elirng.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 elirng.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7 0ringirng.1 ⊢ ( 𝜑 → ¬ 𝑅 ∈ NzRing )
8 rex0 ⊢ ¬ ∃ 𝑝 ∈ ∅ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0
9 eqid ⊢ ( Monic1p ‘ 𝑈 ) = ( Monic1p ‘ 𝑈 )
10 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
11 2 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑈 ∈ Ring )
12 6 11 syl ⊢ ( 𝜑 → 𝑈 ∈ Ring )
13 5 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
14 3 fveq2i ⊢ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( Base ‘ 𝑅 ) )
15 0ringnnzr ⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ ¬ 𝑅 ∈ NzRing ) )
16 15 biimpar ⊢ ( ( 𝑅 ∈ Ring ∧ ¬ 𝑅 ∈ NzRing ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 )
17 13 7 16 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 )
18 14 17 eqtrid ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
19 3 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
20 2 3 ressbas2 ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ 𝑈 ) )
21 6 19 20 3syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝑈 ) )
22 21 6 eqeltrrd ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ∈ ( SubRing ‘ 𝑅 ) )
23 3 13 18 22 0ringsubrg ⊢ ( 𝜑 → ( ♯ ‘ ( Base ‘ 𝑈 ) ) = 1 )
24 9 10 12 23 0ringmon1p ⊢ ( 𝜑 → ( Monic1p ‘ 𝑈 ) = ∅ )
25 24 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ↔ ∃ 𝑝 ∈ ∅ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) )
26 8 25 mtbiri ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 )
27 1 2 3 4 5 6 elirng ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑝 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) )
28 27 simplbda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) ) → ∃ 𝑝 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 )
29 26 28 mtand ⊢ ( 𝜑 → ¬ 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) )
30 29 eq0rdv ⊢ ( 𝜑 → ( 𝑅 IntgRing 𝑆 ) = ∅ )