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		simpl	|- ( ( M e. DivRing /\ M e. CRing ) -> M e. DivRing )
9	8	a1i	|- ( Z e. V -> ( ( M e. DivRing /\ M e. CRing ) -> M e. DivRing ) )
10	7 9	syl5bi	|- ( Z e. V -> ( M e. Field -> M e. DivRing ) )
11	6 10	mtod	|- ( Z e. V -> -. M e. Field )
12		df-nel	|- ( M e/ Field <-> -. M e. Field )
13	11 12	sylibr	|- ( Z e. V -> M e/ Field )