Theorem 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{\dot{}}{0}=0_R$$
Assertion	prmidl0	Could not format assertion : No typesetting found for |- ( ( R e. CRing /\ { .0. } e. ( PrmIdeal ` R ) ) <-> R e. IDomn ) with typecode |-

Proof

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