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 ( 𝜑𝑈𝑉 )
irinitoringc.z ( 𝜑 → ℤring𝑈 )
irinitoringc.c 𝐶 = ( RingCat ‘ 𝑈 )
Assertion irinitoringc ( 𝜑 → ℤring ∈ ( InitO ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 irinitoringc.u ( 𝜑𝑈𝑉 )
2 irinitoringc.z ( 𝜑 → ℤring𝑈 )
3 irinitoringc.c 𝐶 = ( RingCat ‘ 𝑈 )
4 zex ℤ ∈ V
5 4 mptex ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) ∈ V
6 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8 3 6 1 7 ringchomfval ( 𝜑 → ( Hom ‘ 𝐶 ) = ( RingHom ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
9 8 adantr ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( Hom ‘ 𝐶 ) = ( RingHom ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
10 9 oveqd ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) = ( ℤring ( RingHom ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) 𝑟 ) )
11 id ( ℤring𝑈 → ℤring𝑈 )
12 zringring ring ∈ Ring
13 12 a1i ( ℤring𝑈 → ℤring ∈ Ring )
14 11 13 elind ( ℤring𝑈 → ℤring ∈ ( 𝑈 ∩ Ring ) )
15 2 14 syl ( 𝜑 → ℤring ∈ ( 𝑈 ∩ Ring ) )
16 3 6 1 ringcbas ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Ring ) )
17 15 16 eleqtrrd ( 𝜑 → ℤring ∈ ( Base ‘ 𝐶 ) )
18 17 adantr ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → ℤring ∈ ( Base ‘ 𝐶 ) )
19 simpr ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑟 ∈ ( Base ‘ 𝐶 ) )
20 18 19 ovresd ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℤring ( RingHom ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) 𝑟 ) = ( ℤring RingHom 𝑟 ) )
21 16 eleq2d ( 𝜑 → ( 𝑟 ∈ ( Base ‘ 𝐶 ) ↔ 𝑟 ∈ ( 𝑈 ∩ Ring ) ) )
22 elin ( 𝑟 ∈ ( 𝑈 ∩ Ring ) ↔ ( 𝑟𝑈𝑟 ∈ Ring ) )
23 22 simprbi ( 𝑟 ∈ ( 𝑈 ∩ Ring ) → 𝑟 ∈ Ring )
24 21 23 syl6bi ( 𝜑 → ( 𝑟 ∈ ( Base ‘ 𝐶 ) → 𝑟 ∈ Ring ) )
25 24 imp ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑟 ∈ Ring )
26 eqid ( .g𝑟 ) = ( .g𝑟 )
27 eqid ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) = ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) )
28 eqid ( 1r𝑟 ) = ( 1r𝑟 )
29 26 27 28 mulgrhm2 ( 𝑟 ∈ Ring → ( ℤring RingHom 𝑟 ) = { ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) } )
30 25 29 syl ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℤring RingHom 𝑟 ) = { ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) } )
31 10 20 30 3eqtrd ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) = { ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) } )
32 sneq ( 𝑓 = ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) → { 𝑓 } = { ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) } )
33 32 eqeq2d ( 𝑓 = ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) → ( ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) = { 𝑓 } ↔ ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) = { ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) } ) )
34 33 spcegv ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) ∈ V → ( ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) = { ( 𝑧 ∈ ℤ ↦ ( 𝑧 ( .g𝑟 ) ( 1r𝑟 ) ) ) } → ∃ 𝑓 ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) = { 𝑓 } ) )
35 5 31 34 mpsyl ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → ∃ 𝑓 ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) = { 𝑓 } )
36 eusn ( ∃! 𝑓 𝑓 ∈ ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) ↔ ∃ 𝑓 ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) = { 𝑓 } )
37 35 36 sylibr ( ( 𝜑𝑟 ∈ ( Base ‘ 𝐶 ) ) → ∃! 𝑓 𝑓 ∈ ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) )
38 37 ralrimiva ( 𝜑 → ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) )
39 3 ringccat ( 𝑈𝑉𝐶 ∈ Cat )
40 1 39 syl ( 𝜑𝐶 ∈ Cat )
41 12 a1i ( 𝜑 → ℤring ∈ Ring )
42 2 41 elind ( 𝜑 → ℤring ∈ ( 𝑈 ∩ Ring ) )
43 42 16 eleqtrrd ( 𝜑 → ℤring ∈ ( Base ‘ 𝐶 ) )
44 6 7 40 43 isinito ( 𝜑 → ( ℤring ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( ℤring ( Hom ‘ 𝐶 ) 𝑟 ) ) )
45 38 44 mpbird ( 𝜑 → ℤring ∈ ( InitO ‘ 𝐶 ) )