Theorem rng1nfld

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

	Ref	Expression
Hypothesis	rng1nfld.m	|- M = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
Assertion	rng1nfld	|- ( Z e. V -> M e/ Field )

Proof

Step	Hyp	Ref	Expression
1		rng1nfld.m	|- M = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
2	1	rng1nnzr	|- ( Z e. V -> M e/ NzRing )
3		df-nel	|- ( M e/ NzRing <-> -. M e. NzRing )
4	2 3	sylib	|- ( Z e. V -> -. M e. NzRing )
5		drngnzr	|- ( M e. DivRing -> M e. NzRing )
6	4 5	nsyl	|- ( Z e. V -> -. M e. DivRing )
7		isfld	|- ( M e. Field <-> ( M e. DivRing /\ M e. CRing ) )
8	7	simplbi	|- ( M e. Field -> M e. DivRing )
9	6 8	nsyl	|- ( Z e. V -> -. M e. Field )
10		df-nel	|- ( M e/ Field <-> -. M e. Field )
11	9 10	sylibr	|- ( Z e. V -> M e/ Field )