estrcco

Description: Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020)

	Ref	Expression
Hypotheses	estrcbas.c	$⊢ C = ExtStrCat (U)$
	estrcbas.u	$⊢ φ \to U \in V$
	estrcco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	estrcco.x	$⊢ φ \to X \in U$
	estrcco.y	$⊢ φ \to Y \in U$
	estrcco.z	$⊢ φ \to Z \in U$
	estrcco.a	$⊢ A = {Base}_{X}$
	estrcco.b	$⊢ B = {Base}_{Y}$
	estrcco.d	$⊢ D = {Base}_{Z}$
	estrcco.f	$⊢ φ \to F : A ⟶ B$
	estrcco.g	$⊢ φ \to G : B ⟶ D$
Assertion	estrcco	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G \circ F$

Proof

Step	Hyp	Ref	Expression
1		estrcbas.c	$⊢ C = ExtStrCat (U)$
2		estrcbas.u	$⊢ φ \to U \in V$
3		estrcco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		estrcco.x	$⊢ φ \to X \in U$
5		estrcco.y	$⊢ φ \to Y \in U$
6		estrcco.z	$⊢ φ \to Z \in U$
7		estrcco.a	$⊢ A = {Base}_{X}$
8		estrcco.b	$⊢ B = {Base}_{Y}$
9		estrcco.d	$⊢ D = {Base}_{Z}$
10		estrcco.f	$⊢ φ \to F : A ⟶ B$
11		estrcco.g	$⊢ φ \to G : B ⟶ D$
12	1 2 3	estrccofval	$⊢ φ \to \underset{˙}{\cdot} = (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))$
13		fveq2	$⊢ z = Z \to {Base}_{z} = {Base}_{Z}$
14	13	adantl	$⊢ (v = ⟨X, Y⟩ \land z = Z) \to {Base}_{z} = {Base}_{Z}$
15	14	adantl	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to {Base}_{z} = {Base}_{Z}$
16		simprl	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to v = ⟨X, Y⟩$
17	16	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) = 2^{nd} (⟨X, Y⟩)$
18		op2ndg	$⊢ (X \in U \land Y \in U) \to 2^{nd} (⟨X, Y⟩) = Y$
19	4 5 18	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
20	19	adantr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (⟨X, Y⟩) = Y$
21	17 20	eqtrd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) = Y$
22	21	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to {Base}_{2^{nd} (v)} = {Base}_{Y}$
23	15 22	oveq12d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to {Base}_{z}^{{Base}_{2^{nd} (v)}} = {Base}_{Z}^{{Base}_{Y}}$
24	16	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (v) = 1^{st} (⟨X, Y⟩)$
25	24	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to {Base}_{1^{st} (v)} = {Base}_{1^{st} (⟨X, Y⟩)}$
26		op1stg	$⊢ (X \in U \land Y \in U) \to 1^{st} (⟨X, Y⟩) = X$
27	4 5 26	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
28	27	fveq2d	$⊢ φ \to {Base}_{1^{st} (⟨X, Y⟩)} = {Base}_{X}$
29	28	adantr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to {Base}_{1^{st} (⟨X, Y⟩)} = {Base}_{X}$
30	25 29	eqtrd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to {Base}_{1^{st} (v)} = {Base}_{X}$
31	22 30	oveq12d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to {Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}} = {Base}_{Y}^{{Base}_{X}}$
32		eqidd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to g \circ f = g \circ f$
33	23 31 32	mpoeq123dv	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f) = (g \in ({Base}_{Z}^{{Base}_{Y}}), f \in ({Base}_{Y}^{{Base}_{X}}) ⟼ g \circ f)$
34	4 5	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (U \times U)$
35		ovex	$⊢ {Base}_{Z}^{{Base}_{Y}} \in V$
36		ovex	$⊢ {Base}_{Y}^{{Base}_{X}} \in V$
37	35 36	mpoex	$⊢ (g \in ({Base}_{Z}^{{Base}_{Y}}), f \in ({Base}_{Y}^{{Base}_{X}}) ⟼ g \circ f) \in V$
38	37	a1i	$⊢ φ \to (g \in ({Base}_{Z}^{{Base}_{Y}}), f \in ({Base}_{Y}^{{Base}_{X}}) ⟼ g \circ f) \in V$
39	12 33 34 6 38	ovmpod	$⊢ φ \to ⟨X, Y⟩ \underset{˙}{\cdot} Z = (g \in ({Base}_{Z}^{{Base}_{Y}}), f \in ({Base}_{Y}^{{Base}_{X}}) ⟼ g \circ f)$
40		simpl	$⊢ (g = G \land f = F) \to g = G$
41		simpr	$⊢ (g = G \land f = F) \to f = F$
42	40 41	coeq12d	$⊢ (g = G \land f = F) \to g \circ f = G \circ F$
43	42	adantl	$⊢ (φ \land (g = G \land f = F)) \to g \circ f = G \circ F$
44	8	a1i	$⊢ φ \to B = {Base}_{Y}$
45	44	eqcomd	$⊢ φ \to {Base}_{Y} = B$
46	9	a1i	$⊢ φ \to D = {Base}_{Z}$
47	46	eqcomd	$⊢ φ \to {Base}_{Z} = D$
48	45 47	feq23d	$⊢ φ \to (G : {Base}_{Y} ⟶ {Base}_{Z} \leftrightarrow G : B ⟶ D)$
49	11 48	mpbird	$⊢ φ \to G : {Base}_{Y} ⟶ {Base}_{Z}$
50		fvexd	$⊢ φ \to {Base}_{Z} \in V$
51		fvexd	$⊢ φ \to {Base}_{Y} \in V$
52	50 51	elmapd	$⊢ φ \to (G \in ({Base}_{Z}^{{Base}_{Y}}) \leftrightarrow G : {Base}_{Y} ⟶ {Base}_{Z})$
53	49 52	mpbird	$⊢ φ \to G \in ({Base}_{Z}^{{Base}_{Y}})$
54	7	a1i	$⊢ φ \to A = {Base}_{X}$
55	54	eqcomd	$⊢ φ \to {Base}_{X} = A$
56	55 45	feq23d	$⊢ φ \to (F : {Base}_{X} ⟶ {Base}_{Y} \leftrightarrow F : A ⟶ B)$
57	10 56	mpbird	$⊢ φ \to F : {Base}_{X} ⟶ {Base}_{Y}$
58		fvexd	$⊢ φ \to {Base}_{X} \in V$
59	51 58	elmapd	$⊢ φ \to (F \in ({Base}_{Y}^{{Base}_{X}}) \leftrightarrow F : {Base}_{X} ⟶ {Base}_{Y})$
60	57 59	mpbird	$⊢ φ \to F \in ({Base}_{Y}^{{Base}_{X}})$
61		coexg	$⊢ (G \in ({Base}_{Z}^{{Base}_{Y}}) \land F \in ({Base}_{Y}^{{Base}_{X}})) \to G \circ F \in V$
62	53 60 61	syl2anc	$⊢ φ \to G \circ F \in V$
63	39 43 53 60 62	ovmpod	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G \circ F$

Metamath Proof Explorer

Theorem estrcco

Proof