Theorem domnmuln0

Description: In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		domneq0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		domneq0.t	⊢ · = ( .r ‘ 𝑅 )
3		domneq0.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		an4	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) )
5		neanior	⊢ ( ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) )
6	1 2 3	domneq0	⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
7	6	3expb	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
8	7	necon3abid	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
9	5 8	bitr4id	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ↔ ( 𝑋 · 𝑌 ) ≠ 0 ) )
10	9	biimpd	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) → ( 𝑋 · 𝑌 ) ≠ 0 ) )
11	10	expimpd	⊢ ( 𝑅 ∈ Domn → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 ) )
12	4 11	syl5bi	⊢ ( 𝑅 ∈ Domn → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 ) )
13	12	3impib	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 )