Metamath Proof Explorer

Theorem funcco

Description: A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcco.b 
|- B = ( Base ` D )
funcco.h 
|- H = ( Hom ` D )
funcco.o 
|- .x. = ( comp ` D )
funcco.O 
|- O = ( comp ` E )
funcco.f 
|- ( ph -> F ( D Func E ) G )
funcco.x 
|- ( ph -> X e. B )
funcco.y 
|- ( ph -> Y e. B )
funcco.z 
|- ( ph -> Z e. B )
funcco.m 
|- ( ph -> M e. ( X H Y ) )
funcco.n 
|- ( ph -> N e. ( Y H Z ) )
Assertion funcco 
|- ( ph -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) )

Proof

Step Hyp Ref Expression
1 funcco.b 
 |-  B = ( Base ` D )
2 funcco.h 
 |-  H = ( Hom ` D )
3 funcco.o 
 |-  .x. = ( comp ` D )
4 funcco.O 
 |-  O = ( comp ` E )
5 funcco.f 
 |-  ( ph -> F ( D Func E ) G )
6 funcco.x 
 |-  ( ph -> X e. B )
7 funcco.y 
 |-  ( ph -> Y e. B )
8 funcco.z 
 |-  ( ph -> Z e. B )
9 funcco.m 
 |-  ( ph -> M e. ( X H Y ) )
10 funcco.n 
 |-  ( ph -> N e. ( Y H Z ) )
11 eqid 
 |-  ( Base ` E ) = ( Base ` E )
12 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
13 eqid 
 |-  ( Id ` D ) = ( Id ` D )
14 eqid 
 |-  ( Id ` E ) = ( Id ` E )
15 df-br 
 |-  ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
16 5 15 sylib 
 |-  ( ph -> <. F , G >. e. ( D Func E ) )
17 funcrcl 
 |-  ( <. F , G >. e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
18 16 17 syl 
 |-  ( ph -> ( D e. Cat /\ E e. Cat ) )
19 18 simpld 
 |-  ( ph -> D e. Cat )
20 18 simprd 
 |-  ( ph -> E e. Cat )
21 1 11 2 12 13 14 3 4 19 20 isfunc 
 |-  ( ph -> ( F ( D Func E ) G <-> ( F : B --> ( Base ` E ) /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` E ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) )
22 5 21 mpbid 
 |-  ( ph -> ( F : B --> ( Base ` E ) /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` E ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) )
23 22 simp3d 
 |-  ( ph -> A. x e. B ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) )
24 7 adantr 
 |-  ( ( ph /\ x = X ) -> Y e. B )
25 8 ad2antrr 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> Z e. B )
26 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> M e. ( X H Y ) )
27 simpllr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> x = X )
28 simplr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> y = Y )
29 27 28 oveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( x H y ) = ( X H Y ) )
30 26 29 eleqtrrd 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> M e. ( x H y ) )
31 10 ad4antr 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) -> N e. ( Y H Z ) )
32 simpllr 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) -> y = Y )
33 simplr 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) -> z = Z )
34 32 33 oveq12d 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) -> ( y H z ) = ( Y H Z ) )
35 31 34 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) -> N e. ( y H z ) )
36 simp-5r 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> x = X )
37 simpllr 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> z = Z )
38 36 37 oveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( x G z ) = ( X G Z ) )
39 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> y = Y )
40 36 39 opeq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> <. x , y >. = <. X , Y >. )
41 40 37 oveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( <. x , y >. .x. z ) = ( <. X , Y >. .x. Z ) )
42 simpr 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> n = N )
43 simplr 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> m = M )
44 41 42 43 oveq123d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( n ( <. x , y >. .x. z ) m ) = ( N ( <. X , Y >. .x. Z ) M ) )
45 38 44 fveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) )
46 36 fveq2d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( F ` x ) = ( F ` X ) )
47 39 fveq2d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( F ` y ) = ( F ` Y ) )
48 46 47 opeq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> <. ( F ` x ) , ( F ` y ) >. = <. ( F ` X ) , ( F ` Y ) >. )
49 37 fveq2d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( F ` z ) = ( F ` Z ) )
50 48 49 oveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) = ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) )
51 39 37 oveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( y G z ) = ( Y G Z ) )
52 51 42 fveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( ( y G z ) ` n ) = ( ( Y G Z ) ` N ) )
53 36 39 oveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( x G y ) = ( X G Y ) )
54 53 43 fveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( ( x G y ) ` m ) = ( ( X G Y ) ` M ) )
55 50 52 54 oveq123d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) )
56 45 55 eqeq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) /\ n = N ) -> ( ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) <-> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) ) )
57 35 56 rspcdv 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ m = M ) -> ( A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) ) )
58 30 57 rspcimdv 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) ) )
59 25 58 rspcimdv 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) ) )
60 24 59 rspcimdv 
 |-  ( ( ph /\ x = X ) -> ( A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) ) )
61 60 adantld 
 |-  ( ( ph /\ x = X ) -> ( ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) ) )
62 6 61 rspcimdv 
 |-  ( ph -> ( A. x e. B ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) ) )
63 23 62 mpd 
 |-  ( ph -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) )