fucoco

Description: Composition in the source category is mapped to composition in the target. See also fucoco2 . (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fucoco.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) )
	fucoco.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) )
	fucoco.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
	fucoco.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
	fucoco.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fucoco.x	⊢ ( 𝜑 → 𝑋 = ⟨ 𝐹 , 𝐺 ⟩ )
	fucoco.y	⊢ ( 𝜑 → 𝑌 = ⟨ 𝐾 , 𝐿 ⟩ )
	fucoco.z	⊢ ( 𝜑 → 𝑍 = ⟨ 𝑀 , 𝑁 ⟩ )
	fucoco.a	⊢ ( 𝜑 → 𝐴 = ⟨ 𝑅 , 𝑆 ⟩ )
	fucoco.b	⊢ ( 𝜑 → 𝐵 = ⟨ 𝑈 , 𝑉 ⟩ )
	fucoco.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoco.oq	⊢ ∙ = ( comp ‘ 𝑄 )
	fucoco.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
	fucoco.ot	⊢ · = ( comp ‘ 𝑇 )
Assertion	fucoco	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoco.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) )
2		fucoco.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) )
3		fucoco.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
4		fucoco.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
5		fucoco.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
6		fucoco.x	⊢ ( 𝜑 → 𝑋 = ⟨ 𝐹 , 𝐺 ⟩ )
7		fucoco.y	⊢ ( 𝜑 → 𝑌 = ⟨ 𝐾 , 𝐿 ⟩ )
8		fucoco.z	⊢ ( 𝜑 → 𝑍 = ⟨ 𝑀 , 𝑁 ⟩ )
9		fucoco.a	⊢ ( 𝜑 → 𝐴 = ⟨ 𝑅 , 𝑆 ⟩ )
10		fucoco.b	⊢ ( 𝜑 → 𝐵 = ⟨ 𝑈 , 𝑉 ⟩ )
11		fucoco.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
12		fucoco.oq	⊢ ∙ = ( comp ‘ 𝑄 )
13		fucoco.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
14		fucoco.ot	⊢ · = ( comp ‘ 𝑇 )
15		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
16	15 4	nat1st2nd	⊢ ( 𝜑 → 𝑉 ∈ ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝑁 ) , ( 2^nd ‘ 𝑁 ) ⟩ ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝑉 ∈ ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝑁 ) , ( 2^nd ‘ 𝑁 ) ⟩ ) )
18		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
19	18 1	nat1st2nd	⊢ ( 𝜑 → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝑝 ∈ ( Base ‘ 𝐶 ) )
22		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
23	17 20 21 22	fuco23alem	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) = ( ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) )
24	23	oveq1d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) = ( ( ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) )
25	24	oveq2d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) )
26	1	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) )
27	2	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) )
28	3	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
29	4	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
30	18	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
31	1 30	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
32	31	simprd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
34	15	natrcl	⊢ ( 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
35	2 34	syl	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
36	35	simprd	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝐷 ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → 𝐿 ∈ ( 𝐶 Func 𝐷 ) )
38		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
39		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
40		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
41		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
42		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
43	41 32 42	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
45		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
46		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
47		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
48	46 36 47	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
49	45 38 48	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
50	49	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ∈ ( Base ‘ 𝐷 ) )
51	15	natrcl	⊢ ( 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
52	4 51	syl	⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
53	52	simprd	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐶 Func 𝐷 ) )
54		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
55	46 53 54	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
56	45 38 55	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
57	56	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ∈ ( Base ‘ 𝐷 ) )
58	38 39 40 44 50 57	funcf2	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) : ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟶ ( ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) )
59	15 17 45 39 21	natcl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑉 ‘ 𝑝 ) ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) )
60	58 59	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ∈ ( ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) )
61	18 20 38 40 50	natcl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) )
62	26 27 28 29 21 33 37 60 61	fucocolem1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) )
63	25 62	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) = ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) )
64	63	mpteq2dva	⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) ) = ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) ) )
65		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
66	1 2 3 4 5 6 7 8 9 10 13 14 65	fucocolem3	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) ) )
67	1 2 3 4 5 6 7 8 9 10 11 12	fucocolem4	⊢ ( 𝜑 → ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐴 ) ) = ( 𝑝 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ‘ ( 𝑉 ‘ 𝑝 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑝 ) ) ) ( ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑝 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑝 ) ) ‘ ( 𝑆 ‘ 𝑝 ) ) ) ) ) )
68	64 66 67	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem fucoco

Proof