Metamath Proof Explorer

Theorem domneq0

Description: In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015)

Ref Expression
Hypotheses domneq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
domneq0.t ⊢ · = ( .r ‘ 𝑅 )
domneq0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion domneq0 ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 domneq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 domneq0.t ⊢ · = ( .r ‘ 𝑅 )
3 domneq0.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 3simpc ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
5 1 2 3 isdomn ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
6 5 simprbi ⊢ ( 𝑅 ∈ Domn → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
7 6 3ad2ant1 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
8 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑦 ) )
9 8 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 · 𝑦 ) = 0 ↔ ( 𝑋 · 𝑦 ) = 0 ) )
10 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 0 ↔ 𝑋 = 0 ) )
11 10 orbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) ↔ ( 𝑋 = 0 ∨ 𝑦 = 0 ) ) )
12 9 11 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ↔ ( ( 𝑋 · 𝑦 ) = 0 → ( 𝑋 = 0 ∨ 𝑦 = 0 ) ) ) )
13 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
14 13 eqeq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 · 𝑦 ) = 0 ↔ ( 𝑋 · 𝑌 ) = 0 ) )
15 eqeq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 = 0 ↔ 𝑌 = 0 ) )
16 15 orbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 = 0 ∨ 𝑦 = 0 ) ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
17 14 16 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 · 𝑦 ) = 0 → ( 𝑋 = 0 ∨ 𝑦 = 0 ) ) ↔ ( ( 𝑋 · 𝑌 ) = 0 → ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) ) )
18 12 17 rspc2va ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) → ( ( 𝑋 · 𝑌 ) = 0 → ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
19 4 7 18 syl2anc ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 → ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
20 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
21 20 3ad2ant1 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Ring )
22 simp3 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
23 1 2 3 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 0 · 𝑌 ) = 0 )
24 21 22 23 syl2anc ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 0 · 𝑌 ) = 0 )
25 oveq1 ⊢ ( 𝑋 = 0 → ( 𝑋 · 𝑌 ) = ( 0 · 𝑌 ) )
26 25 eqeq1d ⊢ ( 𝑋 = 0 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 0 · 𝑌 ) = 0 ) )
27 24 26 syl5ibrcom ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 0 → ( 𝑋 · 𝑌 ) = 0 ) )
28 simp2 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
29 1 2 3 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 0 ) = 0 )
30 21 28 29 syl2anc ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 0 ) = 0 )
31 oveq2 ⊢ ( 𝑌 = 0 → ( 𝑋 · 𝑌 ) = ( 𝑋 · 0 ) )
32 31 eqeq1d ⊢ ( 𝑌 = 0 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 · 0 ) = 0 ) )
33 30 32 syl5ibrcom ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 = 0 → ( 𝑋 · 𝑌 ) = 0 ) )
34 27 33 jaod ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 = 0 ∨ 𝑌 = 0 ) → ( 𝑋 · 𝑌 ) = 0 ) )
35 19 34 impbid ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )