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 ) ) )