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 
|- ( ph -> U e. V )
irinitoringc.z 
|- ( ph -> ZZring e. U )
irinitoringc.c 
|- C = ( RingCat ` U )
Assertion irinitoringc 
|- ( ph -> ZZring e. ( InitO ` C ) )

Proof

Step Hyp Ref Expression
1 irinitoringc.u 
 |-  ( ph -> U e. V )
2 irinitoringc.z 
 |-  ( ph -> ZZring e. U )
3 irinitoringc.c 
 |-  C = ( RingCat ` U )
4 zex 
 |-  ZZ e. _V
5 4 mptex 
 |-  ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) e. _V
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 3 6 1 7 ringchomfval 
 |-  ( ph -> ( Hom ` C ) = ( RingHom |` ( ( Base ` C ) X. ( Base ` C ) ) ) )
9 8 adantr 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( Hom ` C ) = ( RingHom |` ( ( Base ` C ) X. ( Base ` C ) ) ) )
10 9 oveqd 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( ZZring ( Hom ` C ) r ) = ( ZZring ( RingHom |` ( ( Base ` C ) X. ( Base ` C ) ) ) r ) )
11 id 
 |-  ( ZZring e. U -> ZZring e. U )
12 zringring 
 |-  ZZring e. Ring
13 12 a1i 
 |-  ( ZZring e. U -> ZZring e. Ring )
14 11 13 elind 
 |-  ( ZZring e. U -> ZZring e. ( U i^i Ring ) )
15 2 14 syl 
 |-  ( ph -> ZZring e. ( U i^i Ring ) )
16 3 6 1 ringcbas 
 |-  ( ph -> ( Base ` C ) = ( U i^i Ring ) )
17 15 16 eleqtrrd 
 |-  ( ph -> ZZring e. ( Base ` C ) )
18 17 adantr 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ZZring e. ( Base ` C ) )
19 simpr 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> r e. ( Base ` C ) )
20 18 19 ovresd 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( ZZring ( RingHom |` ( ( Base ` C ) X. ( Base ` C ) ) ) r ) = ( ZZring RingHom r ) )
21 16 eleq2d 
 |-  ( ph -> ( r e. ( Base ` C ) <-> r e. ( U i^i Ring ) ) )
22 elin 
 |-  ( r e. ( U i^i Ring ) <-> ( r e. U /\ r e. Ring ) )
23 22 simprbi 
 |-  ( r e. ( U i^i Ring ) -> r e. Ring )
24 21 23 syl6bi 
 |-  ( ph -> ( r e. ( Base ` C ) -> r e. Ring ) )
25 24 imp 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> r e. Ring )
26 eqid 
 |-  ( .g ` r ) = ( .g ` r )
27 eqid 
 |-  ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) = ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) )
28 eqid 
 |-  ( 1r ` r ) = ( 1r ` r )
29 26 27 28 mulgrhm2 
 |-  ( r e. Ring -> ( ZZring RingHom r ) = { ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) } )
30 25 29 syl 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( ZZring RingHom r ) = { ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) } )
31 10 20 30 3eqtrd 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( ZZring ( Hom ` C ) r ) = { ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) } )
32 sneq 
 |-  ( f = ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) -> { f } = { ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) } )
33 32 eqeq2d 
 |-  ( f = ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) -> ( ( ZZring ( Hom ` C ) r ) = { f } <-> ( ZZring ( Hom ` C ) r ) = { ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) } ) )
34 33 spcegv 
 |-  ( ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) e. _V -> ( ( ZZring ( Hom ` C ) r ) = { ( z e. ZZ |-> ( z ( .g ` r ) ( 1r ` r ) ) ) } -> E. f ( ZZring ( Hom ` C ) r ) = { f } ) )
35 5 31 34 mpsyl 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> E. f ( ZZring ( Hom ` C ) r ) = { f } )
36 eusn 
 |-  ( E! f f e. ( ZZring ( Hom ` C ) r ) <-> E. f ( ZZring ( Hom ` C ) r ) = { f } )
37 35 36 sylibr 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> E! f f e. ( ZZring ( Hom ` C ) r ) )
38 37 ralrimiva 
 |-  ( ph -> A. r e. ( Base ` C ) E! f f e. ( ZZring ( Hom ` C ) r ) )
39 3 ringccat 
 |-  ( U e. V -> C e. Cat )
40 1 39 syl 
 |-  ( ph -> C e. Cat )
41 12 a1i 
 |-  ( ph -> ZZring e. Ring )
42 2 41 elind 
 |-  ( ph -> ZZring e. ( U i^i Ring ) )
43 42 16 eleqtrrd 
 |-  ( ph -> ZZring e. ( Base ` C ) )
44 6 7 40 43 isinito 
 |-  ( ph -> ( ZZring e. ( InitO ` C ) <-> A. r e. ( Base ` C ) E! f f e. ( ZZring ( Hom ` C ) r ) ) )
45 38 44 mpbird 
 |-  ( ph -> ZZring e. ( InitO ` C ) )