Theorem isidom3

Description: The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by AV, 12-Jul-2026)

	Ref	Expression
Hypotheses	isidom3.b	$$⊢B={\mathrm{Base}}_R$$
	isidom3.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isidom3.0	$$⊢\underset{\dot{}}{0}=0_R$$
	isidom3.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	isidom3	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isidom3.b	$$⊢B={\mathrm{Base}}_R$$
2		isidom3.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		isidom3.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		isidom3.1	$$⊢\underset{\dot{}}{1}=1_R$$
5		isidom2	Could not format ( R e. IDomn <-> ( R e. PrmRing /\ R e. CRing ) ) : No typesetting found for |- ( R e. IDomn <-> ( R e. PrmRing /\ R e. CRing ) ) with typecode |-
6		eqid	$$⊢\mathrm{PrmIdeal}\left(R\right)=\mathrm{PrmIdeal}\left(R\right)$$
7	3 6	isprmrng	Could not format ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. ( PrmIdeal ` R ) ) ) with typecode |-
8	1 2	isprmidlc	$$⊢R\in \mathrm{CRing}\to \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{PrmIdeal}\left(R\right)\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)\wedge \left\{\underset{\dot{}}{0}\right\}\ne B\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\right)$$
9		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
10	9	biantrurd	$$⊢R\in \mathrm{CRing}\to \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{PrmIdeal}\left(R\right)\leftrightarrow \left(R\in \mathrm{Ring}\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{PrmIdeal}\left(R\right)\right)\right)$$
11		3anass	$$⊢\left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)\wedge \left\{\underset{\dot{}}{0}\right\}\ne B\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)\wedge \left(\left\{\underset{\dot{}}{0}\right\}\ne B\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\right)$$
12		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
13	12 3	2idl0	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{2Ideal}\left(R\right)$$
14	9 13	syl	$$⊢R\in \mathrm{CRing}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{2Ideal}\left(R\right)$$
15	14	2idllidld	$$⊢R\in \mathrm{CRing}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)$$
16	15	biantrurd	$$⊢R\in \mathrm{CRing}\to \left(\left(\left\{\underset{\dot{}}{0}\right\}\ne B\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)\wedge \left(\left\{\underset{\dot{}}{0}\right\}\ne B\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\right)\right)$$
17	1 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
18		eleq2	$$⊢\left\{\underset{\dot{}}{0}\right\}=B\to \left(\underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{1}\in B\right)$$
19		elsni	$$⊢\underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0}\right\}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
20	19	eqcomd	$$⊢\underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0}\right\}\to \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
21	18 20	biimtrrdi	$$⊢\left\{\underset{\dot{}}{0}\right\}=B\to \left(\underset{\dot{}}{1}\in B\to \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
22	17 21	syl5com	$$⊢R\in \mathrm{Ring}\to \left(\left\{\underset{\dot{}}{0}\right\}=B\to \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
23	1 3 4	0ring01eqbi	$$⊢R\in \mathrm{Ring}\to \left(B\approx 1_{𝑜}\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
24		eqcom	$$⊢\underset{\dot{}}{1}=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
25	23 24	bitrdi	$$⊢R\in \mathrm{Ring}\to \left(B\approx 1_{𝑜}\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
26	1 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
27		en1eqsn	$$⊢\left(\underset{\dot{}}{0}\in B\wedge B\approx 1_{𝑜}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
28	27	eqcomd	$$⊢\left(\underset{\dot{}}{0}\in B\wedge B\approx 1_{𝑜}\right)\to \left\{\underset{\dot{}}{0}\right\}=B$$
29	28	ex	$$⊢\underset{\dot{}}{0}\in B\to \left(B\approx 1_{𝑜}\to \left\{\underset{\dot{}}{0}\right\}=B\right)$$
30	26 29	syl	$$⊢R\in \mathrm{Ring}\to \left(B\approx 1_{𝑜}\to \left\{\underset{\dot{}}{0}\right\}=B\right)$$
31	25 30	sylbird	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{0}=\underset{\dot{}}{1}\to \left\{\underset{\dot{}}{0}\right\}=B\right)$$
32	22 31	impbid	$$⊢R\in \mathrm{Ring}\to \left(\left\{\underset{\dot{}}{0}\right\}=B\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
33	9 32	syl	$$⊢R\in \mathrm{CRing}\to \left(\left\{\underset{\dot{}}{0}\right\}=B\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
34	33	necon3bid	$$⊢R\in \mathrm{CRing}\to \left(\left\{\underset{\dot{}}{0}\right\}\ne B\leftrightarrow \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)$$
35		ovex	$$⊢a\underset{\dot{}}{·}b\in \mathrm{V}$$
36	35	elsn	$$⊢a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow a\underset{\dot{}}{·}b=\underset{\dot{}}{0}$$
37		velsn	$$⊢a\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow a=\underset{\dot{}}{0}$$
38		velsn	$$⊢b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow b=\underset{\dot{}}{0}$$
39	37 38	orbi12i	$$⊢\left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)$$
40	36 39	imbi12i	$$⊢\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\leftrightarrow \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)$$
41	40	a1i	$$⊢R\in \mathrm{CRing}\to \left(\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\leftrightarrow \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)$$
42	41	2ralbidv	$$⊢R\in \mathrm{CRing}\to \left(\forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\leftrightarrow \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)$$
43	34 42	anbi12d	$$⊢R\in \mathrm{CRing}\to \left(\left(\left\{\underset{\dot{}}{0}\right\}\ne B\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\ne \underset{\dot{}}{1}\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)\right)$$
44	16 43	bitr3d	$$⊢R\in \mathrm{CRing}\to \left(\left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)\wedge \left(\left\{\underset{\dot{}}{0}\right\}\ne B\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\ne \underset{\dot{}}{1}\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)\right)$$
45	11 44	bitrid	$$⊢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 B\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b\in \left\{\underset{\dot{}}{0}\right\}\to \left(a\in \left\{\underset{\dot{}}{0}\right\}\vee b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\ne \underset{\dot{}}{1}\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)\right)$$
46	8 10 45	3bitr3d	$$⊢R\in \mathrm{CRing}\to \left(\left(R\in \mathrm{Ring}\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{PrmIdeal}\left(R\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\ne \underset{\dot{}}{1}\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)\right)$$
47	7 46	bitrid	Could not format ( R e. CRing -> ( R e. PrmRing <-> ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) ) : No typesetting found for |- ( R e. CRing -> ( R e. PrmRing <-> ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) ) with typecode |-
48	47	pm5.32i	Could not format ( ( R e. CRing /\ R e. PrmRing ) <-> ( R e. CRing /\ ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) ) : No typesetting found for |- ( ( R e. CRing /\ R e. PrmRing ) <-> ( R e. CRing /\ ( .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) ) with typecode |-
49		ancom	Could not format ( ( R e. PrmRing /\ R e. CRing ) <-> ( R e. CRing /\ R e. PrmRing ) ) : No typesetting found for |- ( ( R e. PrmRing /\ R e. CRing ) <-> ( R e. CRing /\ R e. PrmRing ) ) with typecode |-
50		3anass	$$⊢\left(R\in \mathrm{CRing}\wedge \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(R\in \mathrm{CRing}\wedge \left(\underset{\dot{}}{0}\ne \underset{\dot{}}{1}\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)\right)$$
51	48 49 50	3bitr4i	Could not format ( ( R e. PrmRing /\ R e. CRing ) <-> ( R e. CRing /\ .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) : No typesetting found for |- ( ( R e. PrmRing /\ R e. CRing ) <-> ( R e. CRing /\ .0. =/= .1. /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) ) with typecode |-
52	5 51	bitri	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\wedge \forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\right)$$