ringcval

Description: Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020) (Revised by AV, 8-Mar-2020)

Step	Hyp	Ref	Expression
1		ringcval.c	$⊢ C = RingCat (U)$
2		ringcval.u	$⊢ φ \to U \in V$
3		ringcval.b	$⊢ φ \to B = U \cap Ring$
4		ringcval.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
5		df-ringc	$⊢ RingCat = (u \in V ⟼ ExtStrCat (u) ↾_{cat} ({RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))}))$
6		fveq2	$⊢ u = U \to ExtStrCat (u) = ExtStrCat (U)$
7	6	adantl	$⊢ (φ \land u = U) \to ExtStrCat (u) = ExtStrCat (U)$
8		ineq1	$⊢ u = U \to u \cap Ring = U \cap Ring$
9	8	sqxpeqd	$⊢ u = U \to (u \cap Ring) \times (u \cap Ring) = (U \cap Ring) \times (U \cap Ring)$
10	3	sqxpeqd	$⊢ φ \to B \times B = (U \cap Ring) \times (U \cap Ring)$
11	10	eqcomd	$⊢ φ \to (U \cap Ring) \times (U \cap Ring) = B \times B$
12	9 11	sylan9eqr	$⊢ (φ \land u = U) \to (u \cap Ring) \times (u \cap Ring) = B \times B$
13	12	reseq2d	$⊢ (φ \land u = U) \to {RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))} = {RingHom ↾}_{(B \times B)}$
14	4	eqcomd	$⊢ φ \to {RingHom ↾}_{(B \times B)} = H$
15	14	adantr	$⊢ (φ \land u = U) \to {RingHom ↾}_{(B \times B)} = H$
16	13 15	eqtrd	$⊢ (φ \land u = U) \to {RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))} = H$
17	7 16	oveq12d	$⊢ (φ \land u = U) \to ExtStrCat (u) ↾_{cat} ({RingHom ↾}_{((u \cap Ring) \times (u \cap Ring))}) = ExtStrCat (U) ↾_{cat} H$
18	2	elexd	$⊢ φ \to U \in V$
19		ovexd	$⊢ φ \to ExtStrCat (U) ↾_{cat} H \in V$
20	5 17 18 19	fvmptd2	$⊢ φ \to RingCat (U) = ExtStrCat (U) ↾_{cat} H$
21	1 20	eqtrid	$⊢ φ \to C = ExtStrCat (U) ↾_{cat} H$

Metamath Proof Explorer