ringccoALTV

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)$
	ringccoALTV.x	$⊢ φ \to X \in B$
	ringccoALTV.y	$⊢ φ \to Y \in B$
	ringccoALTV.z	$⊢ φ \to Z \in B$
	ringccoALTV.f	$⊢ φ \to F \in (X RingHom Y)$
	ringccoALTV.g	$⊢ φ \to G \in (Y RingHom Z)$
Assertion	ringccoALTV	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = 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		ringccoALTV.x	$⊢ φ \to X \in B$
6		ringccoALTV.y	$⊢ φ \to Y \in B$
7		ringccoALTV.z	$⊢ φ \to Z \in B$
8		ringccoALTV.f	$⊢ φ \to F \in (X RingHom Y)$
9		ringccoALTV.g	$⊢ φ \to G \in (Y RingHom Z)$
10	1 2 3 4	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))$
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) RingHom z = Y RingHom 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) RingHom 2^{nd} (v) = X RingHom 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) RingHom z), f \in (1^{st} (v) RingHom 2^{nd} (v)) ⟼ g \circ f) = (g \in (Y RingHom Z), f \in (X RingHom 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 RingHom Z \in V$
30		ovex	$⊢ X RingHom Y \in V$
31	29 30	mpoex	$⊢ (g \in (Y RingHom Z), f \in (X RingHom Y) ⟼ g \circ f) \in V$
32	31	a1i	$⊢ φ \to (g \in (Y RingHom Z), f \in (X RingHom Y) ⟼ g \circ f) \in V$
33	10 26 28 7 32	ovmpod	$⊢ φ \to ⟨X, Y⟩ \underset{˙}{\cdot} Z = (g \in (Y RingHom Z), f \in (X RingHom 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 RingHom Z) \land F \in (X RingHom 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 ringccoALTV

Proof