Metamath Proof Explorer

Theorem irinitoringc

Description: The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of Adamek p. 101 , and example in Lang p. 58. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses irinitoringc.u ${⊢}{\phi }\to {U}\in {V}$
irinitoringc.z ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in {U}$
irinitoringc.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
Assertion irinitoringc ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)$

Proof

Step Hyp Ref Expression
1 irinitoringc.u ${⊢}{\phi }\to {U}\in {V}$
2 irinitoringc.z ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in {U}$
3 irinitoringc.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
4 zex ${⊢}ℤ\in \mathrm{V}$
5 4 mptex ${⊢}\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\in \mathrm{V}$
6 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
7 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
8 3 6 1 7 ringchomfval ${⊢}{\phi }\to \mathrm{Hom}\left({C}\right)={\mathrm{RingHom}↾}_{\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)}$
9 8 adantr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \mathrm{Hom}\left({C}\right)={\mathrm{RingHom}↾}_{\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)}$
10 9 oveqd ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}={ℤ}_{\mathrm{ring}}\left({\mathrm{RingHom}↾}_{\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)}\right){r}$
11 id ${⊢}{ℤ}_{\mathrm{ring}}\in {U}\to {ℤ}_{\mathrm{ring}}\in {U}$
12 zringring ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
13 12 a1i ${⊢}{ℤ}_{\mathrm{ring}}\in {U}\to {ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
14 11 13 elind ${⊢}{ℤ}_{\mathrm{ring}}\in {U}\to {ℤ}_{\mathrm{ring}}\in \left({U}\cap \mathrm{Ring}\right)$
15 2 14 syl ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in \left({U}\cap \mathrm{Ring}\right)$
16 3 6 1 ringcbas ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={U}\cap \mathrm{Ring}$
17 15 16 eleqtrrd ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in {\mathrm{Base}}_{{C}}$
18 17 adantr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {ℤ}_{\mathrm{ring}}\in {\mathrm{Base}}_{{C}}$
19 simpr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {r}\in {\mathrm{Base}}_{{C}}$
20 18 19 ovresd ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {ℤ}_{\mathrm{ring}}\left({\mathrm{RingHom}↾}_{\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)}\right){r}={ℤ}_{\mathrm{ring}}\mathrm{RingHom}{r}$
21 16 eleq2d ${⊢}{\phi }\to \left({r}\in {\mathrm{Base}}_{{C}}↔{r}\in \left({U}\cap \mathrm{Ring}\right)\right)$
22 elin ${⊢}{r}\in \left({U}\cap \mathrm{Ring}\right)↔\left({r}\in {U}\wedge {r}\in \mathrm{Ring}\right)$
23 22 simprbi ${⊢}{r}\in \left({U}\cap \mathrm{Ring}\right)\to {r}\in \mathrm{Ring}$
24 21 23 syl6bi ${⊢}{\phi }\to \left({r}\in {\mathrm{Base}}_{{C}}\to {r}\in \mathrm{Ring}\right)$
25 24 imp ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {r}\in \mathrm{Ring}$
26 eqid ${⊢}{\cdot }_{{r}}={\cdot }_{{r}}$
27 eqid ${⊢}\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)=\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)$
28 eqid ${⊢}{1}_{{r}}={1}_{{r}}$
29 26 27 28 mulgrhm2 ${⊢}{r}\in \mathrm{Ring}\to {ℤ}_{\mathrm{ring}}\mathrm{RingHom}{r}=\left\{\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\right\}$
30 25 29 syl ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {ℤ}_{\mathrm{ring}}\mathrm{RingHom}{r}=\left\{\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\right\}$
31 10 20 30 3eqtrd ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to {ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}=\left\{\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\right\}$
32 sneq ${⊢}{f}=\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\to \left\{{f}\right\}=\left\{\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\right\}$
33 32 eqeq2d ${⊢}{f}=\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\to \left({ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}=\left\{{f}\right\}↔{ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}=\left\{\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\right\}\right)$
34 33 spcegv ${⊢}\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\in \mathrm{V}\to \left({ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}=\left\{\left({z}\in ℤ⟼{z}{\cdot }_{{r}}{1}_{{r}}\right)\right\}\to \exists {f}\phantom{\rule{.4em}{0ex}}{ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}=\left\{{f}\right\}\right)$
35 5 31 34 mpsyl ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}=\left\{{f}\right\}$
36 eusn ${⊢}\exists !{f}\phantom{\rule{.4em}{0ex}}{f}\in \left({ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}{ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}=\left\{{f}\right\}$
37 35 36 sylibr ${⊢}\left({\phi }\wedge {r}\in {\mathrm{Base}}_{{C}}\right)\to \exists !{f}\phantom{\rule{.4em}{0ex}}{f}\in \left({ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}\right)$
38 37 ralrimiva ${⊢}{\phi }\to \forall {r}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\exists !{f}\phantom{\rule{.4em}{0ex}}{f}\in \left({ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}\right)$
39 3 ringccat ${⊢}{U}\in {V}\to {C}\in \mathrm{Cat}$
40 1 39 syl ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
41 12 a1i ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
42 2 41 elind ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in \left({U}\cap \mathrm{Ring}\right)$
43 42 16 eleqtrrd ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in {\mathrm{Base}}_{{C}}$
44 6 7 40 43 isinito ${⊢}{\phi }\to \left({ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)↔\forall {r}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\exists !{f}\phantom{\rule{.4em}{0ex}}{f}\in \left({ℤ}_{\mathrm{ring}}\mathrm{Hom}\left({C}\right){r}\right)\right)$
45 38 44 mpbird ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)$