domnrrg

Description: In a domain, a nonzero element is a regular element. (Contributed by Mario Carneiro, 28-Mar-2015)

	Ref	Expression
Hypotheses	isdomn2.b	$⊢ B = {Base}_{R}$
	isdomn2.t	$⊢ E = RLReg (R)$
	isdomn2.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	domnrrg	$⊢ (R \in Domn \land X \in B \land X \neq \underset{˙}{0}) \to X \in E$

Step	Hyp	Ref	Expression
1		isdomn2.b	$⊢ B = {Base}_{R}$
2		isdomn2.t	$⊢ E = RLReg (R)$
3		isdomn2.z	$⊢ \underset{˙}{0} = 0_{R}$
4	1 2 3	isdomn2	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land B ∖ \{\underset{˙}{0}\} \subseteq E)$
5	4	simprbi	$⊢ R \in Domn \to B ∖ \{\underset{˙}{0}\} \subseteq E$
6	5	3ad2ant1	$⊢ (R \in Domn \land X \in B \land X \neq \underset{˙}{0}) \to B ∖ \{\underset{˙}{0}\} \subseteq E$
7		simp2	$⊢ (R \in Domn \land X \in B \land X \neq \underset{˙}{0}) \to X \in B$
8		simp3	$⊢ (R \in Domn \land X \in B \land X \neq \underset{˙}{0}) \to X \neq \underset{˙}{0}$
9		eldifsn	$⊢ X \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in B \land X \neq \underset{˙}{0})$
10	7 8 9	sylanbrc	$⊢ (R \in Domn \land X \in B \land X \neq \underset{˙}{0}) \to X \in (B ∖ \{\underset{˙}{0}\})$
11	6 10	sseldd	$⊢ (R \in Domn \land X \in B \land X \neq \underset{˙}{0}) \to X \in E$

Metamath Proof Explorer