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

Metamath Proof Explorer

Theorem fucorid

Proof