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

Metamath Proof Explorer

Theorem isdomn2

Description: A ring is a domain iff all nonzero elements are regular elements. (Contributed by Mario Carneiro, 28-Mar-2015) (Proof shortened by SN, 21-Jun-2025)

		Ref	Expression
	Hypotheses	isdomn2.b	$⊢ B = {Base}_{R}$
		isdomn2.t	$⊢ E = RLReg (R)$
		isdomn2.z	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	isdomn2	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land B ∖ \{\underset{˙}{0}\} \subseteq E)$

Proof

Step	Hyp	Ref	Expression
1		isdomn2.b	$⊢ B = {Base}_{R}$
2		isdomn2.t	$⊢ E = RLReg (R)$
3		isdomn2.z	$⊢ \underset{˙}{0} = 0_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5	1 4 3	isdomn	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})))$
6		eldifi	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to x \in B$
7	2 1 4 3	isrrg	$⊢ x \in E \leftrightarrow (x \in B \land \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to y = \underset{˙}{0}))$
8	7	baib	$⊢ x \in B \to (x \in E \leftrightarrow \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to y = \underset{˙}{0}))$
9	6 8	syl	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to (x \in E \leftrightarrow \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to y = \underset{˙}{0}))$
10	9	ralbiia	$⊢ \forall x \in (B ∖ \{\underset{˙}{0}\}) x \in E \leftrightarrow \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to y = \underset{˙}{0})$
11		dfss3	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq E \leftrightarrow \forall x \in (B ∖ \{\underset{˙}{0}\}) x \in E$
12		isdomn5	$⊢ \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})) \leftrightarrow \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to y = \underset{˙}{0})$
13	10 11 12	3bitr4ri	$⊢ \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})) \leftrightarrow B ∖ \{\underset{˙}{0}\} \subseteq E$
14	13	anbi2i	$⊢ (R \in NzRing \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))) \leftrightarrow (R \in NzRing \land B ∖ \{\underset{˙}{0}\} \subseteq E)$
15	5 14	bitri	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land B ∖ \{\underset{˙}{0}\} \subseteq E)$