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 
|- ( ph -> U e. V )
zrtermoringc.c 
|- C = ( RingCat ` U )
zrtermoringc.z 
|- ( ph -> Z e. ( Ring \ NzRing ) )
zrtermoringc.e 
|- ( ph -> Z e. U )
Assertion zrtermoringc 
|- ( ph -> Z e. ( TermO ` C ) )

Proof

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