Metamath Proof Explorer

Theorem idomnzd

Description: A domain has no zero-divisors (besides zero). (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 ‘ 𝑅 )
Assertion idomnzd ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 · 𝑌 ) = 0 ) ) → ( 𝑋 = 0 ∨ 𝑌 = 0 ) )

Proof

Step Hyp Ref Expression
1 isidom3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isidom3.t ⊢ · = ( .r ‘ 𝑅 )
3 isidom3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
5 1 2 3 4 isidom3 ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 0 ≠ ( 1r ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
6 5 simp3bi ⊢ ( 𝑅 ∈ IDomn → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) )
7 oveq1 ⊢ ( 𝑎 = 𝑋 → ( 𝑎 · 𝑏 ) = ( 𝑋 · 𝑏 ) )
8 7 eqeq1d ⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 · 𝑏 ) = 0 ↔ ( 𝑋 · 𝑏 ) = 0 ) )
9 eqeq1 ⊢ ( 𝑎 = 𝑋 → ( 𝑎 = 0 ↔ 𝑋 = 0 ) )
10 9 orbi1d ⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 = 0 ∨ 𝑏 = 0 ) ↔ ( 𝑋 = 0 ∨ 𝑏 = 0 ) ) )
11 8 10 imbi12d ⊢ ( 𝑎 = 𝑋 → ( ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ↔ ( ( 𝑋 · 𝑏 ) = 0 → ( 𝑋 = 0 ∨ 𝑏 = 0 ) ) ) )
12 oveq2 ⊢ ( 𝑏 = 𝑌 → ( 𝑋 · 𝑏 ) = ( 𝑋 · 𝑌 ) )
13 12 eqeq1d ⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 · 𝑏 ) = 0 ↔ ( 𝑋 · 𝑌 ) = 0 ) )
14 eqeq1 ⊢ ( 𝑏 = 𝑌 → ( 𝑏 = 0 ↔ 𝑌 = 0 ) )
15 14 orbi2d ⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 = 0 ∨ 𝑏 = 0 ) ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
16 13 15 imbi12d ⊢ ( 𝑏 = 𝑌 → ( ( ( 𝑋 · 𝑏 ) = 0 → ( 𝑋 = 0 ∨ 𝑏 = 0 ) ) ↔ ( ( 𝑋 · 𝑌 ) = 0 → ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) ) )
17 11 16 rspc2v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) → ( ( 𝑋 · 𝑌 ) = 0 → ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) ) )
18 6 17 syl5com ⊢ ( 𝑅 ∈ IDomn → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 → ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) ) )
19 18 expd ⊢ ( 𝑅 ∈ IDomn → ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 → ( ( 𝑋 · 𝑌 ) = 0 → ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) ) ) )
20 19 3imp2 ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 · 𝑌 ) = 0 ) ) → ( 𝑋 = 0 ∨ 𝑌 = 0 ) )