Metamath Proof Explorer

Theorem zrtermoringc

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

Ref Expression
Hypotheses zrtermoringc.u ${⊢}{\phi }\to {U}\in {V}$
zrtermoringc.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
zrtermoringc.z ${⊢}{\phi }\to {Z}\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)$
zrtermoringc.e ${⊢}{\phi }\to {Z}\in {U}$
Assertion zrtermoringc ${⊢}{\phi }\to {Z}\in \mathrm{TermO}\left({C}\right)$

Proof

Step Hyp Ref Expression
1 zrtermoringc.u ${⊢}{\phi }\to {U}\in {V}$
2 zrtermoringc.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
3 zrtermoringc.z ${⊢}{\phi }\to {Z}\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)$
4 zrtermoringc.e ${⊢}{\phi }\to {Z}\in {U}$
5 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
6 2 5 1 ringcbas ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={U}\cap \mathrm{Ring}$
7 6 eleq2d ${⊢}{\phi }\to \left({r}\in {\mathrm{Base}}_{{C}}↔{r}\in \left({U}\cap \mathrm{Ring}\right)\right)$
8 elin ${⊢}{r}\in \left({U}\cap \mathrm{Ring}\right)↔\left({r}\in {U}\wedge {r}\in \mathrm{Ring}\right)$
9 8 simprbi ${⊢}{r}\in \left({U}\cap \mathrm{Ring}\right)\to {r}\in \mathrm{Ring}$
10 7 9 syl6bi ${⊢}{\phi }\to \left({r}\in {\mathrm{Base}}_{{C}}\to {r}\in \mathrm{Ring}\right)$
11 10 imp ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {r}\in \mathrm{Ring}$
12 3 adantr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {Z}\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)$
13 eqid ${⊢}{\mathrm{Base}}_{{r}}={\mathrm{Base}}_{{r}}$
14 eqid ${⊢}{0}_{{Z}}={0}_{{Z}}$
15 eqid ${⊢}\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)$
16 13 14 15 c0rhm ${⊢}\left({r}\in \mathrm{Ring}\wedge {Z}\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\right)\to \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)$
17 11 12 16 syl2anc ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)$
18 simpr ${⊢}\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\to \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)$
19 1 adantr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {U}\in {V}$
20 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
21 simpr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {r}\in {\mathrm{Base}}_{{C}}$
22 3 eldifad ${⊢}{\phi }\to {Z}\in \mathrm{Ring}$
23 4 22 elind ${⊢}{\phi }\to {Z}\in \left({U}\cap \mathrm{Ring}\right)$
24 23 6 eleqtrrd ${⊢}{\phi }\to {Z}\in {\mathrm{Base}}_{{C}}$
25 24 adantr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {Z}\in {\mathrm{Base}}_{{C}}$
26 2 5 19 20 21 25 ringchom ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {r}\mathrm{Hom}\left({C}\right){Z}={r}\mathrm{RingHom}{Z}$
27 26 eqcomd ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {r}\mathrm{RingHom}{Z}={r}\mathrm{Hom}\left({C}\right){Z}$
28 27 eleq2d ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \left(\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)↔\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\right)$
29 28 biimpa ${⊢}\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\to \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)$
30 26 eleq2d ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)↔{h}\in \left({r}\mathrm{RingHom}{Z}\right)\right)$
31 eqid ${⊢}{\mathrm{Base}}_{{Z}}={\mathrm{Base}}_{{Z}}$
32 13 31 rhmf ${⊢}{h}\in \left({r}\mathrm{RingHom}{Z}\right)\to {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}$
33 30 32 syl6bi ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\to {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\right)$
34 33 adantr ${⊢}\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\to \left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\to {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\right)$
35 ffn ${⊢}{h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\to {h}Fn{\mathrm{Base}}_{{r}}$
36 35 adantl ${⊢}\left(\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\wedge {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\right)\to {h}Fn{\mathrm{Base}}_{{r}}$
37 fvex ${⊢}{0}_{{Z}}\in \mathrm{V}$
38 37 15 fnmpti ${⊢}\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)Fn{\mathrm{Base}}_{{r}}$
39 38 a1i ${⊢}\left(\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\wedge {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\right)\to \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)Fn{\mathrm{Base}}_{{r}}$
40 31 14 0ringbas ${⊢}{Z}\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\to {\mathrm{Base}}_{{Z}}=\left\{{0}_{{Z}}\right\}$
41 3 40 syl ${⊢}{\phi }\to {\mathrm{Base}}_{{Z}}=\left\{{0}_{{Z}}\right\}$
42 41 adantr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {\mathrm{Base}}_{{Z}}=\left\{{0}_{{Z}}\right\}$
43 42 feq3d ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \left({h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}↔{h}:{\mathrm{Base}}_{{r}}⟶\left\{{0}_{{Z}}\right\}\right)$
44 fvconst ${⊢}\left({h}:{\mathrm{Base}}_{{r}}⟶\left\{{0}_{{Z}}\right\}\wedge {a}\in {\mathrm{Base}}_{{r}}\right)\to {h}\left({a}\right)={0}_{{Z}}$
45 44 ex ${⊢}{h}:{\mathrm{Base}}_{{r}}⟶\left\{{0}_{{Z}}\right\}\to \left({a}\in {\mathrm{Base}}_{{r}}\to {h}\left({a}\right)={0}_{{Z}}\right)$
46 43 45 syl6bi ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \left({h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\to \left({a}\in {\mathrm{Base}}_{{r}}\to {h}\left({a}\right)={0}_{{Z}}\right)\right)$
47 46 adantr ${⊢}\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\to \left({h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\to \left({a}\in {\mathrm{Base}}_{{r}}\to {h}\left({a}\right)={0}_{{Z}}\right)\right)$
48 47 imp31 ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\wedge {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\right)\wedge {a}\in {\mathrm{Base}}_{{r}}\right)\to {h}\left({a}\right)={0}_{{Z}}$
49 eqidd ${⊢}{a}\in {\mathrm{Base}}_{{r}}\to \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)$
50 eqidd ${⊢}\left({a}\in {\mathrm{Base}}_{{r}}\wedge {x}={a}\right)\to {0}_{{Z}}={0}_{{Z}}$
51 id ${⊢}{a}\in {\mathrm{Base}}_{{r}}\to {a}\in {\mathrm{Base}}_{{r}}$
52 37 a1i ${⊢}{a}\in {\mathrm{Base}}_{{r}}\to {0}_{{Z}}\in \mathrm{V}$
53 49 50 51 52 fvmptd ${⊢}{a}\in {\mathrm{Base}}_{{r}}\to \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\left({a}\right)={0}_{{Z}}$
54 53 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\wedge {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\right)\wedge {a}\in {\mathrm{Base}}_{{r}}\right)\to \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\left({a}\right)={0}_{{Z}}$
55 48 54 eqtr4d ${⊢}\left(\left(\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\wedge {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\right)\wedge {a}\in {\mathrm{Base}}_{{r}}\right)\to {h}\left({a}\right)=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\left({a}\right)$
56 36 39 55 eqfnfvd ${⊢}\left(\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\wedge {h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\right)\to {h}=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)$
57 56 ex ${⊢}\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\to \left({h}:{\mathrm{Base}}_{{r}}⟶{\mathrm{Base}}_{{Z}}\to {h}=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\right)$
58 34 57 syld ${⊢}\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\to \left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\to {h}=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\right)$
59 58 alrimiv ${⊢}\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\to \forall {h}\phantom{\rule{.4em}{0ex}}\left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\to {h}=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\right)$
60 18 29 59 3jca ${⊢}\left(\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\right)\to \left(\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\wedge \forall {h}\phantom{\rule{.4em}{0ex}}\left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\to {h}=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\right)\right)$
61 17 60 mpdan ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \left(\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\wedge \forall {h}\phantom{\rule{.4em}{0ex}}\left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\to {h}=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\right)\right)$
62 eleq1 ${⊢}{h}=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\to \left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)↔\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\right)$
63 62 eqeu ${⊢}\left(\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{RingHom}{Z}\right)\wedge \left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\wedge \forall {h}\phantom{\rule{.4em}{0ex}}\left({h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\to {h}=\left({x}\in {\mathrm{Base}}_{{r}}⟼{0}_{{Z}}\right)\right)\right)\to \exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)$
64 61 63 syl ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)$
65 64 ralrimiva ${⊢}{\phi }\to \forall {r}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)$
66 2 ringccat ${⊢}{U}\in {V}\to {C}\in \mathrm{Cat}$
67 1 66 syl ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
68 5 20 67 24 istermo ${⊢}{\phi }\to \left({Z}\in \mathrm{TermO}\left({C}\right)↔\forall {r}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({r}\mathrm{Hom}\left({C}\right){Z}\right)\right)$
69 65 68 mpbird ${⊢}{\phi }\to {Z}\in \mathrm{TermO}\left({C}\right)$