Metamath Proof Explorer

Theorem isfieldidl

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

Ref Expression
Hypotheses isfieldidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isfieldidl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
isfieldidl.i ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
isfieldidl.1 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion isfieldidl ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 isfieldidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isfieldidl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 isfieldidl.i ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
4 isfieldidl.1 ⊢ 1 = ( 1r ‘ 𝑅 )
5 isfld ⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) )
6 1 2 3 drngidl ⊢ ( 𝑅 ∈ NzRing → ( 𝑅 ∈ DivRing ↔ 𝐼 = { { 0 } , 𝐵 } ) )
7 6 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑅 ∈ CRing ) → ( 𝑅 ∈ DivRing ↔ 𝐼 = { { 0 } , 𝐵 } ) )
8 4 2 nzrnz ⊢ ( 𝑅 ∈ NzRing → 1 ≠ 0 )
9 8 necomd ⊢ ( 𝑅 ∈ NzRing → 0 ≠ 1 )
10 9 a1d ⊢ ( 𝑅 ∈ NzRing → ( 𝐼 = { { 0 } , 𝐵 } → 0 ≠ 1 ) )
11 10 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑅 ∈ CRing ) → ( 𝐼 = { { 0 } , 𝐵 } → 0 ≠ 1 ) )
12 11 pm4.71rd ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑅 ∈ CRing ) → ( 𝐼 = { { 0 } , 𝐵 } ↔ ( 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
13 7 12 bitrd ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑅 ∈ CRing ) → ( 𝑅 ∈ DivRing ↔ ( 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
14 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
15 14 con3i ⊢ ( ¬ 𝑅 ∈ NzRing → ¬ 𝑅 ∈ DivRing )
16 15 adantr ⊢ ( ( ¬ 𝑅 ∈ NzRing ∧ 𝑅 ∈ CRing ) → ¬ 𝑅 ∈ DivRing )
17 ianor ⊢ ( ¬ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ↔ ( ¬ 𝑅 ∈ Ring ∨ ¬ 1 ≠ 0 ) )
18 4 2 isnzr ⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) )
19 17 18 xchnxbir ⊢ ( ¬ 𝑅 ∈ NzRing ↔ ( ¬ 𝑅 ∈ Ring ∨ ¬ 1 ≠ 0 ) )
20 pm2.24 ⊢ ( 𝑅 ∈ Ring → ( ¬ 𝑅 ∈ Ring → ( ¬ 0 ≠ 1 ∨ ¬ 𝐼 = { { 0 } , 𝐵 } ) ) )
21 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
22 20 21 syl11 ⊢ ( ¬ 𝑅 ∈ Ring → ( 𝑅 ∈ CRing → ( ¬ 0 ≠ 1 ∨ ¬ 𝐼 = { { 0 } , 𝐵 } ) ) )
23 id ⊢ ( 0 ≠ 1 → 0 ≠ 1 )
24 23 necomd ⊢ ( 0 ≠ 1 → 1 ≠ 0 )
25 24 con3i ⊢ ( ¬ 1 ≠ 0 → ¬ 0 ≠ 1 )
26 25 orcd ⊢ ( ¬ 1 ≠ 0 → ( ¬ 0 ≠ 1 ∨ ¬ 𝐼 = { { 0 } , 𝐵 } ) )
27 26 a1d ⊢ ( ¬ 1 ≠ 0 → ( 𝑅 ∈ CRing → ( ¬ 0 ≠ 1 ∨ ¬ 𝐼 = { { 0 } , 𝐵 } ) ) )
28 22 27 jaoi ⊢ ( ( ¬ 𝑅 ∈ Ring ∨ ¬ 1 ≠ 0 ) → ( 𝑅 ∈ CRing → ( ¬ 0 ≠ 1 ∨ ¬ 𝐼 = { { 0 } , 𝐵 } ) ) )
29 19 28 sylbi ⊢ ( ¬ 𝑅 ∈ NzRing → ( 𝑅 ∈ CRing → ( ¬ 0 ≠ 1 ∨ ¬ 𝐼 = { { 0 } , 𝐵 } ) ) )
30 29 imp ⊢ ( ( ¬ 𝑅 ∈ NzRing ∧ 𝑅 ∈ CRing ) → ( ¬ 0 ≠ 1 ∨ ¬ 𝐼 = { { 0 } , 𝐵 } ) )
31 ianor ⊢ ( ¬ ( 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) ↔ ( ¬ 0 ≠ 1 ∨ ¬ 𝐼 = { { 0 } , 𝐵 } ) )
32 30 31 sylibr ⊢ ( ( ¬ 𝑅 ∈ NzRing ∧ 𝑅 ∈ CRing ) → ¬ ( 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) )
33 16 32 2falsed ⊢ ( ( ¬ 𝑅 ∈ NzRing ∧ 𝑅 ∈ CRing ) → ( 𝑅 ∈ DivRing ↔ ( 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
34 13 33 pm2.61ian ⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ DivRing ↔ ( 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
35 34 pm5.32i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ DivRing ) ↔ ( 𝑅 ∈ CRing ∧ ( 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
36 ancom ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ DivRing ) )
37 3anass ⊢ ( ( 𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) ↔ ( 𝑅 ∈ CRing ∧ ( 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) ) )
38 35 36 37 3bitr4i ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) ↔ ( 𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) )
39 5 38 bitri ⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ 𝐼 = { { 0 } , 𝐵 } ) )