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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isfieldidl.0	⊢ 0 = ( 0g ‘ 𝑅 )
	isfieldidl.i	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
Assertion	isfieldidl2	⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ CRing ∧ 𝐵 ≠ { 0 } ∧ 𝐼 = { { 0 } , 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		isfieldidl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isfieldidl.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		isfieldidl.i	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
4		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
5	1 2 3 4	isfieldidl	⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ CRing ∧ 0 ≠ ( 1r ‘ 𝑅 ) ∧ 𝐼 = { { 0 } , 𝐵 } ) )
6		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
7		eqcom	⊢ ( 0 = ( 1r ‘ 𝑅 ) ↔ ( 1r ‘ 𝑅 ) = 0 )
8	1 2 4	0ring01eqbi2	⊢ ( 𝑅 ∈ Ring → ( 𝐵 = { 0 } ↔ ( 1r ‘ 𝑅 ) = 0 ) )
9	7 8	bitr4id	⊢ ( 𝑅 ∈ Ring → ( 0 = ( 1r ‘ 𝑅 ) ↔ 𝐵 = { 0 } ) )
10	6 9	syl	⊢ ( 𝑅 ∈ CRing → ( 0 = ( 1r ‘ 𝑅 ) ↔ 𝐵 = { 0 } ) )
11	10	necon3bid	⊢ ( 𝑅 ∈ CRing → ( 0 ≠ ( 1r ‘ 𝑅 ) ↔ 𝐵 ≠ { 0 } ) )
12	11	anbi1d	⊢ ( 𝑅 ∈ CRing → ( ( 0 ≠ ( 1r ‘ 𝑅 ) ∧ 𝐼 = { { 0 } , 𝐵 } ) ↔ ( 𝐵 ≠ { 0 } ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
13	12	pm5.32i	⊢ ( ( 𝑅 ∈ CRing ∧ ( 0 ≠ ( 1r ‘ 𝑅 ) ∧ 𝐼 = { { 0 } , 𝐵 } ) ) ↔ ( 𝑅 ∈ CRing ∧ ( 𝐵 ≠ { 0 } ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
14		3anass	⊢ ( ( 𝑅 ∈ CRing ∧ 0 ≠ ( 1r ‘ 𝑅 ) ∧ 𝐼 = { { 0 } , 𝐵 } ) ↔ ( 𝑅 ∈ CRing ∧ ( 0 ≠ ( 1r ‘ 𝑅 ) ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
15		3anass	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐵 ≠ { 0 } ∧ 𝐼 = { { 0 } , 𝐵 } ) ↔ ( 𝑅 ∈ CRing ∧ ( 𝐵 ≠ { 0 } ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
16	13 14 15	3bitr4i	⊢ ( ( 𝑅 ∈ CRing ∧ 0 ≠ ( 1r ‘ 𝑅 ) ∧ 𝐼 = { { 0 } , 𝐵 } ) ↔ ( 𝑅 ∈ CRing ∧ 𝐵 ≠ { 0 } ∧ 𝐼 = { { 0 } , 𝐵 } ) )
17	5 16	bitri	⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ CRing ∧ 𝐵 ≠ { 0 } ∧ 𝐼 = { { 0 } , 𝐵 } ) )