rng1nfld

		Ref	Expression
	Hypothesis	rng1nfld.m	$⊢ M = \{⟨{Base}_{ndx}, \{Z\}⟩, ⟨+_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩\}$
	Assertion	rng1nfld	$⊢ Z \in V \to M \notin Field$

Step	Hyp	Ref	Expression
1		rng1nfld.m	$⊢ M = \{⟨{Base}_{ndx}, \{Z\}⟩, ⟨+_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩, ⟨\cdot_{ndx}, \{⟨⟨Z, Z⟩, Z⟩\}⟩\}$
2	1	rng1nnzr	$⊢ Z \in V \to M \notin NzRing$
3		df-nel	$⊢ M \notin NzRing \leftrightarrow \neg M \in NzRing$
4	2 3	sylib	$⊢ Z \in V \to \neg M \in NzRing$
5		drngnzr	$⊢ M \in DivRing \to M \in NzRing$
6	4 5	nsyl	$⊢ Z \in V \to \neg M \in DivRing$
7		isfld	$⊢ M \in Field \leftrightarrow (M \in DivRing \land M \in CRing)$
8	7	simplbi	$⊢ M \in Field \to M \in DivRing$
9	6 8	nsyl	$⊢ Z \in V \to \neg M \in Field$
10		df-nel	$⊢ M \notin Field \leftrightarrow \neg M \in Field$
11	9 10	sylibr	$⊢ Z \in V \to M \notin Field$

Metamath Proof Explorer