Metamath Proof Explorer

Theorem fuco22natlem3

Description: Combine fuco22natlem2 with fuco23 . (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fuco22natlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
fuco22natlem1.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
fuco22natlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
fuco22natlem1.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
fuco22natlem2.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
fuco22natlem3.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
fuco22natlem3.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
fuco22natlem3.v ⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
Assertion fuco22natlem3 ( 𝜑 → ( ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑌 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) ) ( ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∘ ( 𝑋 𝐺 𝑌 ) ) ‘ 𝐻 ) ) = ( ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ∘ ( 𝑋 𝑁 𝑌 ) ) ‘ 𝐻 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) ) ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 fuco22natlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
2 fuco22natlem1.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
3 fuco22natlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
4 fuco22natlem1.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
5 fuco22natlem2.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
6 fuco22natlem3.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
7 fuco22natlem3.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
8 fuco22natlem3.v ⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
9 1 2 3 4 5 fuco22natlem2 ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) )
10 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
11 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
12 eqid ⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
13 12 3 natrcl2 ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
14 10 11 13 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
15 14 1 fvco3d ⊢ ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) )
16 14 2 fvco3d ⊢ ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑌 ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) )
17 15 16 opeq12d ⊢ ( 𝜑 → ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑌 ) ⟩ = ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ )
18 12 3 natrcl3 ⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
19 10 11 18 funcf1 ⊢ ( 𝜑 → 𝑀 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
20 19 2 fvco3d ⊢ ( 𝜑 → ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) = ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) )
21 17 20 oveq12d ⊢ ( 𝜑 → ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
22 eqidd ⊢ ( 𝜑 → ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
23 6 7 8 3 5 2 22 fuco23 ⊢ ( 𝜑 → ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑌 ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ) )
24 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
25 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
26 10 24 25 13 1 2 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
27 26 4 fvco3d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∘ ( 𝑋 𝐺 𝑌 ) ) ‘ 𝐻 ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
28 21 23 27 oveq123d ⊢ ( 𝜑 → ( ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑌 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) ) ( ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∘ ( 𝑋 𝐺 𝑌 ) ) ‘ 𝐻 ) ) = ( ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
29 19 1 fvco3d ⊢ ( 𝜑 → ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑋 ) = ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) )
30 15 29 opeq12d ⊢ ( 𝜑 → ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑋 ) ⟩ = ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ )
31 30 20 oveq12d ⊢ ( 𝜑 → ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
32 10 24 25 18 1 2 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ⟶ ( ( 𝑀 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) )
33 32 4 fvco3d ⊢ ( 𝜑 → ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ∘ ( 𝑋 𝑁 𝑌 ) ) ‘ 𝐻 ) = ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) )
34 eqidd ⊢ ( 𝜑 → ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
35 6 7 8 3 5 1 34 fuco23 ⊢ ( 𝜑 → ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑋 ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
36 31 33 35 oveq123d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ∘ ( 𝑋 𝑁 𝑌 ) ) ‘ 𝐻 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) ) ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑋 ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) )
37 9 28 36 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑌 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) ) ( ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∘ ( 𝑋 𝐺 𝑌 ) ) ‘ 𝐻 ) ) = ( ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ∘ ( 𝑋 𝑁 𝑌 ) ) ‘ 𝐻 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑌 ) ) ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑋 ) ) )