prmidl0

Description: The zero ideal of a commutative ring R is a prime ideal if and only if R is an integral domain. (Contributed by Thierry Arnoux, 30-Jun-2024)

		Ref	Expression
	Hypothesis	prmidl0.1	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	prmidl0	$⊢ (R \in CRing \land \{\underset{˙}{0}\} \in PrmIdeal (R)) \leftrightarrow R \in IDomn$

Proof

Step	Hyp	Ref	Expression
1		prmidl0.1	$⊢ \underset{˙}{0} = 0_{R}$
2		df-3an	$⊢ (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\}))) \leftrightarrow ((\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R}) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\})))$
3		crngring	$⊢ R \in CRing \to R \in Ring$
4	3	ad2antrr	$⊢ ((R \in CRing \land \{\underset{˙}{0}\} \in LIdeal (R)) \land \neg R \in NzRing) \to R \in Ring$
5		0ringnnzr	$⊢ R \in Ring \to (\|{Base}_{R}\| = 1 \leftrightarrow \neg R \in NzRing)$
6	5	biimpar	$⊢ (R \in Ring \land \neg R \in NzRing) \to \|{Base}_{R}\| = 1$
7	4 6	sylancom	$⊢ ((R \in CRing \land \{\underset{˙}{0}\} \in LIdeal (R)) \land \neg R \in NzRing) \to \|{Base}_{R}\| = 1$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	8 1	0ring	$⊢ (R \in Ring \land \|{Base}_{R}\| = 1) \to {Base}_{R} = \{\underset{˙}{0}\}$
10	4 7 9	syl2anc	$⊢ ((R \in CRing \land \{\underset{˙}{0}\} \in LIdeal (R)) \land \neg R \in NzRing) \to {Base}_{R} = \{\underset{˙}{0}\}$
11	10	eqcomd	$⊢ ((R \in CRing \land \{\underset{˙}{0}\} \in LIdeal (R)) \land \neg R \in NzRing) \to \{\underset{˙}{0}\} = {Base}_{R}$
12	11	ex	$⊢ (R \in CRing \land \{\underset{˙}{0}\} \in LIdeal (R)) \to (\neg R \in NzRing \to \{\underset{˙}{0}\} = {Base}_{R})$
13	12	necon1ad	$⊢ (R \in CRing \land \{\underset{˙}{0}\} \in LIdeal (R)) \to (\{\underset{˙}{0}\} \neq {Base}_{R} \to R \in NzRing)$
14	13	impr	$⊢ (R \in CRing \land (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R})) \to R \in NzRing$
15		nzrring	$⊢ R \in NzRing \to R \in Ring$
16		eqid	$⊢ LIdeal (R) = LIdeal (R)$
17	16 1	lidl0	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in LIdeal (R)$
18	15 17	syl	$⊢ R \in NzRing \to \{\underset{˙}{0}\} \in LIdeal (R)$
19	1	fvexi	$⊢ \underset{˙}{0} \in V$
20		hashsng	$⊢ \underset{˙}{0} \in V \to \|\{\underset{˙}{0}\}\| = 1$
21	19 20	ax-mp	$⊢ \|\{\underset{˙}{0}\}\| = 1$
22		1re	$⊢ 1 \in ℝ$
23	21 22	eqeltri	$⊢ \|\{\underset{˙}{0}\}\| \in ℝ$
24	23	a1i	$⊢ R \in NzRing \to \|\{\underset{˙}{0}\}\| \in ℝ$
25	8	isnzr2hash	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1 < \|{Base}_{R}\|)$
26	25	simprbi	$⊢ R \in NzRing \to 1 < \|{Base}_{R}\|$
27	21 26	eqbrtrid	$⊢ R \in NzRing \to \|\{\underset{˙}{0}\}\| < \|{Base}_{R}\|$
28	24 27	ltned	$⊢ R \in NzRing \to \|\{\underset{˙}{0}\}\| \neq \|{Base}_{R}\|$
29		fveq2	$⊢ \{\underset{˙}{0}\} = {Base}_{R} \to \|\{\underset{˙}{0}\}\| = \|{Base}_{R}\|$
30	29	necon3i	$⊢ \|\{\underset{˙}{0}\}\| \neq \|{Base}_{R}\| \to \{\underset{˙}{0}\} \neq {Base}_{R}$
31	28 30	syl	$⊢ R \in NzRing \to \{\underset{˙}{0}\} \neq {Base}_{R}$
32	18 31	jca	$⊢ R \in NzRing \to (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R})$
33	32	adantl	$⊢ (R \in CRing \land R \in NzRing) \to (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R})$
34	14 33	impbida	$⊢ R \in CRing \to ((\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R}) \leftrightarrow R \in NzRing)$
35	19	elsn2	$⊢ x \cdot_{R} y \in \{\underset{˙}{0}\} \leftrightarrow x \cdot_{R} y = \underset{˙}{0}$
36		velsn	$⊢ x \in \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0}$
37		velsn	$⊢ y \in \{\underset{˙}{0}\} \leftrightarrow y = \underset{˙}{0}$
38	36 37	orbi12i	$⊢ (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\}) \leftrightarrow (x = \underset{˙}{0} \lor y = \underset{˙}{0})$
39	35 38	imbi12i	$⊢ (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\})) \leftrightarrow (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))$
40	39	2ralbii	$⊢ \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\})) \leftrightarrow \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))$
41	40	a1i	$⊢ R \in CRing \to (\forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\})) \leftrightarrow \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})))$
42	34 41	anbi12d	$⊢ R \in CRing \to (((\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R}) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\}))) \leftrightarrow (R \in NzRing \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))))$
43	2 42	bitrid	$⊢ R \in CRing \to ((\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\}))) \leftrightarrow (R \in NzRing \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))))$
44	43	pm5.32i	$⊢ (R \in CRing \land (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\})))) \leftrightarrow (R \in CRing \land (R \in NzRing \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))))$
45		eqid	$⊢ \cdot_{R} = \cdot_{R}$
46	8 45	isprmidlc	$⊢ R \in CRing \to (\{\underset{˙}{0}\} \in PrmIdeal (R) \leftrightarrow (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\}))))$
47	46	pm5.32i	$⊢ (R \in CRing \land \{\underset{˙}{0}\} \in PrmIdeal (R)) \leftrightarrow (R \in CRing \land (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y \in \{\underset{˙}{0}\} \to (x \in \{\underset{˙}{0}\} \lor y \in \{\underset{˙}{0}\}))))$
48		df-idom	$⊢ IDomn = CRing \cap Domn$
49	48	eleq2i	$⊢ R \in IDomn \leftrightarrow R \in (CRing \cap Domn)$
50		elin	$⊢ R \in (CRing \cap Domn) \leftrightarrow (R \in CRing \land R \in Domn)$
51	8 45 1	isdomn	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})))$
52	51	anbi2i	$⊢ (R \in CRing \land R \in Domn) \leftrightarrow (R \in CRing \land (R \in NzRing \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))))$
53	49 50 52	3bitri	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land (R \in NzRing \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))))$
54	44 47 53	3bitr4i	$⊢ (R \in CRing \land \{\underset{˙}{0}\} \in PrmIdeal (R)) \leftrightarrow R \in IDomn$

Metamath Proof Explorer

Theorem prmidl0

Proof