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 𝑆 ) = ∅ )