evlfcllem

	Ref	Expression
Hypotheses	evlfcl.e	⊢ 𝐸 = ( 𝐶 eval_F 𝐷 )
	evlfcl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	evlfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	evlfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	evlfcl.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	evlfcl.f	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) )
	evlfcl.g	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
	evlfcl.h	⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) )
	evlfcl.a	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝐾 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) )
	evlfcl.b	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐺 𝑁 𝐻 ) ∧ 𝐿 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) ) )
Assertion	evlfcllem	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ( ⟨ 𝐵 , 𝐿 ⟩ ( ⟨ ⟨ 𝐹 , 𝑋 ⟩ , ⟨ 𝐺 , 𝑌 ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝐻 , 𝑍 ⟩ ) ⟨ 𝐴 , 𝐾 ⟩ ) ) = ( ( ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ⟨ 𝐵 , 𝐿 ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑌 ⟩ ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐻 , 𝑍 ⟩ ) ) ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlfcl.e	⊢ 𝐸 = ( 𝐶 eval_F 𝐷 )
2		evlfcl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
3		evlfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		evlfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		evlfcl.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
6		evlfcl.f	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) )
7		evlfcl.g	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
8		evlfcl.h	⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) )
9		evlfcl.a	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝐾 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) )
10		evlfcl.b	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐺 𝑁 𝐻 ) ∧ 𝐿 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) ) )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
14	6	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
15	8	simpld	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐶 Func 𝐷 ) )
16	6	simprd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
17	8	simprd	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
18		eqid	⊢ ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) = ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ )
19		eqid	⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
20	9	simpld	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
21	10	simpld	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐺 𝑁 𝐻 ) )
22	2 5 19 20 21	fuccocl	⊢ ( 𝜑 → ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) ∈ ( 𝐹 𝑁 𝐻 ) )
23		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
24	7	simprd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
25	9	simprd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
26	10	simprd	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
27	11 12 23 3 16 24 17 25 26	catcocl	⊢ ( 𝜑 → ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) )
28	1 3 4 11 12 13 5 14 15 16 17 18 22 27	evlf2val	⊢ ( 𝜑 → ( ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) = ( ( ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) ) )
29	2 5 11 13 19 20 21 17	fuccoval	⊢ ( 𝜑 → ( ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) ‘ 𝑍 ) = ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) )
30	29	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) ) )
31		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
32		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
33	31 14 32	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
34	11 12 23 13 33 16 24 17 25 26	funcco	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) = ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )
35	34	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ) )
36	5 20	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
37	5 36 11 12 13 24 17 26	nati	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ) = ( ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑌 ) ) )
38	37	oveq2d	⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝐴 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ) ) = ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑌 ) ) ) )
39		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
40		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
41	11 39 33	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
42	41 24	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
43	41 17	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) )
44	7	simpld	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
45		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
46	31 44 45	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
47	11 39 46	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
48	47 17	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) )
49	11 12 40 33 24 17	funcf2	⊢ ( 𝜑 → ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) : ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
50	49 26	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
51	5 36 11 40 17	natcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) )
52		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐻 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐻 ) )
53	31 15 52	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐻 ) )
54	11 39 53	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
55	54 17	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) )
56	5 21	nat1st2nd	⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
57	5 56 11 40 17	natcl	⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) )
58	39 40 13 4 42 43 48 50 51 55 57	catass	⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ) = ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝐴 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ) ) )
59	47 24	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
60	5 36 11 40 24	natcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) )
61	11 12 40 46 24 17	funcf2	⊢ ( 𝜑 → ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) : ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) )
62	61 26	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) )
63	39 40 13 4 42 59 48 60 62 55 57	catass	⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑌 ) ) = ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑌 ) ) ) )
64	38 58 63	3eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑌 ) ) )
65	64	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) = ( ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑌 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )
66	41 16	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
67	11 12 40 33 16 24	funcf2	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
68	67 25	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
69	39 40 13 4 43 48 55 51 57	catcocl	⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) )
70	39 40 13 4 66 42 43 68 50 55 69	catass	⊢ ( 𝜑 → ( ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ) )
71	39 40 13 4 59 48 55 62 57	catcocl	⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) )
72	39 40 13 4 66 42 59 68 60 55 71	catass	⊢ ( 𝜑 → ( ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑌 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ) )
73	65 70 72	3eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝐿 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ) )
74	35 73	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( 𝐴 ‘ 𝑍 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ) )
75	28 30 74	3eqtrd	⊢ ( 𝜑 → ( ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ) )
76		eqid	⊢ ( 𝑄 ×_c 𝐶 ) = ( 𝑄 ×_c 𝐶 )
77	2	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
78	2 5	fuchom	⊢ 𝑁 = ( Hom ‘ 𝑄 )
79		eqid	⊢ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) = ( comp ‘ ( 𝑄 ×_c 𝐶 ) )
80	76 77 11 78 12 14 16 44 24 19 23 79 15 17 20 25 21 26	xpcco2	⊢ ( 𝜑 → ( ⟨ 𝐵 , 𝐿 ⟩ ( ⟨ ⟨ 𝐹 , 𝑋 ⟩ , ⟨ 𝐺 , 𝑌 ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝐻 , 𝑍 ⟩ ) ⟨ 𝐴 , 𝐾 ⟩ ) = ⟨ ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) , ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ⟩ )
81	80	fveq2d	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ( ⟨ 𝐵 , 𝐿 ⟩ ( ⟨ ⟨ 𝐹 , 𝑋 ⟩ , ⟨ 𝐺 , 𝑌 ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝐻 , 𝑍 ⟩ ) ⟨ 𝐴 , 𝐾 ⟩ ) ) = ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ⟨ ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) , ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ⟩ ) )
82		df-ov	⊢ ( ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) = ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ⟨ ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) , ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ⟩ )
83	81 82	eqtr4di	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ( ⟨ 𝐵 , 𝐿 ⟩ ( ⟨ ⟨ 𝐹 , 𝑋 ⟩ , ⟨ 𝐺 , 𝑌 ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝐻 , 𝑍 ⟩ ) ⟨ 𝐴 , 𝐾 ⟩ ) ) = ( ( 𝐵 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐻 ) 𝐴 ) ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝐾 ) ) )
84		df-ov	⊢ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ )
85	1 3 4 11 14 16	evlf1	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
86	84 85	eqtr3id	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
87		df-ov	⊢ ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑌 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑌 ⟩ )
88	1 3 4 11 44 24	evlf1	⊢ ( 𝜑 → ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑌 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) )
89	87 88	eqtr3id	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑌 ⟩ ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) )
90	86 89	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑌 ⟩ ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ )
91		df-ov	⊢ ( 𝐻 ( 1^st ‘ 𝐸 ) 𝑍 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐻 , 𝑍 ⟩ )
92	1 3 4 11 15 17	evlf1	⊢ ( 𝜑 → ( 𝐻 ( 1^st ‘ 𝐸 ) 𝑍 ) = ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) )
93	91 92	eqtr3id	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐻 , 𝑍 ⟩ ) = ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) )
94	90 93	oveq12d	⊢ ( 𝜑 → ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑌 ⟩ ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐻 , 𝑍 ⟩ ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) )
95		df-ov	⊢ ( 𝐵 ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) 𝐿 ) = ( ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ⟨ 𝐵 , 𝐿 ⟩ )
96		eqid	⊢ ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) = ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ )
97	1 3 4 11 12 13 5 44 15 24 17 96 21 26	evlf2val	⊢ ( 𝜑 → ( 𝐵 ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) 𝐿 ) = ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) )
98	95 97	eqtr3id	⊢ ( 𝜑 → ( ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ⟨ 𝐵 , 𝐿 ⟩ ) = ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) )
99		df-ov	⊢ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ ) 𝐾 ) = ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ )
100		eqid	⊢ ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ ) = ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ )
101	1 3 4 11 12 13 5 14 44 16 24 100 20 25	evlf2val	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ ) 𝐾 ) = ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )
102	99 101	eqtr3id	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) )
103	94 98 102	oveq123d	⊢ ( 𝜑 → ( ( ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ⟨ 𝐵 , 𝐿 ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑌 ⟩ ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐻 , 𝑍 ⟩ ) ) ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) = ( ( ( 𝐵 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝐿 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑍 ) ) ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) ) )
104	75 83 103	3eqtr4d	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ( ⟨ 𝐵 , 𝐿 ⟩ ( ⟨ ⟨ 𝐹 , 𝑋 ⟩ , ⟨ 𝐺 , 𝑌 ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝐻 , 𝑍 ⟩ ) ⟨ 𝐴 , 𝐾 ⟩ ) ) = ( ( ( ⟨ 𝐺 , 𝑌 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐻 , 𝑍 ⟩ ) ‘ ⟨ 𝐵 , 𝐿 ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑌 ⟩ ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐻 , 𝑍 ⟩ ) ) ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑌 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) )

Metamath Proof Explorer

Theorem evlfcllem

Proof