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

Metamath Proof Explorer

Theorem isdomn6

Description: A ring is a domain iff the regular elements are the nonzero elements. Compare isdomn2 , domnrrg . (Contributed by Thierry Arnoux, 6-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		isdomn6.b	$⊢ B = {Base}_{R}$
2		isdomn6.t	$⊢ E = RLReg (R)$
3		isdomn6.z	$⊢ \underset{˙}{0} = 0_{R}$
4	1 2 3	isdomn2	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land B ∖ \{\underset{˙}{0}\} \subseteq E)$
5	2 1	rrgss	$⊢ E \subseteq B$
6	5	a1i	$⊢ R \in NzRing \to E \subseteq B$
7	2 3	rrgnz	$⊢ R \in NzRing \to \neg \underset{˙}{0} \in E$
8		ssdifsn	$⊢ E \subseteq B ∖ \{\underset{˙}{0}\} \leftrightarrow (E \subseteq B \land \neg \underset{˙}{0} \in E)$
9	6 7 8	sylanbrc	$⊢ R \in NzRing \to E \subseteq B ∖ \{\underset{˙}{0}\}$
10		sssseq	$⊢ E \subseteq B ∖ \{\underset{˙}{0}\} \to (B ∖ \{\underset{˙}{0}\} \subseteq E \leftrightarrow B ∖ \{\underset{˙}{0}\} = E)$
11	9 10	syl	$⊢ R \in NzRing \to (B ∖ \{\underset{˙}{0}\} \subseteq E \leftrightarrow B ∖ \{\underset{˙}{0}\} = E)$
12	11	pm5.32i	$⊢ (R \in NzRing \land B ∖ \{\underset{˙}{0}\} \subseteq E) \leftrightarrow (R \in NzRing \land B ∖ \{\underset{˙}{0}\} = E)$
13	4 12	bitri	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land B ∖ \{\underset{˙}{0}\} = E)$