Metamath Proof Explorer

Theorem oppgoppcco

Description: The converted opposite monoid has the same composition as that of the opposite category. Example 3.6(2) of Adamek p. 25. (Contributed by Zhi Wang, 22-Sep-2025)

Ref Expression
Hypotheses mndtccat.c 
|- ( ph -> C = ( MndToCat ` M ) )
mndtccat.m 
|- ( ph -> M e. Mnd )
oppgoppchom.d 
|- ( ph -> D = ( MndToCat ` ( oppG ` M ) ) )
oppgoppchom.o 
|- O = ( oppCat ` C )
oppgoppchom.x 
|- ( ph -> X e. ( Base ` D ) )
oppgoppchom.y 
|- ( ph -> Y e. ( Base ` O ) )
oppgoppcco.o 
|- ( ph -> .x. = ( comp ` D ) )
oppgoppcco.x 
|- ( ph -> .xb = ( comp ` O ) )
Assertion oppgoppcco 
|- ( ph -> ( <. X , X >. .x. X ) = ( <. Y , Y >. .xb Y ) )

Proof

Step Hyp Ref Expression
1 mndtccat.c 
 |-  ( ph -> C = ( MndToCat ` M ) )
2 mndtccat.m 
 |-  ( ph -> M e. Mnd )
3 oppgoppchom.d 
 |-  ( ph -> D = ( MndToCat ` ( oppG ` M ) ) )
4 oppgoppchom.o 
 |-  O = ( oppCat ` C )
5 oppgoppchom.x 
 |-  ( ph -> X e. ( Base ` D ) )
6 oppgoppchom.y 
 |-  ( ph -> Y e. ( Base ` O ) )
7 oppgoppcco.o 
 |-  ( ph -> .x. = ( comp ` D ) )
8 oppgoppcco.x 
 |-  ( ph -> .xb = ( comp ` O ) )
9 eqid 
 |-  ( Base ` C ) = ( Base ` C )
10 4 9 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
11 10 eqcomi 
 |-  ( Base ` O ) = ( Base ` C )
12 11 a1i 
 |-  ( ph -> ( Base ` O ) = ( Base ` C ) )
13 eqidd 
 |-  ( ph -> ( comp ` C ) = ( comp ` C ) )
14 1 2 12 6 6 6 13 mndtcco 
 |-  ( ph -> ( <. Y , Y >. ( comp ` C ) Y ) = ( +g ` M ) )
15 14 tposeqd 
 |-  ( ph -> tpos ( <. Y , Y >. ( comp ` C ) Y ) = tpos ( +g ` M ) )
16 eqid 
 |-  ( comp ` C ) = ( comp ` C )
17 11 16 4 6 6 6 oppccofval 
 |-  ( ph -> ( <. Y , Y >. ( comp ` O ) Y ) = tpos ( <. Y , Y >. ( comp ` C ) Y ) )
18 eqid 
 |-  ( oppG ` M ) = ( oppG ` M )
19 18 oppgmnd 
 |-  ( M e. Mnd -> ( oppG ` M ) e. Mnd )
20 2 19 syl 
 |-  ( ph -> ( oppG ` M ) e. Mnd )
21 eqidd 
 |-  ( ph -> ( Base ` D ) = ( Base ` D ) )
22 3 20 21 5 5 5 7 mndtcco 
 |-  ( ph -> ( <. X , X >. .x. X ) = ( +g ` ( oppG ` M ) ) )
23 eqid 
 |-  ( +g ` M ) = ( +g ` M )
24 eqid 
 |-  ( +g ` ( oppG ` M ) ) = ( +g ` ( oppG ` M ) )
25 23 18 24 oppgplusfval 
 |-  ( +g ` ( oppG ` M ) ) = tpos ( +g ` M )
26 22 25 eqtrdi 
 |-  ( ph -> ( <. X , X >. .x. X ) = tpos ( +g ` M ) )
27 15 17 26 3eqtr4rd 
 |-  ( ph -> ( <. X , X >. .x. X ) = ( <. Y , Y >. ( comp ` O ) Y ) )
28 8 oveqd 
 |-  ( ph -> ( <. Y , Y >. .xb Y ) = ( <. Y , Y >. ( comp ` O ) Y ) )
29 27 28 eqtr4d 
 |-  ( ph -> ( <. X , X >. .x. X ) = ( <. Y , Y >. .xb Y ) )