Metamath Proof Explorer

Theorem zrinitorngc

Description: The zero ring is an initial object in the category of nonunital rings. (Contributed by AV, 18-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 zrinitorngc 
|- ( ph -> Z e. ( InitO ` 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 ` Z ) = ( Base ` Z )
14 eqid 
 |-  ( 0g ` r ) = ( 0g ` r )
15 eqid 
 |-  ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) = ( x e. ( Base ` Z ) |-> ( 0g ` r ) )
16 13 14 15 zrrnghm 
 |-  ( ( r e. Rng /\ Z e. ( Ring \ NzRing ) ) -> ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) )
17 11 12 16 syl2anc 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) )
18 simpr 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) ) -> ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) )
19 1 adantr 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> U e. V )
20 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
21 eldifi 
 |-  ( Z e. ( Ring \ NzRing ) -> Z e. Ring )
22 ringrng 
 |-  ( Z e. Ring -> Z e. Rng )
23 3 21 22 3syl 
 |-  ( ph -> Z e. Rng )
24 4 23 elind 
 |-  ( ph -> Z e. ( U i^i Rng ) )
25 24 6 eleqtrrd 
 |-  ( ph -> Z e. ( Base ` C ) )
26 25 adantr 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> Z e. ( Base ` C ) )
27 simpr 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> r e. ( Base ` C ) )
28 2 5 19 20 26 27 rngchom 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( Z ( Hom ` C ) r ) = ( Z RngHomo r ) )
29 28 eqcomd 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( Z RngHomo r ) = ( Z ( Hom ` C ) r ) )
30 29 eleq2d 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) <-> ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z ( Hom ` C ) r ) ) )
31 30 biimpa 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) ) -> ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z ( Hom ` C ) r ) )
32 28 eleq2d 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( h e. ( Z ( Hom ` C ) r ) <-> h e. ( Z RngHomo r ) ) )
33 eqid 
 |-  ( Base ` r ) = ( Base ` r )
34 13 33 rnghmf 
 |-  ( h e. ( Z RngHomo r ) -> h : ( Base ` Z ) --> ( Base ` r ) )
35 32 34 syl6bi 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( h e. ( Z ( Hom ` C ) r ) -> h : ( Base ` Z ) --> ( Base ` r ) ) )
36 35 imp 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) -> h : ( Base ` Z ) --> ( Base ` r ) )
37 ffn 
 |-  ( h : ( Base ` Z ) --> ( Base ` r ) -> h Fn ( Base ` Z ) )
38 37 adantl 
 |-  ( ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) /\ h : ( Base ` Z ) --> ( Base ` r ) ) -> h Fn ( Base ` Z ) )
39 fvex 
 |-  ( 0g ` r ) e. _V
40 39 15 fnmpti 
 |-  ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) Fn ( Base ` Z )
41 40 a1i 
 |-  ( ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) /\ h : ( Base ` Z ) --> ( Base ` r ) ) -> ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) Fn ( Base ` Z ) )
42 32 biimpa 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) -> h e. ( Z RngHomo r ) )
43 rnghmghm 
 |-  ( h e. ( Z RngHomo r ) -> h e. ( Z GrpHom r ) )
44 eqid 
 |-  ( 0g ` Z ) = ( 0g ` Z )
45 44 14 ghmid 
 |-  ( h e. ( Z GrpHom r ) -> ( h ` ( 0g ` Z ) ) = ( 0g ` r ) )
