Theorem rng1nnzr

Description: The (smallest) structure representing a zero ring is not a nonzero ring. (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Hypothesis	rng1nnzr.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}$$
Assertion	rng1nnzr	$$⊢Z\in V\to M\notin \mathrm{NzRing}$$

Proof

Step	Hyp	Ref	Expression
1		rng1nnzr.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}$$
2		snex	$$⊢\left\{Z\right\}\in \mathrm{V}$$
3	1	rngbase	$$⊢\left\{Z\right\}\in \mathrm{V}\to \left\{Z\right\}={\mathrm{Base}}_M$$
4	2 3	mp1i	$$⊢Z\in V\to \left\{Z\right\}={\mathrm{Base}}_M$$
5	4	eqcomd	$$⊢Z\in V\to {\mathrm{Base}}_M=\left\{Z\right\}$$
6	5	fveq2d	$$⊢Z\in V\to \left|{\mathrm{Base}}_M\right|=\left|\left\{Z\right\}\right|$$
7		hashsng	$$⊢Z\in V\to \left|\left\{Z\right\}\right|=1$$
8	6 7	eqtrd	$$⊢Z\in V\to \left|{\mathrm{Base}}_M\right|=1$$
9	1	ring1	$$⊢Z\in V\to M\in \mathrm{Ring}$$
10		0ringnnzr	$$⊢M\in \mathrm{Ring}\to \left(\left|{\mathrm{Base}}_M\right|=1\leftrightarrow \neg M\in \mathrm{NzRing}\right)$$
11	9 10	syl	$$⊢Z\in V\to \left(\left|{\mathrm{Base}}_M\right|=1\leftrightarrow \neg M\in \mathrm{NzRing}\right)$$
12	8 11	mpbid	$$⊢Z\in V\to \neg M\in \mathrm{NzRing}$$
13		df-nel	$$⊢M\notin \mathrm{NzRing}\leftrightarrow \neg M\in \mathrm{NzRing}$$
14	12 13	sylibr	$$⊢Z\in V\to M\notin \mathrm{NzRing}$$