Metamath Proof Explorer

Theorem mndtcco

Description: The composition of the category built from a monoid is the monoid operation. (Contributed by Zhi Wang, 22-Sep-2024)

Ref Expression
Hypotheses mndtcbas.c 
|- ( ph -> C = ( MndToCat ` M ) )
mndtcbas.m 
|- ( ph -> M e. Mnd )
mndtcbas.b 
|- ( ph -> B = ( Base ` C ) )
mndtchom.x 
|- ( ph -> X e. B )
mndtchom.y 
|- ( ph -> Y e. B )
mndtcco.z 
|- ( ph -> Z e. B )
mndtcco.o 
|- ( ph -> .x. = ( comp ` C ) )
Assertion mndtcco 
|- ( ph -> ( <. X , Y >. .x. Z ) = ( +g ` M ) )

Proof

Step Hyp Ref Expression
1 mndtcbas.c 
 |-  ( ph -> C = ( MndToCat ` M ) )
2 mndtcbas.m 
 |-  ( ph -> M e. Mnd )
3 mndtcbas.b 
 |-  ( ph -> B = ( Base ` C ) )
4 mndtchom.x 
 |-  ( ph -> X e. B )
5 mndtchom.y 
 |-  ( ph -> Y e. B )
6 mndtcco.z 
 |-  ( ph -> Z e. B )
7 mndtcco.o 
 |-  ( ph -> .x. = ( comp ` C ) )
8 1 2 mndtcval 
 |-  ( ph -> C = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )
9 catstr 
 |-  { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } Struct <. 1 , ; 1 5 >.
10 ccoid 
 |-  comp = Slot ( comp ` ndx )
11 snsstp3 
 |-  { <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } C_ { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. }
12 snex 
 |-  { <. <. M , M , M >. , ( +g ` M ) >. } e. _V
13 12 a1i 
 |-  ( ph -> { <. <. M , M , M >. , ( +g ` M ) >. } e. _V )
14 eqid 
 |-  ( comp ` C ) = ( comp ` C )
15 8 9 10 11 13 14 strfv3 
 |-  ( ph -> ( comp ` C ) = { <. <. M , M , M >. , ( +g ` M ) >. } )
16 7 15 eqtrd 
 |-  ( ph -> .x. = { <. <. M , M , M >. , ( +g ` M ) >. } )
17 1 2 3 4 mndtcob 
 |-  ( ph -> X = M )
18 1 2 3 5 mndtcob 
 |-  ( ph -> Y = M )
19 17 18 opeq12d 
 |-  ( ph -> <. X , Y >. = <. M , M >. )
20 1 2 3 6 mndtcob 
 |-  ( ph -> Z = M )
21 16 19 20 oveq123d 
 |-  ( ph -> ( <. X , Y >. .x. Z ) = ( <. M , M >. { <. <. M , M , M >. , ( +g ` M ) >. } M ) )
22 df-ov 
 |-  ( <. M , M >. { <. <. M , M , M >. , ( +g ` M ) >. } M ) = ( { <. <. M , M , M >. , ( +g ` M ) >. } ` <. <. M , M >. , M >. )
23 df-ot 
 |-  <. M , M , M >. = <. <. M , M >. , M >.
24 23 fveq2i 
 |-  ( { <. <. M , M , M >. , ( +g ` M ) >. } ` <. M , M , M >. ) = ( { <. <. M , M , M >. , ( +g ` M ) >. } ` <. <. M , M >. , M >. )
25 otex 
 |-  <. M , M , M >. e. _V
26 fvex 
 |-  ( +g ` M ) e. _V
27 25 26 fvsn 
 |-  ( { <. <. M , M , M >. , ( +g ` M ) >. } ` <. M , M , M >. ) = ( +g ` M )
28 22 24 27 3eqtr2i 
 |-  ( <. M , M >. { <. <. M , M , M >. , ( +g ` M ) >. } M ) = ( +g ` M )
29 21 28 eqtrdi 
 |-  ( ph -> ( <. X , Y >. .x. Z ) = ( +g ` M ) )