evlfcllem

	Ref	Expression
Hypotheses	evlfcl.e	$⊢ E = C {eval}_{F} D$
	evlfcl.q	$⊢ Q = C FuncCat D$
	evlfcl.c	$⊢ φ \to C \in Cat$
	evlfcl.d	$⊢ φ \to D \in Cat$
	evlfcl.n	$⊢ N = C Nat D$
	evlfcl.f	$⊢ φ \to (F \in (C Func D) \land X \in {Base}_{C})$
	evlfcl.g	$⊢ φ \to (G \in (C Func D) \land Y \in {Base}_{C})$
	evlfcl.h	$⊢ φ \to (H \in (C Func D) \land Z \in {Base}_{C})$
	evlfcl.a	$⊢ φ \to (A \in (F N G) \land K \in (X Hom (C) Y))$
	evlfcl.b	$⊢ φ \to (B \in (G N H) \land L \in (Y Hom (C) Z))$
Assertion	evlfcllem	$⊢ φ \to (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩ (⟨⟨F, X⟩, ⟨G, Y⟩⟩ comp (Q \times_{c} C) ⟨H, Z⟩) ⟨A, K⟩) = (⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩) (⟨1^{st} (E) (⟨F, X⟩), 1^{st} (E) (⟨G, Y⟩)⟩ comp (D) 1^{st} (E) (⟨H, Z⟩)) (⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩) (⟨A, K⟩)$

Proof

