Metamath Proof Explorer

Theorem mndtccatid

Description: Lemma for mndtccat and mndtcid . (Contributed by Zhi Wang, 22-Sep-2024)

Ref Expression
Hypotheses mndtccat.c 
|- ( ph -> C = ( MndToCat ` M ) )
mndtccat.m 
|- ( ph -> M e. Mnd )
Assertion mndtccatid 
|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. ( Base ` C ) |-> ( 0g ` M ) ) ) )

Proof

Step Hyp Ref Expression
1 mndtccat.c 
 |-  ( ph -> C = ( MndToCat ` M ) )
2 mndtccat.m 
 |-  ( ph -> M e. Mnd )
3 eqidd 
 |-  ( ph -> ( Base ` C ) = ( Base ` C ) )
4 eqidd 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` C ) )
5 eqidd 
 |-  ( ph -> ( comp ` C ) = ( comp ` C ) )
6 fvexd 
 |-  ( ph -> ( MndToCat ` M ) e. _V )
7 1 6 eqeltrd 
 |-  ( ph -> C e. _V )
8 biid 
 |-  ( ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) <-> ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) )
9 eqid 
 |-  ( Base ` M ) = ( Base ` M )
10 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
11 9 10 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. ( Base ` M ) )
12 2 11 syl 
 |-  ( ph -> ( 0g ` M ) e. ( Base ` M ) )
13 12 adantr 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( 0g ` M ) e. ( Base ` M ) )
14 1 adantr 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> C = ( MndToCat ` M ) )
15 2 adantr 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> M e. Mnd )
16 eqidd 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( Base ` C ) = ( Base ` C ) )
17 simpr 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> y e. ( Base ` C ) )
18 eqidd 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( Hom ` C ) = ( Hom ` C ) )
19 14 15 16 17 17 18 mndtchom 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( y ( Hom ` C ) y ) = ( Base ` M ) )
20 13 19 eleqtrrd 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( 0g ` M ) e. ( y ( Hom ` C ) y ) )
21 1 adantr 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> C = ( MndToCat ` M ) )
22 2 adantr 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> M e. Mnd )
23 eqidd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( Base ` C ) = ( Base ` C ) )
24 simpr1l 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> x e. ( Base ` C ) )
25 simpr1r 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> y e. ( Base ` C ) )
26 eqidd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( comp ` C ) = ( comp ` C ) )
27 21 22 23 24 25 25 26 mndtcco 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( <. x , y >. ( comp ` C ) y ) = ( +g ` M ) )
28 27 oveqd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( ( 0g ` M ) ( <. x , y >. ( comp ` C ) y ) f ) = ( ( 0g ` M ) ( +g ` M ) f ) )
29 simpr31 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> f e. ( x ( Hom ` C ) y ) )
30 eqidd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( Hom ` C ) = ( Hom ` C ) )
31 21 22 23 24 25 30 mndtchom 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( x ( Hom ` C ) y ) = ( Base ` M ) )
32 29 31 eleqtrd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> f e. ( Base ` M ) )
33 eqid 
 |-  ( +g ` M ) = ( +g ` M )
34 9 33 10 mndlid 
 |-  ( ( M e. Mnd /\ f e. ( Base ` M ) ) -> ( ( 0g ` M ) ( +g ` M ) f ) = f )
35 22 32 34 syl2anc 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( ( 0g ` M ) ( +g ` M ) f ) = f )
36 28 35 eqtrd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( ( 0g ` M ) ( <. x , y >. ( comp ` C ) y ) f ) = f )
37 simpr2l 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> z e. ( Base ` C ) )
38 21 22 23 25 25 37 26 mndtcco 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( <. y , y >. ( comp ` C ) z ) = ( +g ` M ) )
39 38 oveqd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( g ( <. y , y >. ( comp ` C ) z ) ( 0g ` M ) ) = ( g ( +g ` M ) ( 0g ` M ) ) )
40 simpr32 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> g e. ( y ( Hom ` C ) z ) )
41 21 22 23 25 37 30 mndtchom 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( y ( Hom ` C ) z ) = ( Base ` M ) )
42 40 41 eleqtrd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> g e. ( Base ` M ) )
43 9 33 10 mndrid 
 |-  ( ( M e. Mnd /\ g e. ( Base ` M ) ) -> ( g ( +g ` M ) ( 0g ` M ) ) = g )
44 22 42 43 syl2anc 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( g ( +g ` M ) ( 0g ` M ) ) = g )
45 39 44 eqtrd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( g ( <. y , y >. ( comp ` C ) z ) ( 0g ` M ) ) = g )
46 9 33 mndcl 
 |-  ( ( M e. Mnd /\ g e. ( Base ` M ) /\ f e. ( Base ` M ) ) -> ( g ( +g ` M ) f ) e. ( Base ` M ) )
47 22 42 32 46 syl3anc 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( g ( +g ` M ) f ) e. ( Base ` M ) )
48 21 22 23 24 25 37 26 mndtcco 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( <. x , y >. ( comp ` C ) z ) = ( +g ` M ) )
49 48 oveqd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( +g ` M ) f ) )
50 21 22 23 24 37 30 mndtchom 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( x ( Hom ` C ) z ) = ( Base ` M ) )
51 47 49 50 3eltr4d 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) )
52 simpr33 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> k e. ( z ( Hom ` C ) w ) )
53 simpr2r 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> w e. ( Base ` C ) )
54 21 22 23 37 53 30 mndtchom 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( z ( Hom ` C ) w ) = ( Base ` M ) )
55 52 54 eleqtrd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> k e. ( Base ` M ) )
56 9 33 mndass 
 |-  ( ( M e. Mnd /\ ( k e. ( Base ` M ) /\ g e. ( Base ` M ) /\ f e. ( Base ` M ) ) ) -> ( ( k ( +g ` M ) g ) ( +g ` M ) f ) = ( k ( +g ` M ) ( g ( +g ` M ) f ) ) )
57 22 55 42 32 56 syl13anc 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( ( k ( +g ` M ) g ) ( +g ` M ) f ) = ( k ( +g ` M ) ( g ( +g ` M ) f ) ) )
58 21 22 23 24 25 53 26 mndtcco 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( <. x , y >. ( comp ` C ) w ) = ( +g ` M ) )
59 21 22 23 25 37 53 26 mndtcco 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( <. y , z >. ( comp ` C ) w ) = ( +g ` M ) )
60 59 oveqd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( k ( <. y , z >. ( comp ` C ) w ) g ) = ( k ( +g ` M ) g ) )
61 eqidd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> f = f )
62 58 60 61 oveq123d 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( ( k ( +g ` M ) g ) ( +g ` M ) f ) )
63 21 22 23 24 37 53 26 mndtcco 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( <. x , z >. ( comp ` C ) w ) = ( +g ` M ) )
64 eqidd 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> k = k )
65 63 64 49 oveq123d 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( k ( +g ` M ) ( g ( +g ` M ) f ) ) )
66 57 62 65 3eqtr4d 
 |-  ( ( ph /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) /\ k e. ( z ( Hom ` C ) w ) ) ) ) -> ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) )
67 3 4 5 7 8 20 36 45 51 66 iscatd2 
 |-  ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. ( Base ` C ) |-> ( 0g ` M ) ) ) )