Metamath Proof Explorer

Theorem fuco22natlem3

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

Ref Expression
Hypotheses fuco22natlem1.x 
|- ( ph -> X e. ( Base ` C ) )
fuco22natlem1.y 
|- ( ph -> Y e. ( Base ` C ) )
fuco22natlem1.a 
|- ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
fuco22natlem1.h 
|- ( ph -> H e. ( X ( Hom ` C ) Y ) )
fuco22natlem2.b 
|- ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
fuco22natlem3.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fuco22natlem3.u 
|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
fuco22natlem3.v 
|- ( ph -> V = <. <. R , S >. , <. M , N >. >. )
Assertion fuco22natlem3 
|- ( ph -> ( ( ( B ( U P V ) A ) ` Y ) ( <. ( ( K o. F ) ` X ) , ( ( K o. F ) ` Y ) >. ( comp ` E ) ( ( R o. M ) ` Y ) ) ( ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) ` H ) ) = ( ( ( ( ( M ` X ) S ( M ` Y ) ) o. ( X N Y ) ) ` H ) ( <. ( ( K o. F ) ` X ) , ( ( R o. M ) ` X ) >. ( comp ` E ) ( ( R o. M ) ` Y ) ) ( ( B ( U P V ) A ) ` X ) ) )

Proof

Step Hyp Ref Expression
1 fuco22natlem1.x 
 |-  ( ph -> X e. ( Base ` C ) )
2 fuco22natlem1.y 
 |-  ( ph -> Y e. ( Base ` C ) )
3 fuco22natlem1.a 
 |-  ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
4 fuco22natlem1.h 
 |-  ( ph -> H e. ( X ( Hom ` C ) Y ) )
5 fuco22natlem2.b 
 |-  ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
6 fuco22natlem3.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
7 fuco22natlem3.u 
 |-  ( ph -> U = <. <. K , L >. , <. F , G >. >. )
8 fuco22natlem3.v 
 |-  ( ph -> V = <. <. R , S >. , <. M , N >. >. )
9 1 2 3 4 5 fuco22natlem2 
 |-  ( ph -> ( ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` Y ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` Y ) L ( M ` Y ) ) ` ( A ` Y ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( F ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` H ) ) ) = ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) ) )
10 eqid 
 |-  ( Base ` C ) = ( Base ` C )
11 eqid 
 |-  ( Base ` D ) = ( Base ` D )
12 eqid 
 |-  ( C Nat D ) = ( C Nat D )
13 12 3 natrcl2 
 |-  ( ph -> F ( C Func D ) G )
14 10 11 13 funcf1 
 |-  ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
15 14 1 fvco3d 
 |-  ( ph -> ( ( K o. F ) ` X ) = ( K ` ( F ` X ) ) )
16 14 2 fvco3d 
 |-  ( ph -> ( ( K o. F ) ` Y ) = ( K ` ( F ` Y ) ) )
17 15 16 opeq12d 
 |-  ( ph -> <. ( ( K o. F ) ` X ) , ( ( K o. F ) ` Y ) >. = <. ( K ` ( F ` X ) ) , ( K ` ( F ` Y ) ) >. )
18 12 3 natrcl3 
 |-  ( ph -> M ( C Func D ) N )
19 10 11 18 funcf1 
 |-  ( ph -> M : ( Base ` C ) --> ( Base ` D ) )
20 19 2 fvco3d 
 |-  ( ph -> ( ( R o. M ) ` Y ) = ( R ` ( M ` Y ) ) )
21 17 20 oveq12d 
 |-  ( ph -> ( <. ( ( K o. F ) ` X ) , ( ( K o. F ) ` Y ) >. ( comp ` E ) ( ( R o. M ) ` Y ) ) = ( <. ( K ` ( F ` X ) ) , ( K ` ( F ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) )
22 eqidd 
 |-  ( ph -> ( <. ( K ` ( F ` Y ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) = ( <. ( K ` ( F ` Y ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) )
23 6 7 8 3 5 2 22 fuco23 
 |-  ( ph -> ( ( B ( U P V ) A ) ` Y ) = ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` Y ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` Y ) L ( M ` Y ) ) ` ( A ` Y ) ) ) )
24 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
25 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
26 10 24 25 13 1 2 funcf2 
 |-  ( ph -> ( X G Y ) : ( X ( Hom ` C ) Y ) --> ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) )
27 26 4 fvco3d 
 |-  ( ph -> ( ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) ` H ) = ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` H ) ) )
28 21 23 27 oveq123d 
 |-  ( ph -> ( ( ( B ( U P V ) A ) ` Y ) ( <. ( ( K o. F ) ` X ) , ( ( K o. F ) ` Y ) >. ( comp ` E ) ( ( R o. M ) ` Y ) ) ( ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) ` H ) ) = ( ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` Y ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` Y ) L ( M ` Y ) ) ` ( A ` Y ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( F ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` H ) ) ) )
29 19 1 fvco3d 
 |-  ( ph -> ( ( R o. M ) ` X ) = ( R ` ( M ` X ) ) )
30 15 29 opeq12d 
 |-  ( ph -> <. ( ( K o. F ) ` X ) , ( ( R o. M ) ` X ) >. = <. ( K ` ( F ` X ) ) , ( R ` ( M ` X ) ) >. )
31 30 20 oveq12d 
 |-  ( ph -> ( <. ( ( K o. F ) ` X ) , ( ( R o. M ) ` X ) >. ( comp ` E ) ( ( R o. M ) ` Y ) ) = ( <. ( K ` ( F ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) )
32 10 24 25 18 1 2 funcf2 
 |-  ( ph -> ( X N Y ) : ( X ( Hom ` C ) Y ) --> ( ( M ` X ) ( Hom ` D ) ( M ` Y ) ) )
33 32 4 fvco3d 
 |-  ( ph -> ( ( ( ( M ` X ) S ( M ` Y ) ) o. ( X N Y ) ) ` H ) = ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) )
34 eqidd 
 |-  ( ph -> ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) = ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) )
35 6 7 8 3 5 1 34 fuco23 
 |-  ( ph -> ( ( B ( U P V ) A ) ` X ) = ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) )
36 31 33 35 oveq123d 
 |-  ( ph -> ( ( ( ( ( M ` X ) S ( M ` Y ) ) o. ( X N Y ) ) ` H ) ( <. ( ( K o. F ) ` X ) , ( ( R o. M ) ` X ) >. ( comp ` E ) ( ( R o. M ) ` Y ) ) ( ( B ( U P V ) A ) ` X ) ) = ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) ) )
37 9 28 36 3eqtr4d 
 |-  ( ph -> ( ( ( B ( U P V ) A ) ` Y ) ( <. ( ( K o. F ) ` X ) , ( ( K o. F ) ` Y ) >. ( comp ` E ) ( ( R o. M ) ` Y ) ) ( ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) ` H ) ) = ( ( ( ( ( M ` X ) S ( M ` Y ) ) o. ( X N Y ) ) ` H ) ( <. ( ( K o. F ) ` X ) , ( ( R o. M ) ` X ) >. ( comp ` E ) ( ( R o. M ) ` Y ) ) ( ( B ( U P V ) A ) ` X ) ) )