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 = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
Assertion	rng1nnzr	|- ( Z e. V -> M e/ NzRing )

Proof

Step	Hyp	Ref	Expression
1		rng1nnzr.m	|- M = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
2		snex	|- { Z } e. _V
3	1	rngbase	|- ( { Z } e. _V -> { Z } = ( Base ` M ) )
4	2 3	mp1i	|- ( Z e. V -> { Z } = ( Base ` M ) )
5	4	eqcomd	|- ( Z e. V -> ( Base ` M ) = { Z } )
6	5	fveq2d	|- ( Z e. V -> ( # ` ( Base ` M ) ) = ( # ` { Z } ) )
7		hashsng	|- ( Z e. V -> ( # ` { Z } ) = 1 )
8	6 7	eqtrd	|- ( Z e. V -> ( # ` ( Base ` M ) ) = 1 )
9	1	ring1	|- ( Z e. V -> M e. Ring )
10		0ringnnzr	|- ( M e. Ring -> ( ( # ` ( Base ` M ) ) = 1 <-> -. M e. NzRing ) )
11	9 10	syl	|- ( Z e. V -> ( ( # ` ( Base ` M ) ) = 1 <-> -. M e. NzRing ) )
12	8 11	mpbid	|- ( Z e. V -> -. M e. NzRing )
13		df-nel	|- ( M e/ NzRing <-> -. M e. NzRing )
14	12 13	sylibr	|- ( Z e. V -> M e/ NzRing )