Metamath Proof Explorer

Theorem cofuoppf

Description: Composition of opposite functors. (Contributed by Zhi Wang, 26-Nov-2025)

Ref Expression
Hypotheses cofuoppf.k 
|- ( ph -> ( G o.func F ) = K )
cofuoppf.f 
|- ( ph -> F e. ( C Func D ) )
cofuoppf.g 
|- ( ph -> G e. ( D Func E ) )
Assertion cofuoppf 
|- ( ph -> ( ( oppFunc ` G ) o.func ( oppFunc ` F ) ) = ( oppFunc ` K ) )

Proof

Step Hyp Ref Expression
1 cofuoppf.k 
 |-  ( ph -> ( G o.func F ) = K )
2 cofuoppf.f 
 |-  ( ph -> F e. ( C Func D ) )
3 cofuoppf.g 
 |-  ( ph -> G e. ( D Func E ) )
4 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 4 5 oppcbas 
 |-  ( Base ` C ) = ( Base ` ( oppCat ` C ) )
7 eqid 
 |-  ( oppCat ` D ) = ( oppCat ` D )
8 2 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
9 4 7 8 funcoppc 
 |-  ( ph -> ( 1st ` F ) ( ( oppCat ` C ) Func ( oppCat ` D ) ) tpos ( 2nd ` F ) )
10 eqid 
 |-  ( oppCat ` E ) = ( oppCat ` E )
11 3 func1st2nd 
 |-  ( ph -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
12 7 10 11 funcoppc 
 |-  ( ph -> ( 1st ` G ) ( ( oppCat ` D ) Func ( oppCat ` E ) ) tpos ( 2nd ` G ) )
13 6 9 12 cofuval2 
 |-  ( ph -> ( <. ( 1st ` G ) , tpos ( 2nd ` G ) >. o.func <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) ) >. )
14 oppfval2 
 |-  ( G e. ( D Func E ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. )
15 3 14 syl 
 |-  ( ph -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. )
16 oppfval2 
 |-  ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
17 2 16 syl 
 |-  ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
18 15 17 oveq12d 
 |-  ( ph -> ( ( oppFunc ` G ) o.func ( oppFunc ` F ) ) = ( <. ( 1st ` G ) , tpos ( 2nd ` G ) >. o.func <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) )
19 5 2 3 cofuval 
 |-  ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
20 1 19 eqtr3d 
 |-  ( ph -> K = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
21 2 3 cofucl 
 |-  ( ph -> ( G o.func F ) e. ( C Func E ) )
22 1 21 eqeltrrd 
 |-  ( ph -> K e. ( C Func E ) )
23 20 22 oppfval3 
 |-  ( ph -> ( oppFunc ` K ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , tpos ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
24 ovtpos 
 |-  ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) = ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) )
25 ovtpos 
 |-  ( y tpos ( 2nd ` F ) x ) = ( x ( 2nd ` F ) y )
26 24 25 coeq12i 
 |-  ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) )
27 26 eqcomi 
 |-  ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) = ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) )
28 27 a1i 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) = ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) )
29 28 mpoeq3ia 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) )
30 29 tposmpo 
 |-  tpos ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) )
31 30 opeq2i 
 |-  <. ( ( 1st ` G ) o. ( 1st ` F ) ) , tpos ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) ) >.
32 23 31 eqtrdi 
 |-  ( ph -> ( oppFunc ` K ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) ) >. )
33 13 18 32 3eqtr4d 
 |-  ( ph -> ( ( oppFunc ` G ) o.func ( oppFunc ` F ) ) = ( oppFunc ` K ) )