This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ B = {Base}_{R}$
		domneq0.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		domneq0.z	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	domnmuln0	$⊢ (R \in Domn \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		domneq0.b	$⊢ B = {Base}_{R}$
2		domneq0.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		domneq0.z	$⊢ \underset{˙}{0} = 0_{R}$
4		an4	$⊢ ((X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \leftrightarrow ((X \in B \land Y \in B) \land (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0}))$
5		neanior	$⊢ (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0}) \leftrightarrow \neg (X = \underset{˙}{0} \lor Y = \underset{˙}{0})$
6	1 2 3	domneq0	$⊢ (R \in Domn \land X \in B \land Y \in B) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
7	6	3expb	$⊢ (R \in Domn \land (X \in B \land Y \in B)) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
8	7	necon3abid	$⊢ (R \in Domn \land (X \in B \land Y \in B)) \to (X \underset{˙}{\cdot} Y \neq \underset{˙}{0} \leftrightarrow \neg (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
9	5 8	bitr4id	$⊢ (R \in Domn \land (X \in B \land Y \in B)) \to ((X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0}) \leftrightarrow X \underset{˙}{\cdot} Y \neq \underset{˙}{0})$
10	9	biimpd	$⊢ (R \in Domn \land (X \in B \land Y \in B)) \to ((X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0}) \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0})$
11	10	expimpd	$⊢ R \in Domn \to (((X \in B \land Y \in B) \land (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0})) \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0})$
12	4 11	biimtrid	$⊢ R \in Domn \to (((X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0})$
13	12	3impib	$⊢ (R \in Domn \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0}$