upciclem2

	Ref	Expression
Hypotheses	upcic.b	$⊢ B = {Base}_{D}$
	upcic.c	$⊢ C = {Base}_{E}$
	upcic.h	$⊢ H = Hom (D)$
	upcic.j	$⊢ J = Hom (E)$
	upcic.o	$⊢ O = comp (E)$
	upcic.f	$⊢ φ \to F (D Func E) G$
	upcic.x	$⊢ φ \to X \in B$
	upcic.y	$⊢ φ \to Y \in B$
	upciclem2.z	$⊢ φ \to Z \in B$
	upciclem2.w	$⊢ φ \to W \in C$
	upciclem2.m	$⊢ φ \to M \in (W J F (X))$
	upciclem2.od	$⊢ \underset{˙}{\cdot} = comp (D)$
	upciclem2.k	$⊢ φ \to K \in (X H Y)$
	upciclem2.l	$⊢ φ \to L \in (Y H Z)$
	upciclem2.nm	$⊢ φ \to N = (X G Y) (K) (⟨W, F (X)⟩ O F (Y)) M$
Assertion	upciclem2	$⊢ φ \to (X G Z) (L (⟨X, Y⟩ \underset{˙}{\cdot} Z) K) (⟨W, F (X)⟩ O F (Z)) M = (Y G Z) (L) (⟨W, F (Y)⟩ O F (Z)) N$

Proof

Step	Hyp	Ref	Expression
1		upcic.b	$⊢ B = {Base}_{D}$
2		upcic.c	$⊢ C = {Base}_{E}$
3		upcic.h	$⊢ H = Hom (D)$
4		upcic.j	$⊢ J = Hom (E)$
5		upcic.o	$⊢ O = comp (E)$
6		upcic.f	$⊢ φ \to F (D Func E) G$
7		upcic.x	$⊢ φ \to X \in B$
8		upcic.y	$⊢ φ \to Y \in B$
9		upciclem2.z	$⊢ φ \to Z \in B$
10		upciclem2.w	$⊢ φ \to W \in C$
11		upciclem2.m	$⊢ φ \to M \in (W J F (X))$
12		upciclem2.od	$⊢ \underset{˙}{\cdot} = comp (D)$
13		upciclem2.k	$⊢ φ \to K \in (X H Y)$
14		upciclem2.l	$⊢ φ \to L \in (Y H Z)$
15		upciclem2.nm	$⊢ φ \to N = (X G Y) (K) (⟨W, F (X)⟩ O F (Y)) M$
16	6	funcrcl3	$⊢ φ \to E \in Cat$
17	1 2 6	funcf1	$⊢ φ \to F : B ⟶ C$
18	17 7	ffvelcdmd	$⊢ φ \to F (X) \in C$
19	17 8	ffvelcdmd	$⊢ φ \to F (Y) \in C$
20	1 3 4 6 7 8	funcf2	$⊢ φ \to (X G Y) : X H Y ⟶ F (X) J F (Y)$
21	20 13	ffvelcdmd	$⊢ φ \to (X G Y) (K) \in (F (X) J F (Y))$
22	17 9	ffvelcdmd	$⊢ φ \to F (Z) \in C$
23	1 3 4 6 8 9	funcf2	$⊢ φ \to (Y G Z) : Y H Z ⟶ F (Y) J F (Z)$
24	23 14	ffvelcdmd	$⊢ φ \to (Y G Z) (L) \in (F (Y) J F (Z))$
25	2 4 5 16 10 18 19 11 21 22 24	catass	$⊢ φ \to ((Y G Z) (L) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (K)) (⟨W, F (X)⟩ O F (Z)) M = (Y G Z) (L) (⟨W, F (Y)⟩ O F (Z)) ((X G Y) (K) (⟨W, F (X)⟩ O F (Y)) M)$
26	1 3 12 5 6 7 8 9 13 14	funcco	$⊢ φ \to (X G Z) (L (⟨X, Y⟩ \underset{˙}{\cdot} Z) K) = (Y G Z) (L) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (K)$
27	26	oveq1d	$⊢ φ \to (X G Z) (L (⟨X, Y⟩ \underset{˙}{\cdot} Z) K) (⟨W, F (X)⟩ O F (Z)) M = ((Y G Z) (L) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (K)) (⟨W, F (X)⟩ O F (Z)) M$
28	15	oveq2d	$⊢ φ \to (Y G Z) (L) (⟨W, F (Y)⟩ O F (Z)) N = (Y G Z) (L) (⟨W, F (Y)⟩ O F (Z)) ((X G Y) (K) (⟨W, F (X)⟩ O F (Y)) M)$
29	25 27 28	3eqtr4d	$⊢ φ \to (X G Z) (L (⟨X, Y⟩ \underset{˙}{\cdot} Z) K) (⟨W, F (X)⟩ O F (Z)) M = (Y G Z) (L) (⟨W, F (Y)⟩ O F (Z)) N$

Metamath Proof Explorer

Theorem upciclem2

Proof