46 42 43 45 3syl 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) -> ( h ` ( 0g ` Z ) ) = ( 0g ` r ) )
47 46 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) /\ h : ( Base ` Z ) --> ( Base ` r ) ) /\ a e. ( Base ` Z ) ) -> ( h ` ( 0g ` Z ) ) = ( 0g ` r ) )
48 13 44 0ringbas 
 |-  ( Z e. ( Ring \ NzRing ) -> ( Base ` Z ) = { ( 0g ` Z ) } )
49 3 48 syl 
 |-  ( ph -> ( Base ` Z ) = { ( 0g ` Z ) } )
50 49 eleq2d 
 |-  ( ph -> ( a e. ( Base ` Z ) <-> a e. { ( 0g ` Z ) } ) )
51 elsni 
 |-  ( a e. { ( 0g ` Z ) } -> a = ( 0g ` Z ) )
52 51 fveq2d 
 |-  ( a e. { ( 0g ` Z ) } -> ( h ` a ) = ( h ` ( 0g ` Z ) ) )
53 50 52 syl6bi 
 |-  ( ph -> ( a e. ( Base ` Z ) -> ( h ` a ) = ( h ` ( 0g ` Z ) ) ) )
54 53 adantr 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( a e. ( Base ` Z ) -> ( h ` a ) = ( h ` ( 0g ` Z ) ) ) )
55 54 ad2antrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) /\ h : ( Base ` Z ) --> ( Base ` r ) ) -> ( a e. ( Base ` Z ) -> ( h ` a ) = ( h ` ( 0g ` Z ) ) ) )
56 55 imp 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) /\ h : ( Base ` Z ) --> ( Base ` r ) ) /\ a e. ( Base ` Z ) ) -> ( h ` a ) = ( h ` ( 0g ` Z ) ) )
57 eqidd 
 |-  ( a e. ( Base ` Z ) -> ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) )
58 eqidd 
 |-  ( ( a e. ( Base ` Z ) /\ x = a ) -> ( 0g ` r ) = ( 0g ` r ) )
59 id 
 |-  ( a e. ( Base ` Z ) -> a e. ( Base ` Z ) )
60 39 a1i 
 |-  ( a e. ( Base ` Z ) -> ( 0g ` r ) e. _V )
61 57 58 59 60 fvmptd 
 |-  ( a e. ( Base ` Z ) -> ( ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ` a ) = ( 0g ` r ) )
62 61 adantl 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) /\ h : ( Base ` Z ) --> ( Base ` r ) ) /\ a e. ( Base ` Z ) ) -> ( ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ` a ) = ( 0g ` r ) )
63 47 56 62 3eqtr4d 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) /\ h : ( Base ` Z ) --> ( Base ` r ) ) /\ a e. ( Base ` Z ) ) -> ( h ` a ) = ( ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ` a ) )
64 38 41 63 eqfnfvd 
 |-  ( ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) /\ h : ( Base ` Z ) --> ( Base ` r ) ) -> h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) )
65 36 64 mpdan 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ h e. ( Z ( Hom ` C ) r ) ) -> h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) )
66 65 ex 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( h e. ( Z ( Hom ` C ) r ) -> h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ) )
67 66 adantr 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) ) -> ( h e. ( Z ( Hom ` C ) r ) -> h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ) )
68 67 alrimiv 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) ) -> A. h ( h e. ( Z ( Hom ` C ) r ) -> h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ) )
69 18 31 68 3jca 
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) ) -> ( ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) /\ ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z ( Hom ` C ) r ) /\ A. h ( h e. ( Z ( Hom ` C ) r ) -> h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ) ) )
70 17 69 mpdan 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) /\ ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z ( Hom ` C ) r ) /\ A. h ( h e. ( Z ( Hom ` C ) r ) -> h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ) ) )
71 eleq1 
 |-  ( h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) -> ( h e. ( Z ( Hom ` C ) r ) <-> ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z ( Hom ` C ) r ) ) )
72 71 eqeu 
 |-  ( ( ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z RngHomo r ) /\ ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) e. ( Z ( Hom ` C ) r ) /\ A. h ( h e. ( Z ( Hom ` C ) r ) -> h = ( x e. ( Base ` Z ) |-> ( 0g ` r ) ) ) ) -> E! h h e. ( Z ( Hom ` C ) r ) )
73 70 72 syl 
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> E! h h e. ( Z ( Hom ` C ) r ) )
74 73 ralrimiva 
 |-  ( ph -> A. r e. ( Base ` C ) E! h h e. ( Z ( Hom ` C ) r ) )
75 2 rngccat 
 |-  ( U e. V -> C e. Cat )
76 1 75 syl 
 |-  ( ph -> C e. Cat )
77 5 20 76 25 isinito 
 |-  ( ph -> ( Z e. ( InitO ` C ) <-> A. r e. ( Base ` C ) E! h h e. ( Z ( Hom ` C ) r ) ) )
78 74 77 mpbird 
 |-  ( ph -> Z e. ( InitO ` C ) )