fucorid

Description: Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor, in maps-to notation. (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	fucolid.p	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) = 𝑃 )
	fucolid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
	fucorid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucorid.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐷 Nat 𝐸 ) 𝐻 ) )
	fucorid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	fucorid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐹 ⟩ 𝑃 ⟨ 𝐻 , 𝐹 ⟩ ) ( 𝐼 ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucolid.p	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) = 𝑃 )
2		fucolid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
3		fucorid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
4		fucorid.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐷 Nat 𝐸 ) 𝐻 ) )
5		fucorid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
6		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
7	3 2 6 5	fucid	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐹 ) = ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) )
8	7	oveq2d	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐹 ⟩ 𝑃 ⟨ 𝐻 , 𝐹 ⟩ ) ( 𝐼 ‘ 𝐹 ) ) = ( 𝐴 ( ⟨ 𝐺 , 𝐹 ⟩ 𝑃 ⟨ 𝐻 , 𝐹 ⟩ ) ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ) )
9	5	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
10	9	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
11		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
12	11 4	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
13	11 12	natrcl2	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
14	13	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
15	13	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
16		eqidd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) )
17	10 14 15 16	fucoelvv	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ∈ ( V × V ) )
18		1st2nd2	⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ∈ ( V × V ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟩ )
19	17 18	syl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟩ )
20	1	opeq2d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟩ = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , 𝑃 ⟩ )
21	19 20	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , 𝑃 ⟩ )
22		eqidd	⊢ ( 𝜑 → ⟨ 𝐺 , 𝐹 ⟩ = ⟨ 𝐺 , 𝐹 ⟩ )
23		eqidd	⊢ ( 𝜑 → ⟨ 𝐻 , 𝐹 ⟩ = ⟨ 𝐻 , 𝐹 ⟩ )
24		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
25	3 24 6 5	fucidcl	⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝐹 ) )
26	21 22 23 25 4	fuco22a	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐹 ⟩ 𝑃 ⟨ 𝐻 , 𝐹 ⟩ ) ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) ) )
27		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
28		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
29	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
30	27 28 29	funcf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
32	30 31	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
33	32	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
34		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
35	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
36	30 31	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
37	28 6 34 35 36	funcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
38	33 37	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
39	38	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) = ( ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
40		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
41		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
42	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
43	28 40 35	funcf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
44	43 36	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
45		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
46	11 12	natrcl3	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐻 ) )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐻 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐻 ) )
48	28 40 47	funcf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐻 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
49	48 36	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
50	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
51	11 50 28 41 36	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
52	40 41 34 42 44 45 49 51	catrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) = ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
53	39 52	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) = ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
54	53	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
55	8 26 54	3eqtrd	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐺 , 𝐹 ⟩ 𝑃 ⟨ 𝐻 , 𝐹 ⟩ ) ( 𝐼 ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝐴 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem fucorid

Proof