rngccoALTV

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)$
	rngccoALTV.x	$⊢ φ \to X \in B$
	rngccoALTV.y	$⊢ φ \to Y \in B$
	rngccoALTV.z	$⊢ φ \to Z \in B$
	rngccoALTV.f	$⊢ φ \to F \in (X RngHomo Y)$
	rngccoALTV.g	$⊢ φ \to G \in (Y RngHomo Z)$
Assertion	rngccoALTV	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = 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		rngccoALTV.x	$⊢ φ \to X \in B$
6		rngccoALTV.y	$⊢ φ \to Y \in B$
7		rngccoALTV.z	$⊢ φ \to Z \in B$
8		rngccoALTV.f	$⊢ φ \to F \in (X RngHomo Y)$
9		rngccoALTV.g	$⊢ φ \to G \in (Y RngHomo Z)$
10	1 2 3 4	rngccofvalALTV	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) RngHomo z), f \in (1^{st} (v) RngHomo 2^{nd} (v)) ⟼ g \circ f))$
11		simprl	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to v = ⟨X, Y⟩$
12	11	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) = 2^{nd} (⟨X, Y⟩)$
13		op2ndg	$⊢ (X \in B \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
14	5 6 13	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
15	14	adantr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (⟨X, Y⟩) = Y$
16	12 15	eqtrd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) = Y$
17		simprr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to z = Z$
18	16 17	oveq12d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) RngHomo z = Y RngHomo Z$
19	11	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (v) = 1^{st} (⟨X, Y⟩)$
20		op1stg	$⊢ (X \in B \land Y \in B) \to 1^{st} (⟨X, Y⟩) = X$
21	5 6 20	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
22	21	adantr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (⟨X, Y⟩) = X$
23	19 22	eqtrd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (v) = X$
24	23 16	oveq12d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (v) RngHomo 2^{nd} (v) = X RngHomo Y$
25		eqidd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to g \circ f = g \circ f$
26	18 24 25	mpoeq123dv	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to (g \in (2^{nd} (v) RngHomo z), f \in (1^{st} (v) RngHomo 2^{nd} (v)) ⟼ g \circ f) = (g \in (Y RngHomo Z), f \in (X RngHomo Y) ⟼ g \circ f)$
27		opelxpi	$⊢ (X \in B \land Y \in B) \to ⟨X, Y⟩ \in (B \times B)$
28	5 6 27	syl2anc	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
29		ovex	$⊢ Y RngHomo Z \in V$
30		ovex	$⊢ X RngHomo Y \in V$
31	29 30	mpoex	$⊢ (g \in (Y RngHomo Z), f \in (X RngHomo Y) ⟼ g \circ f) \in V$
32	31	a1i	$⊢ φ \to (g \in (Y RngHomo Z), f \in (X RngHomo Y) ⟼ g \circ f) \in V$
33	10 26 28 7 32	ovmpod	$⊢ φ \to ⟨X, Y⟩ \underset{˙}{\cdot} Z = (g \in (Y RngHomo Z), f \in (X RngHomo Y) ⟼ g \circ f)$
34		simprl	$⊢ (φ \land (g = G \land f = F)) \to g = G$
35		simprr	$⊢ (φ \land (g = G \land f = F)) \to f = F$
36	34 35	coeq12d	$⊢ (φ \land (g = G \land f = F)) \to g \circ f = G \circ F$
37		coexg	$⊢ (G \in (Y RngHomo Z) \land F \in (X RngHomo Y)) \to G \circ F \in V$
38	9 8 37	syl2anc	$⊢ φ \to G \circ F \in V$
39	33 36 9 8 38	ovmpod	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G \circ F$

Metamath Proof Explorer

Theorem rngccoALTV

Proof