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 φUV
nzerooringczr.c C=RingCatU
nzerooringczr.z φZRingNzRing
nzerooringczr.e φZU
nzerooringczr.i φringU
Assertion nzerooringczr φZeroOC=

Proof

Step Hyp Ref Expression
1 nzerooringczr.u φUV
2 nzerooringczr.c C=RingCatU
3 nzerooringczr.z φZRingNzRing
4 nzerooringczr.e φZU
5 nzerooringczr.i φringU
6 ax-1 ZeroOC=φZeroOC=
7 neq0 ¬ZeroOC=hhZeroOC
8 2 ringccat UVCCat
9 1 8 syl φCCat
10 iszeroi CCathZeroOChBaseChInitOChTermOC
11 9 10 sylan φhZeroOChBaseChInitOChTermOC
12 1 2 3 4 zrtermoringc φZTermOC
13 1 5 2 irinitoringc φringInitOC
14 9 ad2antrr φhInitOCringInitOCCCat
15 simplr φhInitOCringInitOChInitOC
16 simpr φhInitOCringInitOCringInitOC
17 14 15 16 initoeu1w φhInitOCringInitOCh𝑐Cring
18 9 ad2antrr φhTermOCZTermOCCCat
19 simpr φhTermOCZTermOCZTermOC
20 simplr φhTermOCZTermOChTermOC
21 18 19 20 termoeu1w φhTermOCZTermOCZ𝑐Ch
22 cictr CCatZ𝑐Chh𝑐CringZ𝑐Cring
23 9 22 syl3an1 φZ𝑐Chh𝑐CringZ𝑐Cring
24 eqid IsoC=IsoC
25 eqid BaseC=BaseC
26 3 eldifad φZRing
27 4 26 elind φZURing
28 2 25 1 ringcbas φBaseC=URing
29 27 28 eleqtrrd φZBaseC
30 zringring ringRing
31 30 a1i φringRing
32 5 31 elind φringURing
33 32 28 eleqtrrd φringBaseC
34 24 25 9 29 33 cic φZ𝑐CringffZIsoCring
35 n0 ZIsoCringffZIsoCring
36 eqid HomC=HomC
37 25 36 24 9 29 33 isohom φZIsoCringZHomCring
38 ssn0 ZIsoCringZHomCringZIsoCringZHomCring
39 2 25 1 36 29 33 ringchom φZHomCring=ZRingHomring
40 39 neeq1d φZHomCringZRingHomring
41 zringnzr ringNzRing
42 nrhmzr ZRingNzRingringNzRingZRingHomring=
43 3 41 42 sylancl φZRingHomring=
44 eqneqall ZRingHomring=ZRingHomringZeroOC=
45 43 44 syl φZRingHomringZeroOC=
46 40 45 sylbid φZHomCringZeroOC=
47 38 46 syl5com ZIsoCringZHomCringZIsoCringφZeroOC=
48 47 expcom ZIsoCringZIsoCringZHomCringφZeroOC=
49 48 com13 φZIsoCringZHomCringZIsoCringZeroOC=
50 37 49 mpd φZIsoCringZeroOC=
51 35 50 syl5bir φffZIsoCringZeroOC=
52 34 51 sylbid φZ𝑐CringZeroOC=
53 52 3ad2ant1 φZ𝑐Chh𝑐CringZ𝑐CringZeroOC=
54 23 53 mpd φZ𝑐Chh𝑐CringZeroOC=
55 54 3exp φZ𝑐Chh𝑐CringZeroOC=
56 55 a1dd φZ𝑐ChhBaseCh𝑐CringZeroOC=
57 56 ad2antrr φhTermOCZTermOCZ𝑐ChhBaseCh𝑐CringZeroOC=
58 21 57 mpd φhTermOCZTermOChBaseCh𝑐CringZeroOC=
59 58 exp31 φhTermOCZTermOChBaseCh𝑐CringZeroOC=
60 59 com34 φhTermOChBaseCZTermOCh𝑐CringZeroOC=
61 60 com25 φh𝑐CringhBaseCZTermOChTermOCZeroOC=
62 61 ad2antrr φhInitOCringInitOCh𝑐CringhBaseCZTermOChTermOCZeroOC=
63 17 62 mpd φhInitOCringInitOChBaseCZTermOChTermOCZeroOC=
64 63 ex φhInitOCringInitOChBaseCZTermOChTermOCZeroOC=
65 64 com25 φhInitOChTermOChBaseCZTermOCringInitOCZeroOC=
66 65 expimpd φhInitOChTermOChBaseCZTermOCringInitOCZeroOC=
67 66 com23 φhBaseChInitOChTermOCZTermOCringInitOCZeroOC=
68 67 impd φhBaseChInitOChTermOCZTermOCringInitOCZeroOC=
69 68 com24 φringInitOCZTermOChBaseChInitOChTermOCZeroOC=
70 13 69 mpd φZTermOChBaseChInitOChTermOCZeroOC=
71 12 70 mpd φhBaseChInitOChTermOCZeroOC=
72 71 adantr φhZeroOChBaseChInitOChTermOCZeroOC=
73 11 72 mpd φhZeroOCZeroOC=
74 73 expcom hZeroOCφZeroOC=
75 74 exlimiv hhZeroOCφZeroOC=
76 7 75 sylbi ¬ZeroOC=φZeroOC=
77 6 76 pm2.61i φZeroOC=