Metamath Proof Explorer

Theorem prmringnzring

Description: A prime ring is a nonzero ring. (Contributed by AV, 26-Jun-2026)

		Ref	Expression
	Assertion	prmringnzring	Could not format assertion : No typesetting found for \|- ( R e. PrmRing -> R e. NzRing ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ 0_{R} = 0_{R}$
2		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
3	1 2	isprmrng	Could not format ( R e. PrmRing <-> ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) ) : No typesetting found for \|- ( R e. PrmRing <-> ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) ) with typecode \|-
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4	0ringprmidl	$⊢ (R \in Ring \land \|{Base}_{R}\| = 1) \to PrmIdeal (R) = \emptyset$
6		eleq2	$⊢ PrmIdeal (R) = \emptyset \to (\{0_{R}\} \in PrmIdeal (R) \leftrightarrow \{0_{R}\} \in \emptyset)$
7		noel	$⊢ \neg \{0_{R}\} \in \emptyset$
8	7	pm2.21i	$⊢ \{0_{R}\} \in \emptyset \to R \in NzRing$
9	6 8	biimtrdi	$⊢ PrmIdeal (R) = \emptyset \to (\{0_{R}\} \in PrmIdeal (R) \to R \in NzRing)$
10	5 9	syl	$⊢ (R \in Ring \land \|{Base}_{R}\| = 1) \to (\{0_{R}\} \in PrmIdeal (R) \to R \in NzRing)$
11	10	ex	$⊢ R \in Ring \to (\|{Base}_{R}\| = 1 \to (\{0_{R}\} \in PrmIdeal (R) \to R \in NzRing))$
12		0ringnnzr	$⊢ R \in Ring \to (\|{Base}_{R}\| = 1 \leftrightarrow \neg R \in NzRing)$
13	12	bicomd	$⊢ R \in Ring \to (\neg R \in NzRing \leftrightarrow \|{Base}_{R}\| = 1)$
14	13	con1bid	$⊢ R \in Ring \to (\neg \|{Base}_{R}\| = 1 \leftrightarrow R \in NzRing)$
15		ax1w	$⊢ R \in Ring \to (R \in NzRing \to (\{0_{R}\} \in PrmIdeal (R) \to R \in NzRing))$
16	14 15	sylbid	$⊢ R \in Ring \to (\neg \|{Base}_{R}\| = 1 \to (\{0_{R}\} \in PrmIdeal (R) \to R \in NzRing))$
17	11 16	pm2.61d	$⊢ R \in Ring \to (\{0_{R}\} \in PrmIdeal (R) \to R \in NzRing)$
18	17	imp	$⊢ (R \in Ring \land \{0_{R}\} \in PrmIdeal (R)) \to R \in NzRing$
19	3 18	sylbi	Could not format ( R e. PrmRing -> R e. NzRing ) : No typesetting found for \|- ( R e. PrmRing -> R e. NzRing ) with typecode \|-