coaval

Description: Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homdmcoa.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
	homdmcoa.h	$⊢ H = {Hom}_{a} (C)$
	homdmcoa.f	$⊢ φ \to F \in (X H Y)$
	homdmcoa.g	$⊢ φ \to G \in (Y H Z)$
	coaval.x	$⊢ \underset{˙}{∙} = comp (C)$
Assertion	coaval	$⊢ φ \to G \underset{˙}{\cdot} F = ⟨X, Z, 2^{nd} (G) (⟨X, Y⟩ \underset{˙}{∙} Z) 2^{nd} (F)⟩$

Proof

Step	Hyp	Ref	Expression
1		homdmcoa.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
2		homdmcoa.h	$⊢ H = {Hom}_{a} (C)$
3		homdmcoa.f	$⊢ φ \to F \in (X H Y)$
4		homdmcoa.g	$⊢ φ \to G \in (Y H Z)$
5		coaval.x	$⊢ \underset{˙}{∙} = comp (C)$
6		eqid	$⊢ Arrow (C) = Arrow (C)$
7	1 6 5	coafval	$⊢ \underset{˙}{\cdot} = (g \in Arrow (C), f \in \{h \in Arrow (C) \| {cod}_{a} (h) = {dom}_{a} (g)\} ⟼ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ \underset{˙}{∙} {cod}_{a} (g)) 2^{nd} (f)⟩)$
8	6 2	homarw	$⊢ Y H Z \subseteq Arrow (C)$
9	8 4	sseldi	$⊢ φ \to G \in Arrow (C)$
10		fveqeq2	$⊢ h = F \to ({cod}_{a} (h) = {dom}_{a} (g) \leftrightarrow {cod}_{a} (F) = {dom}_{a} (g))$
11	6 2	homarw	$⊢ X H Y \subseteq Arrow (C)$
12	3	adantr	$⊢ (φ \land g = G) \to F \in (X H Y)$
13	11 12	sseldi	$⊢ (φ \land g = G) \to F \in Arrow (C)$
14	2	homacd	$⊢ F \in (X H Y) \to {cod}_{a} (F) = Y$
15	12 14	syl	$⊢ (φ \land g = G) \to {cod}_{a} (F) = Y$
16		simpr	$⊢ (φ \land g = G) \to g = G$
17	16	fveq2d	$⊢ (φ \land g = G) \to {dom}_{a} (g) = {dom}_{a} (G)$
18	4	adantr	$⊢ (φ \land g = G) \to G \in (Y H Z)$
19	2	homadm	$⊢ G \in (Y H Z) \to {dom}_{a} (G) = Y$
20	18 19	syl	$⊢ (φ \land g = G) \to {dom}_{a} (G) = Y$
21	17 20	eqtrd	$⊢ (φ \land g = G) \to {dom}_{a} (g) = Y$
22	15 21	eqtr4d	$⊢ (φ \land g = G) \to {cod}_{a} (F) = {dom}_{a} (g)$
23	10 13 22	elrabd	$⊢ (φ \land g = G) \to F \in \{h \in Arrow (C) \| {cod}_{a} (h) = {dom}_{a} (g)\}$
24		otex	$⊢ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ \underset{˙}{∙} {cod}_{a} (g)) 2^{nd} (f)⟩ \in V$
25	24	a1i	$⊢ (φ \land (g = G \land f = F)) \to ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ \underset{˙}{∙} {cod}_{a} (g)) 2^{nd} (f)⟩ \in V$
26		simprr	$⊢ (φ \land (g = G \land f = F)) \to f = F$
27	26	fveq2d	$⊢ (φ \land (g = G \land f = F)) \to {dom}_{a} (f) = {dom}_{a} (F)$
28	2	homadm	$⊢ F \in (X H Y) \to {dom}_{a} (F) = X$
29	12 28	syl	$⊢ (φ \land g = G) \to {dom}_{a} (F) = X$
30	29	adantrr	$⊢ (φ \land (g = G \land f = F)) \to {dom}_{a} (F) = X$
31	27 30	eqtrd	$⊢ (φ \land (g = G \land f = F)) \to {dom}_{a} (f) = X$
32	16	fveq2d	$⊢ (φ \land g = G) \to {cod}_{a} (g) = {cod}_{a} (G)$
33	2	homacd	$⊢ G \in (Y H Z) \to {cod}_{a} (G) = Z$
34	18 33	syl	$⊢ (φ \land g = G) \to {cod}_{a} (G) = Z$
35	32 34	eqtrd	$⊢ (φ \land g = G) \to {cod}_{a} (g) = Z$
36	35	adantrr	$⊢ (φ \land (g = G \land f = F)) \to {cod}_{a} (g) = Z$
37	21	adantrr	$⊢ (φ \land (g = G \land f = F)) \to {dom}_{a} (g) = Y$
38	31 37	opeq12d	$⊢ (φ \land (g = G \land f = F)) \to ⟨{dom}_{a} (f), {dom}_{a} (g)⟩ = ⟨X, Y⟩$
39	38 36	oveq12d	$⊢ (φ \land (g = G \land f = F)) \to ⟨{dom}_{a} (f), {dom}_{a} (g)⟩ \underset{˙}{∙} {cod}_{a} (g) = ⟨X, Y⟩ \underset{˙}{∙} Z$
40		simprl	$⊢ (φ \land (g = G \land f = F)) \to g = G$
41	40	fveq2d	$⊢ (φ \land (g = G \land f = F)) \to 2^{nd} (g) = 2^{nd} (G)$
42	26	fveq2d	$⊢ (φ \land (g = G \land f = F)) \to 2^{nd} (f) = 2^{nd} (F)$
43	39 41 42	oveq123d	$⊢ (φ \land (g = G \land f = F)) \to 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ \underset{˙}{∙} {cod}_{a} (g)) 2^{nd} (f) = 2^{nd} (G) (⟨X, Y⟩ \underset{˙}{∙} Z) 2^{nd} (F)$
44	31 36 43	oteq123d	$⊢ (φ \land (g = G \land f = F)) \to ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ \underset{˙}{∙} {cod}_{a} (g)) 2^{nd} (f)⟩ = ⟨X, Z, 2^{nd} (G) (⟨X, Y⟩ \underset{˙}{∙} Z) 2^{nd} (F)⟩$
45	9 23 25 44	ovmpodv2	$⊢ φ \to (\underset{˙}{\cdot} = (g \in Arrow (C), f \in \{h \in Arrow (C) \| {cod}_{a} (h) = {dom}_{a} (g)\} ⟼ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ \underset{˙}{∙} {cod}_{a} (g)) 2^{nd} (f)⟩) \to G \underset{˙}{\cdot} F = ⟨X, Z, 2^{nd} (G) (⟨X, Y⟩ \underset{˙}{∙} Z) 2^{nd} (F)⟩)$
46	7 45	mpi	$⊢ φ \to G \underset{˙}{\cdot} F = ⟨X, Z, 2^{nd} (G) (⟨X, Y⟩ \underset{˙}{∙} Z) 2^{nd} (F)⟩$

Metamath Proof Explorer

Theorem coaval

Proof