rngccofvalALTV

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

	Ref	Expression
Hypotheses	rngcbasALTV.c	$⊢ C = RngCatALTV (U)$
	rngcbasALTV.b	$⊢ B = {Base}_{C}$
	rngcbasALTV.u	$⊢ φ \to U \in V$
	rngccofvalALTV.o	$⊢ \underset{˙}{\cdot} = comp (C)$
Assertion	rngccofvalALTV	$⊢ φ \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))$

Proof

Step	Hyp	Ref	Expression
1		rngcbasALTV.c	$⊢ C = RngCatALTV (U)$
2		rngcbasALTV.b	$⊢ B = {Base}_{C}$
3		rngcbasALTV.u	$⊢ φ \to U \in V$
4		rngccofvalALTV.o	$⊢ \underset{˙}{\cdot} = comp (C)$
5	1 2 3	rngcbasALTV	$⊢ φ \to B = U \cap Rng$
6		eqid	$⊢ Hom (C) = Hom (C)$
7	1 2 3 6	rngchomfvalALTV	$⊢ φ \to Hom (C) = (x \in B, y \in B ⟼ x RngHom y)$
8		eqidd	$⊢ φ \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))$
9	1 3 5 7 8	rngcvalALTV	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨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))⟩\}$
10	9	fveq2d	$⊢ φ \to comp (C) = comp (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨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))⟩\})$
11	2	fvexi	$⊢ B \in V$
12		sqxpexg	$⊢ B \in V \to B \times B \in V$
13	11 12	ax-mp	$⊢ B \times B \in V$
14	13 11	mpoex	$⊢ (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)) \in V$
15		catstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨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))⟩\} Struct ⟨1, 15⟩$
16		ccoid	$⊢ comp = Slot comp (ndx)$
17		snsstp3	$⊢ \{⟨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))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨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))⟩\}$
18	15 16 17	strfv	$⊢ (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)) \in V \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)) = comp (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨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))⟩\})$
19	14 18	ax-mp	$⊢ (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 (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨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))⟩\})$
20	10 4 19	3eqtr4g	$⊢ φ \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))$

Metamath Proof Explorer

Theorem rngccofvalALTV

Proof