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	$$⊢\phi \to U\in V$$
	zrinitorngc.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
	zrinitorngc.z	$$⊢\phi \to Z\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)$$
	zrinitorngc.e	$$⊢\phi \to Z\in U$$
Assertion	zrzeroorngc	$$⊢\phi \to Z\in \mathrm{ZeroO}\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		zrinitorngc.u	$$⊢\phi \to U\in V$$
2		zrinitorngc.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
3		zrinitorngc.z	$$⊢\phi \to Z\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)$$
4		zrinitorngc.e	$$⊢\phi \to Z\in U$$
5	1 2 3 4	zrinitorngc	$$⊢\phi \to Z\in \mathrm{InitO}\left(C\right)$$
6	1 2 3 4	zrtermorngc	$$⊢\phi \to Z\in \mathrm{TermO}\left(C\right)$$
7		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
8		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
9	2	rngccat	$$⊢U\in V\to C\in \mathrm{Cat}$$
10	1 9	syl	$$⊢\phi \to C\in \mathrm{Cat}$$
11	3	eldifad	$$⊢\phi \to Z\in \mathrm{Ring}$$
12		ringrng	$$⊢Z\in \mathrm{Ring}\to Z\in \mathrm{Rng}$$
13	11 12	syl	$$⊢\phi \to Z\in \mathrm{Rng}$$
14	4 13	elind	$$⊢\phi \to Z\in \left(U\cap \mathrm{Rng}\right)$$
15	2 7 1	rngcbas	$$⊢\phi \to {\mathrm{Base}}_C=U\cap \mathrm{Rng}$$
16	14 15	eleqtrrd	$$⊢\phi \to Z\in {\mathrm{Base}}_C$$
17	7 8 10 16	iszeroo	$$⊢\phi \to \left(Z\in \mathrm{ZeroO}\left(C\right)\leftrightarrow \left(Z\in \mathrm{InitO}\left(C\right)\wedge Z\in \mathrm{TermO}\left(C\right)\right)\right)$$
18	5 6 17	mpbir2and	$$⊢\phi \to Z\in \mathrm{ZeroO}\left(C\right)$$