Theorem comfeqval

Description: Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	comfeqval.b	$$⊢B={\mathrm{Base}}_C$$
	comfeqval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	comfeqval.1	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	comfeqval.2	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(D\right)$$
	comfeqval.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	comfeqval.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	comfeqval.x	$$⊢\phi \to X\in B$$
	comfeqval.y	$$⊢\phi \to Y\in B$$
	comfeqval.z	$$⊢\phi \to Z\in B$$
	comfeqval.f	$$⊢\phi \to F\in \left(XHY\right)$$
	comfeqval.g	$$⊢\phi \to G\in \left(YHZ\right)$$
Assertion	comfeqval	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=G\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)F$$

Proof

Step	Hyp	Ref	Expression
1		comfeqval.b	$$⊢B={\mathrm{Base}}_C$$
2		comfeqval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		comfeqval.1	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
4		comfeqval.2	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(D\right)$$
5		comfeqval.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
6		comfeqval.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
7		comfeqval.x	$$⊢\phi \to X\in B$$
8		comfeqval.y	$$⊢\phi \to Y\in B$$
9		comfeqval.z	$$⊢\phi \to Z\in B$$
10		comfeqval.f	$$⊢\phi \to F\in \left(XHY\right)$$
11		comfeqval.g	$$⊢\phi \to G\in \left(YHZ\right)$$
12	6	oveqd	$$⊢\phi \to ⟨X,Y⟩{\mathrm{comp}}_{𝑓}\left(C\right)Z=⟨X,Y⟩{\mathrm{comp}}_{𝑓}\left(D\right)Z$$
13	12	oveqd	$$⊢\phi \to G\left(⟨X,Y⟩{\mathrm{comp}}_{𝑓}\left(C\right)Z\right)F=G\left(⟨X,Y⟩{\mathrm{comp}}_{𝑓}\left(D\right)Z\right)F$$
14		eqid	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(C\right)$$
15	14 1 2 3 7 8 9 10 11	comfval	$$⊢\phi \to G\left(⟨X,Y⟩{\mathrm{comp}}_{𝑓}\left(C\right)Z\right)F=G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$
16		eqid	$$⊢{\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
17		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
18		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
19	5	homfeqbas	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_D$$
20	1 19	syl5eq	$$⊢\phi \to B={\mathrm{Base}}_D$$
21	7 20	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
22	8 20	eleqtrd	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
23	9 20	eleqtrd	$$⊢\phi \to Z\in {\mathrm{Base}}_D$$
24	1 2 18 5 7 8	homfeqval	$$⊢\phi \to XHY=X\mathrm{Hom}\left(D\right)Y$$
25	10 24	eleqtrd	$$⊢\phi \to F\in \left(X\mathrm{Hom}\left(D\right)Y\right)$$
26	1 2 18 5 8 9	homfeqval	$$⊢\phi \to YHZ=Y\mathrm{Hom}\left(D\right)Z$$
27	11 26	eleqtrd	$$⊢\phi \to G\in \left(Y\mathrm{Hom}\left(D\right)Z\right)$$
28	16 17 18 4 21 22 23 25 27	comfval	$$⊢\phi \to G\left(⟨X,Y⟩{\mathrm{comp}}_{𝑓}\left(D\right)Z\right)F=G\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)F$$
29	13 15 28	3eqtr3d	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=G\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)F$$