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

Metamath Proof Explorer

Theorem drngmcl

Description: The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011) (Proof shortened by SN, 25-Jun-2025)

		Ref	Expression
	Hypotheses	drngmcl.b	$⊢ B = {Base}_{R}$
		drngmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		drngmcl.z	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	drngmcl	$⊢ (R \in DivRing \land X \in (B ∖ \{\underset{˙}{0}\}) \land Y \in (B ∖ \{\underset{˙}{0}\})) \to X \underset{˙}{\cdot} Y \in (B ∖ \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		drngmcl.b	$⊢ B = {Base}_{R}$
2		drngmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		drngmcl.z	$⊢ \underset{˙}{0} = 0_{R}$
4		drngring	$⊢ R \in DivRing \to R \in Ring$
5		eldifi	$⊢ X \in (B ∖ \{\underset{˙}{0}\}) \to X \in B$
6		eldifi	$⊢ Y \in (B ∖ \{\underset{˙}{0}\}) \to Y \in B$
7	1 2	ringcl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
8	4 5 6 7	syl3an	$⊢ (R \in DivRing \land X \in (B ∖ \{\underset{˙}{0}\}) \land Y \in (B ∖ \{\underset{˙}{0}\})) \to X \underset{˙}{\cdot} Y \in B$
9		drngdomn	$⊢ R \in DivRing \to R \in Domn$
10		eldifsn	$⊢ X \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in B \land X \neq \underset{˙}{0})$
11	10	biimpi	$⊢ X \in (B ∖ \{\underset{˙}{0}\}) \to (X \in B \land X \neq \underset{˙}{0})$
12		eldifsn	$⊢ Y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \in B \land Y \neq \underset{˙}{0})$
13	12	biimpi	$⊢ Y \in (B ∖ \{\underset{˙}{0}\}) \to (Y \in B \land Y \neq \underset{˙}{0})$
14	1 2 3	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}$
15	9 11 13 14	syl3an	$⊢ (R \in DivRing \land X \in (B ∖ \{\underset{˙}{0}\}) \land Y \in (B ∖ \{\underset{˙}{0}\})) \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0}$
16	8 15	eldifsnd	$⊢ (R \in DivRing \land X \in (B ∖ \{\underset{˙}{0}\}) \land Y \in (B ∖ \{\underset{˙}{0}\})) \to X \underset{˙}{\cdot} Y \in (B ∖ \{\underset{˙}{0}\})$