This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zrzeroorngc

Description: The zero ring is a zero object in the category of non-unital 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 zrzeroorngc 
|- ( ph -> Z e. ( ZeroO ` 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 1 2 3 4 zrinitorngc 
 |-  ( ph -> Z e. ( InitO ` C ) )
6 1 2 3 4 zrtermorngc 
 |-  ( ph -> Z e. ( TermO ` C ) )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 2 rngccat 
 |-  ( U e. V -> C e. Cat )
10 1 9 syl 
 |-  ( ph -> C e. Cat )
11 3 eldifad 
 |-  ( ph -> Z e. Ring )
12 ringrng 
 |-  ( Z e. Ring -> Z e. Rng )
13 11 12 syl 
 |-  ( ph -> Z e. Rng )
14 4 13 elind 
 |-  ( ph -> Z e. ( U i^i Rng ) )
15 2 7 1 rngcbas 
 |-  ( ph -> ( Base ` C ) = ( U i^i Rng ) )
16 14 15 eleqtrrd 
 |-  ( ph -> Z e. ( Base ` C ) )
17 7 8 10 16 iszeroo 
 |-  ( ph -> ( Z e. ( ZeroO ` C ) <-> ( Z e. ( InitO ` C ) /\ Z e. ( TermO ` C ) ) ) )
18 5 6 17 mpbir2and 
 |-  ( ph -> Z e. ( ZeroO ` C ) )