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 ( 𝜑𝑈𝑉 )
zrinitorngc.c 𝐶 = ( RngCat ‘ 𝑈 )
zrinitorngc.z ( 𝜑𝑍 ∈ ( Ring ∖ NzRing ) )
zrinitorngc.e ( 𝜑𝑍𝑈 )
Assertion zrzeroorngc ( 𝜑𝑍 ∈ ( ZeroO ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 zrinitorngc.u ( 𝜑𝑈𝑉 )
2 zrinitorngc.c 𝐶 = ( RngCat ‘ 𝑈 )
3 zrinitorngc.z ( 𝜑𝑍 ∈ ( Ring ∖ NzRing ) )
4 zrinitorngc.e ( 𝜑𝑍𝑈 )
5 1 2 3 4 zrinitorngc ( 𝜑𝑍 ∈ ( InitO ‘ 𝐶 ) )
6 1 2 3 4 zrtermorngc ( 𝜑𝑍 ∈ ( TermO ‘ 𝐶 ) )
7 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 2 rngccat ( 𝑈𝑉𝐶 ∈ Cat )
10 1 9 syl ( 𝜑𝐶 ∈ Cat )
11 3 eldifad ( 𝜑𝑍 ∈ Ring )
12 ringrng ( 𝑍 ∈ Ring → 𝑍 ∈ Rng )
13 11 12 syl ( 𝜑𝑍 ∈ Rng )
14 4 13 elind ( 𝜑𝑍 ∈ ( 𝑈 ∩ Rng ) )
15 2 7 1 rngcbas ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Rng ) )
16 14 15 eleqtrrd ( 𝜑𝑍 ∈ ( Base ‘ 𝐶 ) )
17 7 8 10 16 iszeroo ( 𝜑 → ( 𝑍 ∈ ( ZeroO ‘ 𝐶 ) ↔ ( 𝑍 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑍 ∈ ( TermO ‘ 𝐶 ) ) ) )
18 5 6 17 mpbir2and ( 𝜑𝑍 ∈ ( ZeroO ‘ 𝐶 ) )