Theorem isfieldidl2

Description: Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 30-Jun-2026)

	Ref	Expression
Hypotheses	isfieldidl.b	$$⊢B={\mathrm{Base}}_R$$
	isfieldidl.0	$$⊢\underset{\dot{}}{0}=0_R$$
	isfieldidl.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
Assertion	isfieldidl2	$$⊢R\in \mathrm{Field}\leftrightarrow \left(R\in \mathrm{CRing}\wedge B\ne \left\{\underset{\dot{}}{0}\right\}\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfieldidl.b	$$⊢B={\mathrm{Base}}_R$$
2		isfieldidl.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		isfieldidl.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
4		eqid	$$⊢1_R=1_R$$
5	1 2 3 4	isfieldidl	$$⊢R\in \mathrm{Field}\leftrightarrow \left(R\in \mathrm{CRing}\wedge \underset{\dot{}}{0}\ne 1_R\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)$$
6		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
7		eqcom	$$⊢\underset{\dot{}}{0}=1_R\leftrightarrow 1_R=\underset{\dot{}}{0}$$
8	1 2 4	0ring01eqbi2	$$⊢R\in \mathrm{Ring}\to \left(B=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow 1_R=\underset{\dot{}}{0}\right)$$
9	7 8	bitr4id	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{0}=1_R\leftrightarrow B=\left\{\underset{\dot{}}{0}\right\}\right)$$
10	6 9	syl	$$⊢R\in \mathrm{CRing}\to \left(\underset{\dot{}}{0}=1_R\leftrightarrow B=\left\{\underset{\dot{}}{0}\right\}\right)$$
11	10	necon3bid	$$⊢R\in \mathrm{CRing}\to \left(\underset{\dot{}}{0}\ne 1_R\leftrightarrow B\ne \left\{\underset{\dot{}}{0}\right\}\right)$$
12	11	anbi1d	$$⊢R\in \mathrm{CRing}\to \left(\left(\underset{\dot{}}{0}\ne 1_R\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\leftrightarrow \left(B\ne \left\{\underset{\dot{}}{0}\right\}\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\right)$$
13	12	pm5.32i	$$⊢\left(R\in \mathrm{CRing}\wedge \left(\underset{\dot{}}{0}\ne 1_R\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\right)\leftrightarrow \left(R\in \mathrm{CRing}\wedge \left(B\ne \left\{\underset{\dot{}}{0}\right\}\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\right)$$
14		3anass	$$⊢\left(R\in \mathrm{CRing}\wedge \underset{\dot{}}{0}\ne 1_R\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\leftrightarrow \left(R\in \mathrm{CRing}\wedge \left(\underset{\dot{}}{0}\ne 1_R\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\right)$$
15		3anass	$$⊢\left(R\in \mathrm{CRing}\wedge B\ne \left\{\underset{\dot{}}{0}\right\}\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\leftrightarrow \left(R\in \mathrm{CRing}\wedge \left(B\ne \left\{\underset{\dot{}}{0}\right\}\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\right)$$
16	13 14 15	3bitr4i	$$⊢\left(R\in \mathrm{CRing}\wedge \underset{\dot{}}{0}\ne 1_R\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\leftrightarrow \left(R\in \mathrm{CRing}\wedge B\ne \left\{\underset{\dot{}}{0}\right\}\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)$$
17	5 16	bitri	$$⊢R\in \mathrm{Field}\leftrightarrow \left(R\in \mathrm{CRing}\wedge B\ne \left\{\underset{\dot{}}{0}\right\}\wedge I=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)$$