Metamath Proof Explorer

Theorem catass

Description: Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catcocl.b 
|- B = ( Base ` C )
catcocl.h 
|- H = ( Hom ` C )
catcocl.o 
|- .x. = ( comp ` C )
catcocl.c 
|- ( ph -> C e. Cat )
catcocl.x 
|- ( ph -> X e. B )
catcocl.y 
|- ( ph -> Y e. B )
catcocl.z 
|- ( ph -> Z e. B )
catcocl.f 
|- ( ph -> F e. ( X H Y ) )
catcocl.g 
|- ( ph -> G e. ( Y H Z ) )
catass.w 
|- ( ph -> W e. B )
catass.g 
|- ( ph -> K e. ( Z H W ) )
Assertion catass 
|- ( ph -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) )

Proof

Step Hyp Ref Expression
1 catcocl.b 
 |-  B = ( Base ` C )
2 catcocl.h 
 |-  H = ( Hom ` C )
3 catcocl.o 
 |-  .x. = ( comp ` C )
4 catcocl.c 
 |-  ( ph -> C e. Cat )
5 catcocl.x 
 |-  ( ph -> X e. B )
6 catcocl.y 
 |-  ( ph -> Y e. B )
7 catcocl.z 
 |-  ( ph -> Z e. B )
8 catcocl.f 
 |-  ( ph -> F e. ( X H Y ) )
9 catcocl.g 
 |-  ( ph -> G e. ( Y H Z ) )
10 catass.w 
 |-  ( ph -> W e. B )
11 catass.g 
 |-  ( ph -> K e. ( Z H W ) )
12 1 2 3 iscat 
 |-  ( C e. Cat -> ( C e. Cat <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
13 12 ibi 
 |-  ( C e. Cat -> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
14 4 13 syl 
 |-  ( ph -> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
15 6 adantr 
 |-  ( ( ph /\ x = X ) -> Y e. B )
16 7 ad2antrr 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> Z e. B )
17 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> F e. ( X H Y ) )
18 simpllr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> x = X )
19 simplr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> y = Y )
20 18 19 oveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( x H y ) = ( X H Y ) )
21 17 20 eleqtrrd 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> F e. ( x H y ) )
22 9 ad4antr 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> G e. ( Y H Z ) )
23 simpllr 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> y = Y )
24 simplr 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> z = Z )
25 23 24 oveq12d 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> ( y H z ) = ( Y H Z ) )
26 22 25 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> G e. ( y H z ) )
27 10 ad5antr 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> W e. B )
28 11 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) -> K e. ( Z H W ) )
29 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) -> z = Z )
30 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) -> w = W )
31 29 30 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) -> ( z H w ) = ( Z H W ) )
32 28 31 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) -> K e. ( z H w ) )
33 simp-7r 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> x = X )
34 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> y = Y )
35 33 34 opeq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> <. x , y >. = <. X , Y >. )
36 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> w = W )
37 35 36 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( <. x , y >. .x. w ) = ( <. X , Y >. .x. W ) )
38 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> z = Z )
39 34 38 opeq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> <. y , z >. = <. Y , Z >. )
40 39 36 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( <. y , z >. .x. w ) = ( <. Y , Z >. .x. W ) )
41 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> k = K )
42 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> g = G )
43 40 41 42 oveq123d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( k ( <. y , z >. .x. w ) g ) = ( K ( <. Y , Z >. .x. W ) G ) )
44 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> f = F )
45 37 43 44 oveq123d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) )
46 33 38 opeq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> <. x , z >. = <. X , Z >. )
47 46 36 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( <. x , z >. .x. w ) = ( <. X , Z >. .x. W ) )
48 35 38 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( <. x , y >. .x. z ) = ( <. X , Y >. .x. Z ) )
49 48 42 44 oveq123d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( g ( <. x , y >. .x. z ) f ) = ( G ( <. X , Y >. .x. Z ) F ) )
50 47 41 49 oveq123d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) )
51 45 50 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) /\ k = K ) -> ( ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) <-> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
52 32 51 rspcdv 
 |-  ( ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) /\ w = W ) -> ( A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
53 27 52 rspcimdv 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
54 53 adantld 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
55 26 54 rspcimdv 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> ( A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
56 21 55 rspcimdv 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
57 16 56 rspcimdv 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
58 15 57 rspcimdv 
 |-  ( ( ph /\ x = X ) -> ( A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
59 58 adantld 
 |-  ( ( ph /\ x = X ) -> ( ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
60 5 59 rspcimdv 
 |-  ( ph -> ( A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
61 14 60 mpd 
 |-  ( ph -> ( ( K ( <. Y , Z >. .x. W ) G ) ( <. X , Y >. .x. W ) F ) = ( K ( <. X , Z >. .x. W ) ( G ( <. X , Y >. .x. Z ) F ) ) )