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 biimtrdi ⊢ ( 𝜑 → ( 𝑟 ∈ ( 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 ‘ 𝐶 ) )