Metamath Proof Explorer

Theorem zrtermorngc

Description: The zero ring is a terminal object in the category of nonunital rings. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrinitorngc.u 
|- ( ph -> U e. V )
zrinitorngc.c 
|- C = ( RngCat ` U )
zrinitorngc.z 
|- ( ph -> Z e. ( Ring \ NzRing ) )
zrinitorngc.e 
|- ( ph -> Z e. U )
Assertion zrtermorngc 
|- ( ph -> Z e. ( TermO ` C ) )

Proof

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