rngcvalALTV

Description: Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020)

	Ref	Expression
Hypotheses	rngcvalALTV.c	$⊢ C = RngCatALTV (U)$
	rngcvalALTV.u	$⊢ φ \to U \in V$
	rngcvalALTV.b	$⊢ φ \to B = U \cap Rng$
	rngcvalALTV.h	$⊢ φ \to H = (x \in B, y \in B ⟼ x RngHom y)$
	rngcvalALTV.o	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))$
Assertion	rngcvalALTV	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		rngcvalALTV.c	$⊢ C = RngCatALTV (U)$
2		rngcvalALTV.u	$⊢ φ \to U \in V$
3		rngcvalALTV.b	$⊢ φ \to B = U \cap Rng$
4		rngcvalALTV.h	$⊢ φ \to H = (x \in B, y \in B ⟼ x RngHom y)$
5		rngcvalALTV.o	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))$
6		df-rngcALTV	$⊢ RngCatALTV = (u \in V ⟼ ⦋ (u \cap Rng) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RngHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))⟩\})$
7	6	a1i	$⊢ φ \to RngCatALTV = (u \in V ⟼ ⦋ (u \cap Rng) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RngHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))⟩\})$
8		vex	$⊢ u \in V$
9	8	inex1	$⊢ u \cap Rng \in V$
10	9	a1i	$⊢ (φ \land u = U) \to u \cap Rng \in V$
11		ineq1	$⊢ u = U \to u \cap Rng = U \cap Rng$
12	11	adantl	$⊢ (φ \land u = U) \to u \cap Rng = U \cap Rng$
13	3	adantr	$⊢ (φ \land u = U) \to B = U \cap Rng$
14	12 13	eqtr4d	$⊢ (φ \land u = U) \to u \cap Rng = B$
15		simpr	$⊢ ((φ \land u = U) \land b = B) \to b = B$
16	15	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨{Base}_{ndx}, b⟩ = ⟨{Base}_{ndx}, B⟩$
17		eqidd	$⊢ ((φ \land u = U) \land b = B) \to x RngHom y = x RngHom y$
18	15 15 17	mpoeq123dv	$⊢ ((φ \land u = U) \land b = B) \to (x \in b, y \in b ⟼ x RngHom y) = (x \in B, y \in B ⟼ x RngHom y)$
19	4	ad2antrr	$⊢ ((φ \land u = U) \land b = B) \to H = (x \in B, y \in B ⟼ x RngHom y)$
20	18 19	eqtr4d	$⊢ ((φ \land u = U) \land b = B) \to (x \in b, y \in b ⟼ x RngHom y) = H$
21	20	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨Hom (ndx), (x \in b, y \in b ⟼ x RngHom y)⟩ = ⟨Hom (ndx), H⟩$
22	15	sqxpeqd	$⊢ ((φ \land u = U) \land b = B) \to b \times b = B \times B$
23		eqidd	$⊢ ((φ \land u = U) \land b = B) \to (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f) = (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f)$
24	22 15 23	mpoeq123dv	$⊢ ((φ \land u = U) \land b = B) \to (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f)) = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))$
25	5	ad2antrr	$⊢ ((φ \land u = U) \land b = B) \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))$
26	24 25	eqtr4d	$⊢ ((φ \land u = U) \land b = B) \to (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f)) = \underset{˙}{\cdot}$
27	26	opeq2d	$⊢ ((φ \land u = U) \land b = B) \to ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))⟩ = ⟨comp (ndx), \underset{˙}{\cdot}⟩$
28	16 21 27	tpeq123d	$⊢ ((φ \land u = U) \land b = B) \to \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RngHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
29	10 14 28	csbied2	$⊢ (φ \land u = U) \to ⦋ (u \cap Rng) / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), (x \in b, y \in b ⟼ x RngHom y)⟩, ⟨comp (ndx), (v \in (b \times b), z \in b ⟼ (g \in (2^{nd} (v) RngHom z), f \in (1^{st} (v) RngHom 2^{nd} (v)) ⟼ g \circ f))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
30		elex	$⊢ U \in V \to U \in V$
31	2 30	syl	$⊢ φ \to U \in V$
32		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
33	32	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
34	7 29 31 33	fvmptd	$⊢ φ \to RngCatALTV (U) = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
35	1 34	eqtrid	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Metamath Proof Explorer

Theorem rngcvalALTV

Proof