fucocolem3

Description: Lemma for fucoco . The composed natural transformations are mapped to composition of 4 natural transformations. (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	⊢ ( 𝜑 → 𝐵 = ⟨ 𝑈 , 𝑉 ⟩ )
	fucocolem2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
	fucocolem2.ot	⊢ · = ( comp ‘ 𝑇 )
	fucocolem2.od	⊢ ∗ = ( comp ‘ 𝐷 )
Assertion	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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) ) )

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		fucocolem2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
12		fucocolem2.ot	⊢ · = ( comp ‘ 𝑇 )
13		fucocolem2.od	⊢ ∗ = ( comp ‘ 𝐷 )
14	1 2 3 4 5 6 7 8 9 10 11 12 13	fucocolem2	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( 𝑥 ∈ ( 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 ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ) ) ) )
15		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
16		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
17		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
18		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
19		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
20	19	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
21	1 20	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
22	21	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
23		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐹 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
24	18 22 23	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
26		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
27		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
28		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
29	28	natrcl	⊢ ( 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
30	2 29	syl	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
31	30	simpld	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
32		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
33	27 31 32	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
34	26 15 33	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
35	34	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
36	30	simprd	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝐷 ) )
37		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
38	27 36 37	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
39	26 15 38	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
40	39	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
41	28	natrcl	⊢ ( 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
42	4 41	syl	⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
43	42	simprd	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐶 Func 𝐷 ) )
44		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
45	27 43 44	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
46	26 15 45	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
47	46	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
48	28 2	nat1st2nd	⊢ ( 𝜑 → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ) )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ) )
50		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
51	28 49 26 16 50	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) )
52	28 4	nat1st2nd	⊢ ( 𝜑 → 𝑉 ∈ ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝑁 ) , ( 2^nd ‘ 𝑁 ) ⟩ ) )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑉 ∈ ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝑁 ) , ( 2^nd ‘ 𝑁 ) ⟩ ) )
54	28 53 26 16 50	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑉 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
55	15 16 13 17 25 35 40 47 51 54	funcco	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) )
56	55	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 ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) )
57	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) )
58	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) )
59	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
60	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
61	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
62	43	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑁 ∈ ( 𝐶 Func 𝐷 ) )
63	19 1	nat1st2nd	⊢ ( 𝜑 → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) )
64	63	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) )
65		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
66	19 64 15 65 47	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑅 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) )
67	15 16 65 25 40 47	funcf2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) : ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) )
68	67 54	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( 𝑉 ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) )
69	57 58 59 60 50 61 62 66 68	fucocolem1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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 ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) )
70	56 69	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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 ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) )
71	70	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 ‘ 𝑁 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) ) )
72	14 71	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( 𝑥 ∈ ( 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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Theorem fucocolem3

Proof