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 ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
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 ‘ 𝐶 ) )