Theorem fuco22natlem1

Description: Lemma for fuco22nat . The commutative square of natural transformation A in category D , mapped to category E by the morphism part L of the functor. (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fuco22natlem1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
	fuco22natlem1.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
	fuco22natlem1.a	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
	fuco22natlem1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
	fuco22natlem1.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
Assertion	fuco22natlem1	⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco22natlem1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
2		fuco22natlem1.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
3		fuco22natlem1.a	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
4		fuco22natlem1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
5		fuco22natlem1.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
6		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
7		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
10	6 3 7 8 9 1 2 4	nati	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝑀 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) )
11	10	fveq2d	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝑀 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) ) )
12		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
13		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
14		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
15	6 3	natrcl2	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
16	7 12 15	funcf1	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
17	16 1	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
18	16 2	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
19	6 3	natrcl3	⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
20	7 12 19	funcf1	⊢ ( 𝜑 → 𝑀 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
21	20 2	ffvelcdmd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
22	7 8 13 15 1 2	funcf2	⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
23	22 4	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ∈ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
24	6 3 7 13 2	natcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) ∈ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) )
25	12 13 9 14 5 17 18 21 23 24	funcco	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
26	20 1	ffvelcdmd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
27	6 3 7 13 1	natcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑋 ) ) )
28	7 8 13 19 1 2	funcf2	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ⟶ ( ( 𝑀 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) )
29	28 4	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ∈ ( ( 𝑀 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) )
30	12 13 9 14 5 17 26 21 27 29	funcco	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝑀 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
31	11 25 30	3eqtr3d	⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )