rngcval

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

Step	Hyp	Ref	Expression
1		rngcval.c	$⊢ C = RngCat (U)$
2		rngcval.u	$⊢ φ \to U \in V$
3		rngcval.b	$⊢ φ \to B = U \cap Rng$
4		rngcval.h	$⊢ φ \to H = {RngHomo ↾}_{(B \times B)}$
5		df-rngc	$⊢ RngCat = (u \in V ⟼ ExtStrCat (u) ↾_{cat} ({RngHomo ↾}_{((u \cap Rng) \times (u \cap Rng))}))$
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 Rng = U \cap Rng$
9	8	sqxpeqd	$⊢ u = U \to (u \cap Rng) \times (u \cap Rng) = (U \cap Rng) \times (U \cap Rng)$
10	3	sqxpeqd	$⊢ φ \to B \times B = (U \cap Rng) \times (U \cap Rng)$
11	10	eqcomd	$⊢ φ \to (U \cap Rng) \times (U \cap Rng) = B \times B$
12	9 11	sylan9eqr	$⊢ (φ \land u = U) \to (u \cap Rng) \times (u \cap Rng) = B \times B$
13	12	reseq2d	$⊢ (φ \land u = U) \to {RngHomo ↾}_{((u \cap Rng) \times (u \cap Rng))} = {RngHomo ↾}_{(B \times B)}$
14	4	eqcomd	$⊢ φ \to {RngHomo ↾}_{(B \times B)} = H$
15	14	adantr	$⊢ (φ \land u = U) \to {RngHomo ↾}_{(B \times B)} = H$
16	13 15	eqtrd	$⊢ (φ \land u = U) \to {RngHomo ↾}_{((u \cap Rng) \times (u \cap Rng))} = H$
17	7 16	oveq12d	$⊢ (φ \land u = U) \to ExtStrCat (u) ↾_{cat} ({RngHomo ↾}_{((u \cap Rng) \times (u \cap Rng))}) = 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 RngCat (U) = ExtStrCat (U) ↾_{cat} H$
21	1 20	syl5eq	$⊢ φ \to C = ExtStrCat (U) ↾_{cat} H$

Metamath Proof Explorer