Metamath Proof Explorer


Theorem zrtermorngc

Description: The zero ring is a terminal object in the category of nonunital rings. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrinitorngc.u φUV
zrinitorngc.c C=RngCatU
zrinitorngc.z φZRingNzRing
zrinitorngc.e φZU
Assertion zrtermorngc φZTermOC

Proof

Step Hyp Ref Expression
1 zrinitorngc.u φUV
2 zrinitorngc.c C=RngCatU
3 zrinitorngc.z φZRingNzRing
4 zrinitorngc.e φZU
5 eqid BaseC=BaseC
6 2 5 1 rngcbas φBaseC=URng
7 6 eleq2d φrBaseCrURng
8 elin rURngrUrRng
9 8 simprbi rURngrRng
10 7 9 syl6bi φrBaseCrRng
11 10 imp φrBaseCrRng
12 3 adantr φrBaseCZRingNzRing
13 eqid Baser=Baser
14 eqid 0Z=0Z
15 eqid xBaser0Z=xBaser0Z
16 13 14 15 c0rnghm rRngZRingNzRingxBaser0ZrRngHomoZ
17 11 12 16 syl2anc φrBaseCxBaser0ZrRngHomoZ
18 simpr φrBaseCxBaser0ZrRngHomoZxBaser0ZrRngHomoZ
19 1 adantr φrBaseCUV
20 eqid HomC=HomC
21 simpr φrBaseCrBaseC
22 eldifi ZRingNzRingZRing
23 ringrng ZRingZRng
24 3 22 23 3syl φZRng
25 4 24 elind φZURng
26 25 6 eleqtrrd φZBaseC
27 26 adantr φrBaseCZBaseC
28 2 5 19 20 21 27 rngchom φrBaseCrHomCZ=rRngHomoZ
29 28 eqcomd φrBaseCrRngHomoZ=rHomCZ
30 29 eleq2d φrBaseCxBaser0ZrRngHomoZxBaser0ZrHomCZ
31 30 biimpa φrBaseCxBaser0ZrRngHomoZxBaser0ZrHomCZ
32 28 eleq2d φrBaseChrHomCZhrRngHomoZ
33 eqid BaseZ=BaseZ
34 13 33 rnghmf hrRngHomoZh:BaserBaseZ
35 32 34 syl6bi φrBaseChrHomCZh:BaserBaseZ
36 35 adantr φrBaseCxBaser0ZrRngHomoZhrHomCZh:BaserBaseZ
37 ffn h:BaserBaseZhFnBaser
38 37 adantl φrBaseCxBaser0ZrRngHomoZh:BaserBaseZhFnBaser
39 fvex 0ZV
40 39 15 fnmpti xBaser0ZFnBaser
41 40 a1i φrBaseCxBaser0ZrRngHomoZh:BaserBaseZxBaser0ZFnBaser
42 33 14 0ringbas ZRingNzRingBaseZ=0Z
43 3 42 syl φBaseZ=0Z
44 43 adantr φrBaseCBaseZ=0Z
45 44 feq3d φrBaseCh:BaserBaseZh:Baser0Z
46 fvconst h:Baser0ZaBaserha=0Z
47 46 ex h:Baser0ZaBaserha=0Z
48 45 47 syl6bi φrBaseCh:BaserBaseZaBaserha=0Z
49 48 adantr φrBaseCxBaser0ZrRngHomoZh:BaserBaseZaBaserha=0Z
50 49 imp31 φrBaseCxBaser0ZrRngHomoZh:BaserBaseZaBaserha=0Z
51 eqidd aBaserxBaser0Z=xBaser0Z
52 eqidd aBaserx=a0Z=0Z
53 id aBaseraBaser
54 39 a1i aBaser0ZV
55 51 52 53 54 fvmptd aBaserxBaser0Za=0Z
56 55 adantl φrBaseCxBaser0ZrRngHomoZh:BaserBaseZaBaserxBaser0Za=0Z
57 50 56 eqtr4d φrBaseCxBaser0ZrRngHomoZh:BaserBaseZaBaserha=xBaser0Za
58 38 41 57 eqfnfvd φrBaseCxBaser0ZrRngHomoZh:BaserBaseZh=xBaser0Z
59 58 ex φrBaseCxBaser0ZrRngHomoZh:BaserBaseZh=xBaser0Z
60 36 59 syld φrBaseCxBaser0ZrRngHomoZhrHomCZh=xBaser0Z
61 60 alrimiv φrBaseCxBaser0ZrRngHomoZhhrHomCZh=xBaser0Z
62 18 31 61 3jca φrBaseCxBaser0ZrRngHomoZxBaser0ZrRngHomoZxBaser0ZrHomCZhhrHomCZh=xBaser0Z
63 17 62 mpdan φrBaseCxBaser0ZrRngHomoZxBaser0ZrHomCZhhrHomCZh=xBaser0Z
64 eleq1 h=xBaser0ZhrHomCZxBaser0ZrHomCZ
65 64 eqeu xBaser0ZrRngHomoZxBaser0ZrHomCZhhrHomCZh=xBaser0Z∃!hhrHomCZ
66 63 65 syl φrBaseC∃!hhrHomCZ
67 66 ralrimiva φrBaseC∃!hhrHomCZ
68 2 rngccat UVCCat
69 1 68 syl φCCat
70 5 20 69 26 istermo φZTermOCrBaseC∃!hhrHomCZ
71 67 70 mpbird φZTermOC