rngccat

Description: The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020) (Revised by AV, 9-Mar-2020)

		Ref	Expression
	Hypothesis	rngccat.c	$⊢ C = RngCat (U)$
	Assertion	rngccat	$⊢ U \in V \to C \in Cat$

Step	Hyp	Ref	Expression
1		rngccat.c	$⊢ C = RngCat (U)$
2		id	$⊢ U \in V \to U \in V$
3		eqidd	$⊢ U \in V \to U \cap Rng = U \cap Rng$
4		eqidd	$⊢ U \in V \to {RngHomo ↾}_{((U \cap Rng) \times (U \cap Rng))} = {RngHomo ↾}_{((U \cap Rng) \times (U \cap Rng))}$
5	1 2 3 4	rngcval	$⊢ U \in V \to C = ExtStrCat (U) ↾_{cat} ({RngHomo ↾}_{((U \cap Rng) \times (U \cap Rng))})$
6		eqid	$⊢ ExtStrCat (U) ↾_{cat} ({RngHomo ↾}_{((U \cap Rng) \times (U \cap Rng))}) = ExtStrCat (U) ↾_{cat} ({RngHomo ↾}_{((U \cap Rng) \times (U \cap Rng))})$
7		eqid	$⊢ ExtStrCat (U) = ExtStrCat (U)$
8		eqidd	$⊢ U \in V \to Rng \cap U = Rng \cap U$
9		incom	$⊢ U \cap Rng = Rng \cap U$
10	9	a1i	$⊢ U \in V \to U \cap Rng = Rng \cap U$
11	10	sqxpeqd	$⊢ U \in V \to (U \cap Rng) \times (U \cap Rng) = (Rng \cap U) \times (Rng \cap U)$
12	11	reseq2d	$⊢ U \in V \to {RngHomo ↾}_{((U \cap Rng) \times (U \cap Rng))} = {RngHomo ↾}_{((Rng \cap U) \times (Rng \cap U))}$
13	7 2 8 12	rnghmsubcsetc	$⊢ U \in V \to {RngHomo ↾}_{((U \cap Rng) \times (U \cap Rng))} \in Subcat (ExtStrCat (U))$
14	6 13	subccat	$⊢ U \in V \to ExtStrCat (U) ↾_{cat} ({RngHomo ↾}_{((U \cap Rng) \times (U \cap Rng))}) \in Cat$
15	5 14	eqeltrd	$⊢ U \in V \to C \in Cat$

Metamath Proof Explorer