Theorem estrcco

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

	Ref	Expression
Hypotheses	estrcbas.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
	estrcbas.u	$$⊢\phi \to U\in V$$
	estrcco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	estrcco.x	$$⊢\phi \to X\in U$$
	estrcco.y	$$⊢\phi \to Y\in U$$
	estrcco.z	$$⊢\phi \to Z\in U$$
	estrcco.a	$$⊢A={\mathrm{Base}}_X$$
	estrcco.b	$$⊢B={\mathrm{Base}}_Y$$
	estrcco.d	$$⊢D={\mathrm{Base}}_Z$$
	estrcco.f	$$⊢\phi \to F:A⟶B$$
	estrcco.g	$$⊢\phi \to G:B⟶D$$
Assertion	estrcco	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=G\circ F$$

Proof

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