Theorem rng1nfld

Description: The zero ring is not a field. (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Hypothesis	rng1nfld.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	rng1nfld	$$⊢Z\in V\to M\notin \mathrm{Field}$$

Proof

Step	Hyp	Ref	Expression
1		rng1nfld.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	1	rng1nnzr	$$⊢Z\in V\to M\notin \mathrm{NzRing}$$
3		df-nel	$$⊢M\notin \mathrm{NzRing}\leftrightarrow \neg M\in \mathrm{NzRing}$$
4	2 3	sylib	$$⊢Z\in V\to \neg M\in \mathrm{NzRing}$$
5		drngnzr	$$⊢M\in \mathrm{DivRing}\to M\in \mathrm{NzRing}$$
6	4 5	nsyl	$$⊢Z\in V\to \neg M\in \mathrm{DivRing}$$
7		isfld	$$⊢M\in \mathrm{Field}\leftrightarrow \left(M\in \mathrm{DivRing}\wedge M\in \mathrm{CRing}\right)$$
8	7	simplbi	$$⊢M\in \mathrm{Field}\to M\in \mathrm{DivRing}$$
9	6 8	nsyl	$$⊢Z\in V\to \neg M\in \mathrm{Field}$$
10		df-nel	$$⊢M\notin \mathrm{Field}\leftrightarrow \neg M\in \mathrm{Field}$$
11	9 10	sylibr	$$⊢Z\in V\to M\notin \mathrm{Field}$$