ringccofvalALTV

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

	Ref	Expression
Hypotheses	ringcbasALTV.c	$⊢ C = RingCatALTV (U)$
	ringcbasALTV.b	$⊢ B = {Base}_{C}$
	ringcbasALTV.u	$⊢ φ \to U \in V$
	ringccoALTV.o	$⊢ \underset{˙}{\cdot} = comp (C)$
Assertion	ringccofvalALTV	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))$

Proof

Step	Hyp	Ref	Expression
1		ringcbasALTV.c	$⊢ C = RingCatALTV (U)$
2		ringcbasALTV.b	$⊢ B = {Base}_{C}$
3		ringcbasALTV.u	$⊢ φ \to U \in V$
4		ringccoALTV.o	$⊢ \underset{˙}{\cdot} = comp (C)$
5	1 2 3	ringcbasALTV	$⊢ φ \to B = U \cap Ring$
6		eqid	$⊢ Hom (C) = Hom (C)$
7	1 2 3 6	ringchomfvalALTV	$⊢ φ \to Hom (C) = (x \in B, y \in B ⟼ x RingHom y)$
8		eqidd	$⊢ φ \to (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f)) = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))$
9	1 3 5 7 8	ringcvalALTV	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\}$
18	15 16 17	strfv	$⊢ (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f)) \in V \to (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))⟩\})$
19	14 18	ax-mp	$⊢ (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RingHom z), f \in (1^{st} (v) RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f))$

Metamath Proof Explorer

Theorem ringccofvalALTV

Proof