Metamath Proof Explorer

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 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion prmidl0 ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ) ↔ 𝑅 ∈ IDomn )

Proof

Step Hyp Ref Expression
1 prmidl0.1 ⊢ 0 = ( 0g ‘ 𝑅 )
2 df-3an ⊢ ( ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ) ↔ ( ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ) )
3 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
4 3 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑅 ∈ NzRing ) → 𝑅 ∈ Ring )
5 0ringnnzr ⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ ¬ 𝑅 ∈ NzRing ) )
6 5 biimpar ⊢ ( ( 𝑅 ∈ Ring ∧ ¬ 𝑅 ∈ NzRing ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 )
7 4 6 sylancom ⊢ ( ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑅 ∈ NzRing ) → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 8 1 0ring ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → ( Base ‘ 𝑅 ) = { 0 } )
10 4 7 9 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑅 ∈ NzRing ) → ( Base ‘ 𝑅 ) = { 0 } )
11 10 eqcomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑅 ∈ NzRing ) → { 0 } = ( Base ‘ 𝑅 ) )
12 11 ex ⊢ ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( LIdeal ‘ 𝑅 ) ) → ( ¬ 𝑅 ∈ NzRing → { 0 } = ( Base ‘ 𝑅 ) ) )
13 12 necon1ad ⊢ ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( LIdeal ‘ 𝑅 ) ) → ( { 0 } ≠ ( Base ‘ 𝑅 ) → 𝑅 ∈ NzRing ) )
14 13 impr ⊢ ( ( 𝑅 ∈ CRing ∧ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ NzRing )
15 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
16 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
17 16 1 lidl0 ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
18 15 17 syl ⊢ ( 𝑅 ∈ NzRing → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
19 1 fvexi ⊢ 0 ∈ V
20 hashsng ⊢ ( 0 ∈ V → ( ♯ ‘ { 0 } ) = 1 )
21 19 20 ax-mp ⊢ ( ♯ ‘ { 0 } ) = 1
22 1re ⊢ 1 ∈ ℝ
23 21 22 eqeltri ⊢ ( ♯ ‘ { 0 } ) ∈ ℝ
24 23 a1i ⊢ ( 𝑅 ∈ NzRing → ( ♯ ‘ { 0 } ) ∈ ℝ )
25 8 isnzr2hash ⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) )
26 25 simprbi ⊢ ( 𝑅 ∈ NzRing → 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
27 21 26 eqbrtrid ⊢ ( 𝑅 ∈ NzRing → ( ♯ ‘ { 0 } ) < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
28 24 27 ltned ⊢ ( 𝑅 ∈ NzRing → ( ♯ ‘ { 0 } ) ≠ ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
29 fveq2 ⊢ ( { 0 } = ( Base ‘ 𝑅 ) → ( ♯ ‘ { 0 } ) = ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
30 29 necon3i ⊢ ( ( ♯ ‘ { 0 } ) ≠ ( ♯ ‘ ( Base ‘ 𝑅 ) ) → { 0 } ≠ ( Base ‘ 𝑅 ) )
31 28 30 syl ⊢ ( 𝑅 ∈ NzRing → { 0 } ≠ ( Base ‘ 𝑅 ) )
32 18 31 jca ⊢ ( 𝑅 ∈ NzRing → ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ) )
33 32 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ) → ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ) )
34 14 33 impbida ⊢ ( 𝑅 ∈ CRing → ( ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ) ↔ 𝑅 ∈ NzRing ) )
35 19 elsn2 ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 )
36 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
37 velsn ⊢ ( 𝑦 ∈ { 0 } ↔ 𝑦 = 0 )
38 36 37 orbi12i ⊢ ( ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ↔ ( 𝑥 = 0 ∨ 𝑦 = 0 ) )
39 35 38 imbi12i ⊢ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
40 39 2ralbii ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
41 40 a1i ⊢ ( 𝑅 ∈ CRing → ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
42 34 41 anbi12d ⊢ ( 𝑅 ∈ CRing → ( ( ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ) ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) )
43 2 42 syl5bb ⊢ ( 𝑅 ∈ CRing → ( ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ) ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) )
44 43 pm5.32i ⊢ ( ( 𝑅 ∈ CRing ∧ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ) ) ↔ ( 𝑅 ∈ CRing ∧ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) )
45 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
46 8 45 isprmidlc ⊢ ( 𝑅 ∈ CRing → ( { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ) ) )
47 46 pm5.32i ⊢ ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ CRing ∧ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑥 ∈ { 0 } ∨ 𝑦 ∈ { 0 } ) ) ) ) )
48 df-idom ⊢ IDomn = ( CRing ∩ Domn )
49 48 eleq2i ⊢ ( 𝑅 ∈ IDomn ↔ 𝑅 ∈ ( CRing ∩ Domn ) )
50 elin ⊢ ( 𝑅 ∈ ( CRing ∩ Domn ) ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
51 8 45 1 isdomn ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
52 51 anbi2i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) ↔ ( 𝑅 ∈ CRing ∧ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) )
53 49 50 52 3bitri ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) )
54 44 47 53 3bitr4i ⊢ ( ( 𝑅 ∈ CRing ∧ { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ) ↔ 𝑅 ∈ IDomn )