ringelnzr

Description: A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by Mario Carneiro, 13-Jun-2015)

	Ref	Expression
Hypotheses	ringelnzr.z	$⊢ \underset{˙}{0} = 0_{R}$
	ringelnzr.b	$⊢ B = {Base}_{R}$
Assertion	ringelnzr	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to R \in NzRing$

Step	Hyp	Ref	Expression
1		ringelnzr.z	$⊢ \underset{˙}{0} = 0_{R}$
2		ringelnzr.b	$⊢ B = {Base}_{R}$
3		simpl	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to R \in Ring$
4		eldifsni	$⊢ X \in (B ∖ \{\underset{˙}{0}\}) \to X \neq \underset{˙}{0}$
5	4	adantl	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to X \neq \underset{˙}{0}$
6		eldifi	$⊢ X \in (B ∖ \{\underset{˙}{0}\}) \to X \in B$
7	6	adantl	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to X \in B$
8	2 1	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
9	8	adantr	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to \underset{˙}{0} \in B$
10		eqid	$⊢ 1_{R} = 1_{R}$
11	2 10 1	ring1eq0	$⊢ (R \in Ring \land X \in B \land \underset{˙}{0} \in B) \to (1_{R} = \underset{˙}{0} \to X = \underset{˙}{0})$
12	3 7 9 11	syl3anc	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to (1_{R} = \underset{˙}{0} \to X = \underset{˙}{0})$
13	12	necon3d	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to (X \neq \underset{˙}{0} \to 1_{R} \neq \underset{˙}{0})$
14	5 13	mpd	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to 1_{R} \neq \underset{˙}{0}$
15	10 1	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq \underset{˙}{0})$
16	3 14 15	sylanbrc	$⊢ (R \in Ring \land X \in (B ∖ \{\underset{˙}{0}\})) \to R \in NzRing$

Metamath Proof Explorer