Metamath Proof Explorer

Theorem ringchomfvalALTV

Description: Set of arrows of the category of rings (in a universe). (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$
		ringchomfvalALTV.h	$⊢ H = Hom (C)$
	Assertion	ringchomfvalALTV	$⊢ φ \to H = (x \in B, y \in B ⟼ x RingHom y)$

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		ringchomfvalALTV.h	$⊢ H = Hom (C)$
5	1 2 3	ringcbasALTV	$⊢ φ \to B = U \cap Ring$
6		eqidd	$⊢ φ \to (x \in B, y \in B ⟼ x RingHom y) = (x \in B, y \in B ⟼ x RingHom y)$
7		eqidd	$⊢ φ \to (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g)) = (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g))$
8	1 3 5 6 7	ringcvalALTV	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (x \in B, y \in B ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g))⟩\}$
9	8	fveq2d	$⊢ φ \to Hom (C) = Hom (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (x \in B, y \in B ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g))⟩\})$
10	4 9	syl5eq	$⊢ φ \to H = Hom (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (x \in B, y \in B ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g))⟩\})$
11	2	fvexi	$⊢ B \in V$
12	11 11	mpoex	$⊢ (x \in B, y \in B ⟼ x RingHom y) \in V$
13		catstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (x \in B, y \in B ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g))⟩\} Struct ⟨1, 15⟩$
14		homid	$⊢ Hom = Slot Hom (ndx)$
15		snsstp2	$⊢ \{⟨Hom (ndx), (x \in B, y \in B ⟼ x RingHom y)⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (x \in B, y \in B ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g))⟩\}$
16	13 14 15	strfv	$⊢ (x \in B, y \in B ⟼ x RingHom y) \in V \to (x \in B, y \in B ⟼ x RingHom y) = Hom (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (x \in B, y \in B ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g))⟩\})$
17	12 16	mp1i	$⊢ φ \to (x \in B, y \in B ⟼ x RingHom y) = Hom (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (x \in B, y \in B ⟼ x RingHom y)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (f \in (2^{nd} (v) RingHom z), g \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ f \circ g))⟩\})$
18	10 17	eqtr4d	$⊢ φ \to H = (x \in B, y \in B ⟼ x RingHom y)$