Metamath Proof Explorer

Theorem fucoaltvallem

Description: Lemma for fucoaltval . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

Ref Expression
Hypotheses fucoaltfunc.q 
|- Q = ( C FuncCat E )
fucoaltval.l 
|- L = ( <. C , C >. o.F E )
fucoaltval.c 
|- ( ph -> C e. Cat )
fucoaltval.e 
|- ( ph -> E e. Cat )
fucoaltval.k 
|- ( ph -> K e. ( Q Func Q ) )
fucoaltval.f 
|- ( ph -> F e. ( C Func E ) )
fucoaltval.g 
|- ( ph -> G e. ( C Func E ) )
fucoaltval.a 
|- ( ph -> A e. ( F ( C Nat E ) G ) )
fucoaltval.i 
|- I = ( idFunc ` C )
fucoaltval.j 
|- J = ( Id ` ( C FuncCat C ) )
fucoaltvallem.t 
|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
Assertion fucoaltvallem 
|- ( ph -> ( A ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ( J ` I ) ) = ( ( F ( 2nd ` K ) G ) ` A ) )

Proof

Step Hyp Ref Expression
1 fucoaltfunc.q 
 |-  Q = ( C FuncCat E )
2 fucoaltval.l 
 |-  L = ( <. C , C >. o.F E )
3 fucoaltval.c 
 |-  ( ph -> C e. Cat )
4 fucoaltval.e 
 |-  ( ph -> E e. Cat )
5 fucoaltval.k 
 |-  ( ph -> K e. ( Q Func Q ) )
6 fucoaltval.f 
 |-  ( ph -> F e. ( C Func E ) )
7 fucoaltval.g 
 |-  ( ph -> G e. ( C Func E ) )
8 fucoaltval.a 
 |-  ( ph -> A e. ( F ( C Nat E ) G ) )
9 fucoaltval.i 
 |-  I = ( idFunc ` C )
10 fucoaltval.j 
 |-  J = ( Id ` ( C FuncCat C ) )
11 fucoaltvallem.t 
 |-  T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
12 df-ov 
 |-  ( A ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ( J ` I ) ) = ( ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ` <. A , ( J ` I ) >. )
13 11 xpcfucbas 
 |-  ( ( C Func E ) X. ( C Func C ) ) = ( Base ` T )
14 11 1 3 3 4 fucofunca 
 |-  ( ph -> ( <. C , C >. o.F E ) e. ( T Func Q ) )
15 2 14 eqeltrid 
 |-  ( ph -> L e. ( T Func Q ) )
16 9 idfucl 
 |-  ( C e. Cat -> I e. ( C Func C ) )
17 3 16 syl 
 |-  ( ph -> I e. ( C Func C ) )
18 6 17 opelxpd 
 |-  ( ph -> <. F , I >. e. ( ( C Func E ) X. ( C Func C ) ) )
19 7 17 opelxpd 
 |-  ( ph -> <. G , I >. e. ( ( C Func E ) X. ( C Func C ) ) )
20 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
21 eqid 
 |-  ( C FuncCat C ) = ( C FuncCat C )
22 21 fucbas 
 |-  ( C Func C ) = ( Base ` ( C FuncCat C ) )
23 eqid 
 |-  ( C Nat C ) = ( C Nat C )
24 21 23 fuchom 
 |-  ( C Nat C ) = ( Hom ` ( C FuncCat C ) )
25 21 3 3 fuccat 
 |-  ( ph -> ( C FuncCat C ) e. Cat )
26 22 24 10 25 17 catidcl 
 |-  ( ph -> ( J ` I ) e. ( I ( C Nat C ) I ) )
27 8 26 opelxpd 
 |-  ( ph -> <. A , ( J ` I ) >. e. ( ( F ( C Nat E ) G ) X. ( I ( C Nat C ) I ) ) )
28 11 6 17 7 17 20 xpcfuchom2 
 |-  ( ph -> ( <. F , I >. ( Hom ` T ) <. G , I >. ) = ( ( F ( C Nat E ) G ) X. ( I ( C Nat C ) I ) ) )
29 27 28 eleqtrrd 
 |-  ( ph -> <. A , ( J ` I ) >. e. ( <. F , I >. ( Hom ` T ) <. G , I >. ) )
30 13 15 5 18 19 20 29 cofu2 
 |-  ( ph -> ( ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ` <. A , ( J ` I ) >. ) = ( ( ( ( 1st ` L ) ` <. F , I >. ) ( 2nd ` K ) ( ( 1st ` L ) ` <. G , I >. ) ) ` ( ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ` <. A , ( J ` I ) >. ) ) )
31 df-ov 
 |-  ( F ( 1st ` L ) I ) = ( ( 1st ` L ) ` <. F , I >. )
32 2 eqcomi 
 |-  ( <. C , C >. o.F E ) = L
33 32 fveq2i 
 |-  ( 1st ` ( <. C , C >. o.F E ) ) = ( 1st ` L )
34 33 a1i 
 |-  ( ph -> ( 1st ` ( <. C , C >. o.F E ) ) = ( 1st ` L ) )
35 34 17 6 fuco11b 
 |-  ( ph -> ( F ( 1st ` L ) I ) = ( F o.func I ) )
36 6 9 cofurid 
 |-  ( ph -> ( F o.func I ) = F )
37 35 36 eqtrd 
 |-  ( ph -> ( F ( 1st ` L ) I ) = F )
38 31 37 eqtr3id 
 |-  ( ph -> ( ( 1st ` L ) ` <. F , I >. ) = F )
39 df-ov 
 |-  ( G ( 1st ` L ) I ) = ( ( 1st ` L ) ` <. G , I >. )
40 34 17 7 fuco11b 
 |-  ( ph -> ( G ( 1st ` L ) I ) = ( G o.func I ) )
41 7 9 cofurid 
 |-  ( ph -> ( G o.func I ) = G )
42 40 41 eqtrd 
 |-  ( ph -> ( G ( 1st ` L ) I ) = G )
43 39 42 eqtr3id 
 |-  ( ph -> ( ( 1st ` L ) ` <. G , I >. ) = G )
44 38 43 oveq12d 
 |-  ( ph -> ( ( ( 1st ` L ) ` <. F , I >. ) ( 2nd ` K ) ( ( 1st ` L ) ` <. G , I >. ) ) = ( F ( 2nd ` K ) G ) )
45 df-ov 
 |-  ( A ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ( J ` I ) ) = ( ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ` <. A , ( J ` I ) >. )
46 32 fveq2i 
 |-  ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L )
47 46 a1i 
 |-  ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) )
48 47 21 10 9 3 8 fucoridid 
 |-  ( ph -> ( A ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ( J ` I ) ) = A )
49 45 48 eqtr3id 
 |-  ( ph -> ( ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ` <. A , ( J ` I ) >. ) = A )
50 44 49 fveq12d 
 |-  ( ph -> ( ( ( ( 1st ` L ) ` <. F , I >. ) ( 2nd ` K ) ( ( 1st ` L ) ` <. G , I >. ) ) ` ( ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ` <. A , ( J ` I ) >. ) ) = ( ( F ( 2nd ` K ) G ) ` A ) )
51 30 50 eqtrd 
 |-  ( ph -> ( ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ` <. A , ( J ` I ) >. ) = ( ( F ( 2nd ` K ) G ) ` A ) )
52 12 51 eqtrid 
 |-  ( ph -> ( A ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ( J ` I ) ) = ( ( F ( 2nd ` K ) G ) ` A ) )