Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
isidom3.t ⊢ · = ( .r ‘ 𝑅 )
isidom3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
isidom3.1 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion isidom3 ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 isidom3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isidom3.t ⊢ · = ( .r ‘ 𝑅 )
3 isidom3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 isidom3.1 ⊢ 1 = ( 1r ‘ 𝑅 )
5 isidom2 ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ PrmRing ∧ 𝑅 ∈ CRing ) )
6 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
7 3 6 isprmrng ⊢ ( 𝑅 ∈ PrmRing ↔ ( 𝑅 ∈ Ring ∧ { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ) )
8 1 2 isprmidlc ⊢ ( 𝑅 ∈ CRing → ( { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ) ) )
9 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10 9 biantrurd ⊢ ( 𝑅 ∈ CRing → ( { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑅 ∈ Ring ∧ { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ) ) )
11 3anass ⊢ ( ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ) ↔ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ ( { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ) ) )
12 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
13 12 3 2idl0 ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( 2Ideal ‘ 𝑅 ) )
14 9 13 syl ⊢ ( 𝑅 ∈ CRing → { 0 } ∈ ( 2Ideal ‘ 𝑅 ) )
15 14 2idllidld ⊢ ( 𝑅 ∈ CRing → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
16 15 biantrurd ⊢ ( 𝑅 ∈ CRing → ( ( { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ) ↔ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ ( { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ) ) ) )
17 1 4 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
18 eleq2 ⊢ ( { 0 } = 𝐵 → ( 1 ∈ { 0 } ↔ 1 ∈ 𝐵 ) )
19 elsni ⊢ ( 1 ∈ { 0 } → 1 = 0 )
20 19 eqcomd ⊢ ( 1 ∈ { 0 } → 0 = 1 )
21 18 20 biimtrrdi ⊢ ( { 0 } = 𝐵 → ( 1 ∈ 𝐵 → 0 = 1 ) )
22 17 21 syl5com ⊢ ( 𝑅 ∈ Ring → ( { 0 } = 𝐵 → 0 = 1 ) )
23 1 3 4 0ring01eqbi ⊢ ( 𝑅 ∈ Ring → ( 𝐵 ≈ 1o ↔ 1 = 0 ) )
24 eqcom ⊢ ( 1 = 0 ↔ 0 = 1 )
25 23 24 bitrdi ⊢ ( 𝑅 ∈ Ring → ( 𝐵 ≈ 1o ↔ 0 = 1 ) )
26 1 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
27 en1eqsn ⊢ ( ( 0 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 0 } )
28 27 eqcomd ⊢ ( ( 0 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → { 0 } = 𝐵 )
29 28 ex ⊢ ( 0 ∈ 𝐵 → ( 𝐵 ≈ 1o → { 0 } = 𝐵 ) )
30 26 29 syl ⊢ ( 𝑅 ∈ Ring → ( 𝐵 ≈ 1o → { 0 } = 𝐵 ) )
31 25 30 sylbird ⊢ ( 𝑅 ∈ Ring → ( 0 = 1 → { 0 } = 𝐵 ) )
32 22 31 impbid ⊢ ( 𝑅 ∈ Ring → ( { 0 } = 𝐵 ↔ 0 = 1 ) )
33 9 32 syl ⊢ ( 𝑅 ∈ CRing → ( { 0 } = 𝐵 ↔ 0 = 1 ) )
34 33 necon3bid ⊢ ( 𝑅 ∈ CRing → ( { 0 } ≠ 𝐵 ↔ 0 ≠ 1 ) )
35 ovex ⊢ ( 𝑎 · 𝑏 ) ∈ V
36 35 elsn ⊢ ( ( 𝑎 · 𝑏 ) ∈ { 0 } ↔ ( 𝑎 · 𝑏 ) = 0 )
37 velsn ⊢ ( 𝑎 ∈ { 0 } ↔ 𝑎 = 0 )
38 velsn ⊢ ( 𝑏 ∈ { 0 } ↔ 𝑏 = 0 )
39 37 38 orbi12i ⊢ ( ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ↔ ( 𝑎 = 0 ∨ 𝑏 = 0 ) )
40 36 39 imbi12i ⊢ ( ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ↔ ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) )
41 40 a1i ⊢ ( 𝑅 ∈ CRing → ( ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ↔ ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
42 41 2ralbidv ⊢ ( 𝑅 ∈ CRing → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
43 34 42 anbi12d ⊢ ( 𝑅 ∈ CRing → ( ( { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ) ↔ ( 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) ) )
44 16 43 bitr3d ⊢ ( 𝑅 ∈ CRing → ( ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ ( { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ) ) ↔ ( 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) ) )
45 11 44 bitrid ⊢ ( 𝑅 ∈ CRing → ( ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) ∈ { 0 } → ( 𝑎 ∈ { 0 } ∨ 𝑏 ∈ { 0 } ) ) ) ↔ ( 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) ) )
46 8 10 45 3bitr3d ⊢ ( 𝑅 ∈ CRing → ( ( 𝑅 ∈ Ring ∧ { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ) ↔ ( 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) ) )
47 7 46 bitrid ⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ PrmRing ↔ ( 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) ) )
48 47 pm5.32i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ PrmRing ) ↔ ( 𝑅 ∈ CRing ∧ ( 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) ) )
49 ancom ⊢ ( ( 𝑅 ∈ PrmRing ∧ 𝑅 ∈ CRing ) ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ PrmRing ) )
50 3anass ⊢ ( ( 𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) ↔ ( 𝑅 ∈ CRing ∧ ( 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) ) )
51 48 49 50 3bitr4i ⊢ ( ( 𝑅 ∈ PrmRing ∧ 𝑅 ∈ CRing ) ↔ ( 𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
52 5 51 bitri ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 0 ≠ 1 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )