Theorem fuco22natlem1 48909

Description: Lemma for fuco22nat 48913. The commutative square of natural transformation 𝐴 in category 𝐷, mapped to category 𝐸 by the morphism part 𝐿 of the functor. (Contributed by Zhi Wang, 30-Sep-2025.)

Hypotheses

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

Assertion

Ref	Expression
fuco22natlem1	⊢ (𝜑 → ((((𝐹‘𝑌)𝐿(𝑀‘𝑌))‘(𝐴‘𝑌))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝐹‘𝑌))⟩(comp‘𝐸)(𝐾‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝐹‘𝑌))‘((𝑋𝐺𝑌)‘𝐻))) = ((((𝑀‘𝑋)𝐿(𝑀‘𝑌))‘((𝑋𝑁𝑌)‘𝐻))(⟨(𝐾‘(𝐹‘𝑋)), (𝐾‘(𝑀‘𝑋))⟩(comp‘𝐸)(𝐾‘(𝑀‘𝑌)))(((𝐹‘𝑋)𝐿(𝑀‘𝑋))‘(𝐴‘𝑋))))

Proof of Theorem fuco22natlem1

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ⟨cop 4640   class class class wbr 5151  ‘cfv 6569  (class class class)co 7438  Basecbs 17254  Hom chom 17318  compcco 17319   Func cfunc 17914   Nat cnat 18005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5288  ax-sep 5305  ax-nul 5315  ax-pow 5374  ax-pr 5441  ax-un 7761

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3483  df-sbc 3795  df-csb 3912  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4916  df-iun 5001  df-br 5152  df-opab 5214  df-mpt 5235  df-id 5587  df-xp 5699  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-res 5705  df-ima 5706  df-iota 6522  df-fun 6571  df-fn 6572  df-f 6573  df-f1 6574  df-fo 6575  df-f1o 6576  df-fv 6577  df-ov 7441  df-oprab 7442  df-mpo 7443  df-1st 8022  df-2nd 8023  df-map 8876  df-ixp 8946  df-func 17918  df-nat 18007

This theorem is referenced by:  fuco22natlem2  48910