ringccat

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

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

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

Metamath Proof Explorer