Step	Hyp	Ref	Expression
1		evlfcl.e	$⊢ E = C {eval}_{F} D$
2		evlfcl.q	$⊢ Q = C FuncCat D$
3		evlfcl.c	$⊢ φ \to C \in Cat$
4		evlfcl.d	$⊢ φ \to D \in Cat$
5		evlfcl.n	$⊢ N = C Nat D$
6		evlfcl.f	$⊢ φ \to (F \in (C Func D) \land X \in {Base}_{C})$
7		evlfcl.g	$⊢ φ \to (G \in (C Func D) \land Y \in {Base}_{C})$
8		evlfcl.h	$⊢ φ \to (H \in (C Func D) \land Z \in {Base}_{C})$
9		evlfcl.a	$⊢ φ \to (A \in (F N G) \land K \in (X Hom (C) Y))$
10		evlfcl.b	$⊢ φ \to (B \in (G N H) \land L \in (Y Hom (C) Z))$
11		eqid	$⊢ {Base}_{C} = {Base}_{C}$
12		eqid	$⊢ Hom (C) = Hom (C)$
13		eqid	$⊢ comp (D) = comp (D)$
14	6	simpld	$⊢ φ \to F \in (C Func D)$
15	8	simpld	$⊢ φ \to H \in (C Func D)$
16	6	simprd	$⊢ φ \to X \in {Base}_{C}$
17	8	simprd	$⊢ φ \to Z \in {Base}_{C}$
18		eqid	$⊢ ⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩ = ⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩$
19		eqid	$⊢ comp (Q) = comp (Q)$
20	9	simpld	$⊢ φ \to A \in (F N G)$
21	10	simpld	$⊢ φ \to B \in (G N H)$
22	2 5 19 20 21	fuccocl	$⊢ φ \to B (⟨F, G⟩ comp (Q) H) A \in (F N H)$
23		eqid	$⊢ comp (C) = comp (C)$
24	7	simprd	$⊢ φ \to Y \in {Base}_{C}$
25	9	simprd	$⊢ φ \to K \in (X Hom (C) Y)$
26	10	simprd	$⊢ φ \to L \in (Y Hom (C) Z)$
27	11 12 23 3 16 24 17 25 26	catcocl	$⊢ φ \to L (⟨X, Y⟩ comp (C) Z) K \in (X Hom (C) Z)$
28	1 3 4 11 12 13 5 14 15 16 17 18 22 27	evlf2val	$⊢ φ \to (B (⟨F, G⟩ comp (Q) H) A) (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (L (⟨X, Y⟩ comp (C) Z) K) = (B (⟨F, G⟩ comp (Q) H) A) (Z) (⟨1^{st} (F) (X), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Z) (L (⟨X, Y⟩ comp (C) Z) K)$
29	2 5 11 13 19 20 21 17	fuccoval	$⊢ φ \to (B (⟨F, G⟩ comp (Q) H) A) (Z) = B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)$
30	29	oveq1d	$⊢ φ \to (B (⟨F, G⟩ comp (Q) H) A) (Z) (⟨1^{st} (F) (X), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Z) (L (⟨X, Y⟩ comp (C) Z) K) = (B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (X), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Z) (L (⟨X, Y⟩ comp (C) Z) K)$
31		relfunc	$⊢ Rel (C Func D)$
32		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
33	31 14 32	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
34	11 12 23 13 33 16 24 17 25 26	funcco	$⊢ φ \to (X 2^{nd} (F) Z) (L (⟨X, Y⟩ comp (C) Z) K) = (Y 2^{nd} (F) Z) (L) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (F) (Z)) (X 2^{nd} (F) Y) (K)$
35	34	oveq2d	$⊢ φ \to (B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (X), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Z) (L (⟨X, Y⟩ comp (C) Z) K) = (B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (X), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) ((Y 2^{nd} (F) Z) (L) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (F) (Z)) (X 2^{nd} (F) Y) (K))$
36	5 20	nat1st2nd	$⊢ φ \to A \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
37	5 36 11 12 13 24 17 26	nati	$⊢ φ \to A (Z) (⟨1^{st} (F) (Y), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (G) (Z)) (Y 2^{nd} (F) Z) (L) = (Y 2^{nd} (G) Z) (L) (⟨1^{st} (F) (Y), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (G) (Z)) A (Y)$
38	37	oveq2d	$⊢ φ \to B (Z) (⟨1^{st} (F) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (A (Z) (⟨1^{st} (F) (Y), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (G) (Z)) (Y 2^{nd} (F) Z) (L)) = B (Z) (⟨1^{st} (F) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) ((Y 2^{nd} (G) Z) (L) (⟨1^{st} (F) (Y), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (G) (Z)) A (Y))$
39		eqid	$⊢ {Base}_{D} = {Base}_{D}$
40		eqid	$⊢ Hom (D) = Hom (D)$
41	11 39 33	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
42	41 24	ffvelrnd	$⊢ φ \to 1^{st} (F) (Y) \in {Base}_{D}$
43	41 17	ffvelrnd	$⊢ φ \to 1^{st} (F) (Z) \in {Base}_{D}$
44	7	simpld	$⊢ φ \to G \in (C Func D)$
45		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
46	31 44 45	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
47	11 39 46	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
48	47 17	ffvelrnd	$⊢ φ \to 1^{st} (G) (Z) \in {Base}_{D}$
49	11 12 40 33 24 17	funcf2	$⊢ φ \to (Y 2^{nd} (F) Z) : Y Hom (C) Z ⟶ 1^{st} (F) (Y) Hom (D) 1^{st} (F) (Z)$
50	49 26	ffvelrnd	$⊢ φ \to (Y 2^{nd} (F) Z) (L) \in (1^{st} (F) (Y) Hom (D) 1^{st} (F) (Z))$
51	5 36 11 40 17	natcl	$⊢ φ \to A (Z) \in (1^{st} (F) (Z) Hom (D) 1^{st} (G) (Z))$
52		1st2ndbr	$⊢ (Rel (C Func D) \land H \in (C Func D)) \to 1^{st} (H) (C Func D) 2^{nd} (H)$
53	31 15 52	sylancr	$⊢ φ \to 1^{st} (H) (C Func D) 2^{nd} (H)$
54	11 39 53	funcf1	$⊢ φ \to 1^{st} (H) : {Base}_{C} ⟶ {Base}_{D}$
55	54 17	ffvelrnd	$⊢ φ \to 1^{st} (H) (Z) \in {Base}_{D}$
56	5 21	nat1st2nd	$⊢ φ \to B \in (⟨1^{st} (G), 2^{nd} (G)⟩ N ⟨1^{st} (H), 2^{nd} (H)⟩)$
57	5 56 11 40 17	natcl	$⊢ φ \to B (Z) \in (1^{st} (G) (Z) Hom (D) 1^{st} (H) (Z))$
58	39 40 13 4 42 43 48 50 51 55 57	catass	$⊢ φ \to (B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (Y), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (F) Z) (L) = B (Z) (⟨1^{st} (F) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (A (Z) (⟨1^{st} (F) (Y), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (G) (Z)) (Y 2^{nd} (F) Z) (L))$
59	47 24	ffvelrnd	$⊢ φ \to 1^{st} (G) (Y) \in {Base}_{D}$
60	5 36 11 40 24	natcl	$⊢ φ \to A (Y) \in (1^{st} (F) (Y) Hom (D) 1^{st} (G) (Y))$
61	11 12 40 46 24 17	funcf2	$⊢ φ \to (Y 2^{nd} (G) Z) : Y Hom (C) Z ⟶ 1^{st} (G) (Y) Hom (D) 1^{st} (G) (Z)$
62	61 26	ffvelrnd	$⊢ φ \to (Y 2^{nd} (G) Z) (L) \in (1^{st} (G) (Y) Hom (D) 1^{st} (G) (Z))$
63	39 40 13 4 42 59 48 60 62 55 57	catass	$⊢ φ \to (B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (Y), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) A (Y) = B (Z) (⟨1^{st} (F) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) ((Y 2^{nd} (G) Z) (L) (⟨1^{st} (F) (Y), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (G) (Z)) A (Y))$
64	38 58 63	3eqtr4d	$⊢ φ \to (B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (Y), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (F) Z) (L) = (B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (Y), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) A (Y)$
65	64	oveq1d	$⊢ φ \to ((B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (Y), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (F) Z) (L)) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Y) (K) = ((B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (Y), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) A (Y)) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Y) (K)$
66	41 16	ffvelrnd	$⊢ φ \to 1^{st} (F) (X) \in {Base}_{D}$
67	11 12 40 33 16 24	funcf2	$⊢ φ \to (X 2^{nd} (F) Y) : X Hom (C) Y ⟶ 1^{st} (F) (X) Hom (D) 1^{st} (F) (Y)$
68	67 25	ffvelrnd	$⊢ φ \to (X 2^{nd} (F) Y) (K) \in (1^{st} (F) (X) Hom (D) 1^{st} (F) (Y))$
69	39 40 13 4 43 48 55 51 57	catcocl	$⊢ φ \to B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z) \in (1^{st} (F) (Z) Hom (D) 1^{st} (H) (Z))$
70	39 40 13 4 66 42 43 68 50 55 69	catass	$⊢ φ \to ((B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (Y), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (F) Z) (L)) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Y) (K) = (B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (X), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) ((Y 2^{nd} (F) Z) (L) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (F) (Z)) (X 2^{nd} (F) Y) (K))$
71	39 40 13 4 59 48 55 62 57	catcocl	$⊢ φ \to B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L) \in (1^{st} (G) (Y) Hom (D) 1^{st} (H) (Z))$
72	39 40 13 4 66 42 59 68 60 55 71	catass	$⊢ φ \to ((B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (Y), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) A (Y)) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Y) (K) = (B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (X), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) (A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K))$
73	65 70 72	3eqtr3d	$⊢ φ \to (B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (X), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) ((Y 2^{nd} (F) Z) (L) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (F) (Z)) (X 2^{nd} (F) Y) (K)) = (B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (X), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) (A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K))$
74	35 73	eqtrd	$⊢ φ \to (B (Z) (⟨1^{st} (F) (Z), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) A (Z)) (⟨1^{st} (F) (X), 1^{st} (F) (Z)⟩ comp (D) 1^{st} (H) (Z)) (X 2^{nd} (F) Z) (L (⟨X, Y⟩ comp (C) Z) K) = (B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (X), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) (A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K))$
75	28 30 74	3eqtrd	$⊢ φ \to (B (⟨F, G⟩ comp (Q) H) A) (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (L (⟨X, Y⟩ comp (C) Z) K) = (B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (X), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) (A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K))$
76		eqid	$⊢ Q \times_{c} C = Q \times_{c} C$
77	2	fucbas	$⊢ C Func D = {Base}_{Q}$
78	2 5	fuchom	$⊢ N = Hom (Q)$
79		eqid	$⊢ comp (Q \times_{c} C) = comp (Q \times_{c} C)$
80	76 77 11 78 12 14 16 44 24 19 23 79 15 17 20 25 21 26	xpcco2	$⊢ φ \to ⟨B, L⟩ (⟨⟨F, X⟩, ⟨G, Y⟩⟩ comp (Q \times_{c} C) ⟨H, Z⟩) ⟨A, K⟩ = ⟨B (⟨F, G⟩ comp (Q) H) A, L (⟨X, Y⟩ comp (C) Z) K⟩$
81	80	fveq2d	$⊢ φ \to (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩ (⟨⟨F, X⟩, ⟨G, Y⟩⟩ comp (Q \times_{c} C) ⟨H, Z⟩) ⟨A, K⟩) = (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B (⟨F, G⟩ comp (Q) H) A, L (⟨X, Y⟩ comp (C) Z) K⟩)$
82		df-ov	$⊢ (B (⟨F, G⟩ comp (Q) H) A) (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (L (⟨X, Y⟩ comp (C) Z) K) = (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B (⟨F, G⟩ comp (Q) H) A, L (⟨X, Y⟩ comp (C) Z) K⟩)$
83	81 82	eqtr4di	$⊢ φ \to (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩ (⟨⟨F, X⟩, ⟨G, Y⟩⟩ comp (Q \times_{c} C) ⟨H, Z⟩) ⟨A, K⟩) = (B (⟨F, G⟩ comp (Q) H) A) (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (L (⟨X, Y⟩ comp (C) Z) K)$
84		df-ov	$⊢ F 1^{st} (E) X = 1^{st} (E) (⟨F, X⟩)$
85	1 3 4 11 14 16	evlf1	$⊢ φ \to F 1^{st} (E) X = 1^{st} (F) (X)$
86	84 85	eqtr3id	$⊢ φ \to 1^{st} (E) (⟨F, X⟩) = 1^{st} (F) (X)$
87		df-ov	$⊢ G 1^{st} (E) Y = 1^{st} (E) (⟨G, Y⟩)$
88	1 3 4 11 44 24	evlf1	$⊢ φ \to G 1^{st} (E) Y = 1^{st} (G) (Y)$
89	87 88	eqtr3id	$⊢ φ \to 1^{st} (E) (⟨G, Y⟩) = 1^{st} (G) (Y)$
90	86 89	opeq12d	$⊢ φ \to ⟨1^{st} (E) (⟨F, X⟩), 1^{st} (E) (⟨G, Y⟩)⟩ = ⟨1^{st} (F) (X), 1^{st} (G) (Y)⟩$
91		df-ov	$⊢ H 1^{st} (E) Z = 1^{st} (E) (⟨H, Z⟩)$
92	1 3 4 11 15 17	evlf1	$⊢ φ \to H 1^{st} (E) Z = 1^{st} (H) (Z)$
93	91 92	eqtr3id	$⊢ φ \to 1^{st} (E) (⟨H, Z⟩) = 1^{st} (H) (Z)$
94	90 93	oveq12d	$⊢ φ \to ⟨1^{st} (E) (⟨F, X⟩), 1^{st} (E) (⟨G, Y⟩)⟩ comp (D) 1^{st} (E) (⟨H, Z⟩) = ⟨1^{st} (F) (X), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)$
95		df-ov	$⊢ B (⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩) L = (⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩)$
96		eqid	$⊢ ⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩ = ⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩$
97	1 3 4 11 12 13 5 44 15 24 17 96 21 26	evlf2val	$⊢ φ \to B (⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩) L = B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)$
98	95 97	eqtr3id	$⊢ φ \to (⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩) = B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)$
99		df-ov	$⊢ A (⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩) K = (⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩) (⟨A, K⟩)$
100		eqid	$⊢ ⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩ = ⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩$
101	1 3 4 11 12 13 5 14 44 16 24 100 20 25	evlf2val	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩) K = A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K)$
102	99 101	eqtr3id	$⊢ φ \to (⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩) (⟨A, K⟩) = A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K)$
103	94 98 102	oveq123d	$⊢ φ \to (⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩) (⟨1^{st} (E) (⟨F, X⟩), 1^{st} (E) (⟨G, Y⟩)⟩ comp (D) 1^{st} (E) (⟨H, Z⟩)) (⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩) (⟨A, K⟩) = (B (Z) (⟨1^{st} (G) (Y), 1^{st} (G) (Z)⟩ comp (D) 1^{st} (H) (Z)) (Y 2^{nd} (G) Z) (L)) (⟨1^{st} (F) (X), 1^{st} (G) (Y)⟩ comp (D) 1^{st} (H) (Z)) (A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ comp (D) 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K))$
104	75 83 103	3eqtr4d	$⊢ φ \to (⟨F, X⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩ (⟨⟨F, X⟩, ⟨G, Y⟩⟩ comp (Q \times_{c} C) ⟨H, Z⟩) ⟨A, K⟩) = (⟨G, Y⟩ 2^{nd} (E) ⟨H, Z⟩) (⟨B, L⟩) (⟨1^{st} (E) (⟨F, X⟩), 1^{st} (E) (⟨G, Y⟩)⟩ comp (D) 1^{st} (E) (⟨H, Z⟩)) (⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩) (⟨A, K⟩)$

Metamath Proof Explorer

Theorem evlfcllem

Proof