This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrid 
 |-  ( 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 ) = (/) )