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

Metamath Proof Explorer

Theorem fucolid

Proof