Theorem nzerooringczr

Description: There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in Adamek p. 103. (Contributed by AV, 18-Apr-2020)

	Ref	Expression
Hypotheses	nzerooringczr.u	|- ( ph -> U e. V )
	nzerooringczr.c	|- C = ( RingCat ` U )
	nzerooringczr.z	|- ( ph -> Z e. ( Ring \ NzRing ) )
	nzerooringczr.e	|- ( ph -> Z e. U )
	nzerooringczr.i	|- ( ph -> ZZring e. U )
Assertion	nzerooringczr	|- ( ph -> ( ZeroO ` C ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		nzerooringczr.u	|- ( ph -> U e. V )
2		nzerooringczr.c	|- C = ( RingCat ` U )
3		nzerooringczr.z	|- ( ph -> Z e. ( Ring \ NzRing ) )
4		nzerooringczr.e	|- ( ph -> Z e. U )
5		nzerooringczr.i	|- ( ph -> ZZring e. U )
6		ax-1	|- ( ( ZeroO ` C ) = (/) -> ( ph -> ( ZeroO ` C ) = (/) ) )
7		neq0	|- ( -. ( ZeroO ` C ) = (/) <-> E. h h e. ( ZeroO ` C ) )
8	2	ringccat	|- ( U e. V -> C e. Cat )
9	1 8	syl	|- ( ph -> C e. Cat )
10		iszeroi	|- ( ( C e. Cat /\ h e. ( ZeroO ` C ) ) -> ( h e. ( Base ` C ) /\ ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) ) )
11	9 10	sylan	|- ( ( ph /\ h e. ( ZeroO ` C ) ) -> ( h e. ( Base ` C ) /\ ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) ) )
12	1 2 3 4	zrtermoringc	|- ( ph -> Z e. ( TermO ` C ) )
13	1 5 2	irinitoringc	|- ( ph -> ZZring e. ( InitO ` C ) )
14	9	ad2antrr	|- ( ( ( ph /\ h e. ( InitO ` C ) ) /\ ZZring e. ( InitO ` C ) ) -> C e. Cat )
15		simplr	|- ( ( ( ph /\ h e. ( InitO ` C ) ) /\ ZZring e. ( InitO ` C ) ) -> h e. ( InitO ` C ) )
16		simpr	|- ( ( ( ph /\ h e. ( InitO ` C ) ) /\ ZZring e. ( InitO ` C ) ) -> ZZring e. ( InitO ` C ) )
17	14 15 16	initoeu1w	|- ( ( ( ph /\ h e. ( InitO ` C ) ) /\ ZZring e. ( InitO ` C ) ) -> h ( ~=c ` C ) ZZring )
18	9	ad2antrr	|- ( ( ( ph /\ h e. ( TermO ` C ) ) /\ Z e. ( TermO ` C ) ) -> C e. Cat )
19		simpr	|- ( ( ( ph /\ h e. ( TermO ` C ) ) /\ Z e. ( TermO ` C ) ) -> Z e. ( TermO ` C ) )
20		simplr	|- ( ( ( ph /\ h e. ( TermO ` C ) ) /\ Z e. ( TermO ` C ) ) -> h e. ( TermO ` C ) )
21	18 19 20	termoeu1w	|- ( ( ( ph /\ h e. ( TermO ` C ) ) /\ Z e. ( TermO ` C ) ) -> Z ( ~=c ` C ) h )
22		cictr	|- ( ( C e. Cat /\ Z ( ~=c ` C ) h /\ h ( ~=c ` C ) ZZring ) -> Z ( ~=c ` C ) ZZring )
23	9 22	syl3an1	|- ( ( ph /\ Z ( ~=c ` C ) h /\ h ( ~=c ` C ) ZZring ) -> Z ( ~=c ` C ) ZZring )
24		eqid	|- ( Iso ` C ) = ( Iso ` C )
25		eqid	|- ( Base ` C ) = ( Base ` C )
26	3	eldifad	|- ( ph -> Z e. Ring )
27	4 26	elind	|- ( ph -> Z e. ( U i^i Ring ) )
28	2 25 1	ringcbas	|- ( ph -> ( Base ` C ) = ( U i^i Ring ) )
29	27 28	eleqtrrd	|- ( ph -> Z e. ( Base ` C ) )
30		zringring	|- ZZring e. Ring
31	30	a1i	|- ( ph -> ZZring e. Ring )
32	5 31	elind	|- ( ph -> ZZring e. ( U i^i Ring ) )
33	32 28	eleqtrrd	|- ( ph -> ZZring e. ( Base ` C ) )
34	24 25 9 29 33	cic	|- ( ph -> ( Z ( ~=c ` C ) ZZring <-> E. f f e. ( Z ( Iso ` C ) ZZring ) ) )
35		n0	|- ( ( Z ( Iso ` C ) ZZring ) =/= (/) <-> E. f f e. ( Z ( Iso ` C ) ZZring ) )
36		eqid	|- ( Hom ` C ) = ( Hom ` C )
37	25 36 24 9 29 33	isohom	|- ( ph -> ( Z ( Iso ` C ) ZZring ) C_ ( Z ( Hom ` C ) ZZring ) )
38		ssn0	|- ( ( ( Z ( Iso ` C ) ZZring ) C_ ( Z ( Hom ` C ) ZZring ) /\ ( Z ( Iso ` C ) ZZring ) =/= (/) ) -> ( Z ( Hom ` C ) ZZring ) =/= (/) )
39	2 25 1 36 29 33	ringchom	|- ( ph -> ( Z ( Hom ` C ) ZZring ) = ( Z RingHom ZZring ) )
40	39	neeq1d	|- ( ph -> ( ( Z ( Hom ` C ) ZZring ) =/= (/) <-> ( Z RingHom ZZring ) =/= (/) ) )
41		zringnzr	|- ZZring e. NzRing
42		nrhmzr	|- ( ( Z e. ( Ring \ NzRing ) /\ ZZring e. NzRing ) -> ( Z RingHom ZZring ) = (/) )
43	3 41 42	sylancl	|- ( ph -> ( Z RingHom ZZring ) = (/) )
44		eqneqall	|- ( ( Z RingHom ZZring ) = (/) -> ( ( Z RingHom ZZring ) =/= (/) -> ( ZeroO ` C ) = (/) ) )
45	43 44	syl	|- ( ph -> ( ( Z RingHom ZZring ) =/= (/) -> ( ZeroO ` C ) = (/) ) )
46	40 45	sylbid	|- ( ph -> ( ( Z ( Hom ` C ) ZZring ) =/= (/) -> ( ZeroO ` C ) = (/) ) )
47	38 46	syl5com	|- ( ( ( Z ( Iso ` C ) ZZring ) C_ ( Z ( Hom ` C ) ZZring ) /\ ( Z ( Iso ` C ) ZZring ) =/= (/) ) -> ( ph -> ( ZeroO ` C ) = (/) ) )
48	47	expcom	|- ( ( Z ( Iso ` C ) ZZring ) =/= (/) -> ( ( Z ( Iso ` C ) ZZring ) C_ ( Z ( Hom ` C ) ZZring ) -> ( ph -> ( ZeroO ` C ) = (/) ) ) )
49	48	com13	|- ( ph -> ( ( Z ( Iso ` C ) ZZring ) C_ ( Z ( Hom ` C ) ZZring ) -> ( ( Z ( Iso ` C ) ZZring ) =/= (/) -> ( ZeroO ` C ) = (/) ) ) )
50	37 49	mpd	|- ( ph -> ( ( Z ( Iso ` C ) ZZring ) =/= (/) -> ( ZeroO ` C ) = (/) ) )
51	35 50	syl5bir	|- ( ph -> ( E. f f e. ( Z ( Iso ` C ) ZZring ) -> ( ZeroO ` C ) = (/) ) )
52	34 51	sylbid	|- ( ph -> ( Z ( ~=c ` C ) ZZring -> ( ZeroO ` C ) = (/) ) )
53	52	3ad2ant1	|- ( ( ph /\ Z ( ~=c ` C ) h /\ h ( ~=c ` C ) ZZring ) -> ( Z ( ~=c ` C ) ZZring -> ( ZeroO ` C ) = (/) ) )
54	23 53	mpd	|- ( ( ph /\ Z ( ~=c ` C ) h /\ h ( ~=c ` C ) ZZring ) -> ( ZeroO ` C ) = (/) )
55	54	3exp	|- ( ph -> ( Z ( ~=c ` C ) h -> ( h ( ~=c ` C ) ZZring -> ( ZeroO ` C ) = (/) ) ) )
56	55	a1dd	|- ( ph -> ( Z ( ~=c ` C ) h -> ( h e. ( Base ` C ) -> ( h ( ~=c ` C ) ZZring -> ( ZeroO ` C ) = (/) ) ) ) )
57	56	ad2antrr	|- ( ( ( ph /\ h e. ( TermO ` C ) ) /\ Z e. ( TermO ` C ) ) -> ( Z ( ~=c ` C ) h -> ( h e. ( Base ` C ) -> ( h ( ~=c ` C ) ZZring -> ( ZeroO ` C ) = (/) ) ) ) )
58	21 57	mpd	|- ( ( ( ph /\ h e. ( TermO ` C ) ) /\ Z e. ( TermO ` C ) ) -> ( h e. ( Base ` C ) -> ( h ( ~=c ` C ) ZZring -> ( ZeroO ` C ) = (/) ) ) )
59	58	exp31	|- ( ph -> ( h e. ( TermO ` C ) -> ( Z e. ( TermO ` C ) -> ( h e. ( Base ` C ) -> ( h ( ~=c ` C ) ZZring -> ( ZeroO ` C ) = (/) ) ) ) ) )
60	59	com34	|- ( ph -> ( h e. ( TermO ` C ) -> ( h e. ( Base ` C ) -> ( Z e. ( TermO ` C ) -> ( h ( ~=c ` C ) ZZring -> ( ZeroO ` C ) = (/) ) ) ) ) )
61	60	com25	|- ( ph -> ( h ( ~=c ` C ) ZZring -> ( h e. ( Base ` C ) -> ( Z e. ( TermO ` C ) -> ( h e. ( TermO ` C ) -> ( ZeroO ` C ) = (/) ) ) ) ) )
62	61	ad2antrr	|- ( ( ( ph /\ h e. ( InitO ` C ) ) /\ ZZring e. ( InitO ` C ) ) -> ( h ( ~=c ` C ) ZZring -> ( h e. ( Base ` C ) -> ( Z e. ( TermO ` C ) -> ( h e. ( TermO ` C ) -> ( ZeroO ` C ) = (/) ) ) ) ) )
63	17 62	mpd	|- ( ( ( ph /\ h e. ( InitO ` C ) ) /\ ZZring e. ( InitO ` C ) ) -> ( h e. ( Base ` C ) -> ( Z e. ( TermO ` C ) -> ( h e. ( TermO ` C ) -> ( ZeroO ` C ) = (/) ) ) ) )
64	63	ex	|- ( ( ph /\ h e. ( InitO ` C ) ) -> ( ZZring e. ( InitO ` C ) -> ( h e. ( Base ` C ) -> ( Z e. ( TermO ` C ) -> ( h e. ( TermO ` C ) -> ( ZeroO ` C ) = (/) ) ) ) ) )
65	64	com25	|- ( ( ph /\ h e. ( InitO ` C ) ) -> ( h e. ( TermO ` C ) -> ( h e. ( Base ` C ) -> ( Z e. ( TermO ` C ) -> ( ZZring e. ( InitO ` C ) -> ( ZeroO ` C ) = (/) ) ) ) ) )
66	65	expimpd	|- ( ph -> ( ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) -> ( h e. ( Base ` C ) -> ( Z e. ( TermO ` C ) -> ( ZZring e. ( InitO ` C ) -> ( ZeroO ` C ) = (/) ) ) ) ) )
67	66	com23	|- ( ph -> ( h e. ( Base ` C ) -> ( ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) -> ( Z e. ( TermO ` C ) -> ( ZZring e. ( InitO ` C ) -> ( ZeroO ` C ) = (/) ) ) ) ) )
68	67	impd	|- ( ph -> ( ( h e. ( Base ` C ) /\ ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) ) -> ( Z e. ( TermO ` C ) -> ( ZZring e. ( InitO ` C ) -> ( ZeroO ` C ) = (/) ) ) ) )
69	68	com24	|- ( ph -> ( ZZring e. ( InitO ` C ) -> ( Z e. ( TermO ` C ) -> ( ( h e. ( Base ` C ) /\ ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) ) -> ( ZeroO ` C ) = (/) ) ) ) )
70	13 69	mpd	|- ( ph -> ( Z e. ( TermO ` C ) -> ( ( h e. ( Base ` C ) /\ ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) ) -> ( ZeroO ` C ) = (/) ) ) )
71	12 70	mpd	|- ( ph -> ( ( h e. ( Base ` C ) /\ ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) ) -> ( ZeroO ` C ) = (/) ) )
72	71	adantr	|- ( ( ph /\ h e. ( ZeroO ` C ) ) -> ( ( h e. ( Base ` C ) /\ ( h e. ( InitO ` C ) /\ h e. ( TermO ` C ) ) ) -> ( ZeroO ` C ) = (/) ) )
73	11 72	mpd	|- ( ( ph /\ h e. ( ZeroO ` C ) ) -> ( ZeroO ` C ) = (/) )
74	73	expcom	|- ( h e. ( ZeroO ` C ) -> ( ph -> ( ZeroO ` C ) = (/) ) )
75	74	exlimiv	|- ( E. h h e. ( ZeroO ` C ) -> ( ph -> ( ZeroO ` C ) = (/) ) )
76	7 75	sylbi	|- ( -. ( ZeroO ` C ) = (/) -> ( ph -> ( ZeroO ` C ) = (/) ) )
77	6 76	pm2.61i	|- ( ph -> ( ZeroO ` C ) = (/) )