Metamath Proof Explorer

Theorem rngchomfvalALTV

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

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