fucolid

Description: Post-compose a natural transformation with an identity natural transformation. (Contributed by Zhi Wang, 11-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fucolid.p	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) = 𝑃 )
2		fucolid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
3		fucolid.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐸 )
4		fucolid.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) )
5		fucolid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
6		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
7	3 2 6 5	fucid	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐹 ) = ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ 𝐹 ) ) )
8	7	oveq1d	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝐹 ) ( ⟨ 𝐹 , 𝐺 ⟩ 𝑃 ⟨ 𝐹 , 𝐻 ⟩ ) 𝐴 ) = ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ 𝐹 ) ) ( ⟨ 𝐹 , 𝐺 ⟩ 𝑃 ⟨ 𝐹 , 𝐻 ⟩ ) 𝐴 ) )
9		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
10	9 4	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
11	9 10	natrcl2	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
12	11	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13	11	funcrcl3	⊢ ( 𝜑 → 𝐷 ∈ Cat )
14	5	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
15	14	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
16		eqidd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) )
17	12 13 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 4 25	fuco22a	⊢ ( 𝜑 → ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ 𝐹 ) ) ( ⟨ 𝐹 , 𝐺 ⟩ 𝑃 ⟨ 𝐹 , 𝐻 ⟩ ) 𝐴 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ) )
27		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
28		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
29	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
30	27 28 29	funcf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
31		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
32	9 10	natrcl3	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐻 ) )
33	31 27 32	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
34	33	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
35	30 34	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
36	35	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ ( ( 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 ‘ 𝐻 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) )
37		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
38	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
39	31 27 11	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
40	39	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
41	30 40	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
42		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
43	30 34	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
44		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
45	27 44 37 29 40 34	funcf2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) : ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
46	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
47		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
48	9 46 31 44 47	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
49	45 48	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
50	28 37 6 38 41 42 43 49	catlid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐸 ) ‘ ( ( 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 ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) )
51	36 50	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( Id ‘ 𝐸 ) ∘ ( 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 ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) )
52	51	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) )
53	8 26 52	3eqtrd	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝐹 ) ( ⟨ 𝐹 , 𝐺 ⟩ 𝑃 ⟨ 𝐹 , 𝐻 ⟩ ) 𝐴 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem fucolid

Proof