Metamath Proof Explorer

Theorem fucass

Description: Associativity of natural transformation composition. Remark 6.14(b) in Adamek p. 87. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fucass.q 
|- Q = ( C FuncCat D )
fucass.n 
|- N = ( C Nat D )
fucass.x 
|- .xb = ( comp ` Q )
fucass.r 
|- ( ph -> R e. ( F N G ) )
fucass.s 
|- ( ph -> S e. ( G N H ) )
fucass.t 
|- ( ph -> T e. ( H N K ) )
Assertion fucass 
|- ( ph -> ( ( T ( <. G , H >. .xb K ) S ) ( <. F , G >. .xb K ) R ) = ( T ( <. F , H >. .xb K ) ( S ( <. F , G >. .xb H ) R ) ) )

Proof

Step Hyp Ref Expression
1 fucass.q 
 |-  Q = ( C FuncCat D )
2 fucass.n 
 |-  N = ( C Nat D )
3 fucass.x 
 |-  .xb = ( comp ` Q )
4 fucass.r 
 |-  ( ph -> R e. ( F N G ) )
5 fucass.s 
 |-  ( ph -> S e. ( G N H ) )
6 fucass.t 
 |-  ( ph -> T e. ( H N K ) )
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
9 eqid 
 |-  ( comp ` D ) = ( comp ` D )
10 2 natrcl 
 |-  ( R e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
11 4 10 syl 
 |-  ( ph -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
12 11 simpld 
 |-  ( ph -> F e. ( C Func D ) )
13 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
14 12 13 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
15 14 simprd 
 |-  ( ph -> D e. Cat )
16 15 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
17 eqid 
 |-  ( Base ` C ) = ( Base ` C )
18 relfunc 
 |-  Rel ( C Func D )
19 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
20 18 12 19 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
21 17 7 20 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
22 21 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
23 11 simprd 
 |-  ( ph -> G e. ( C Func D ) )
24 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
25 18 23 24 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
26 17 7 25 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
27 26 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
28 2 natrcl 
 |-  ( T e. ( H N K ) -> ( H e. ( C Func D ) /\ K e. ( C Func D ) ) )
29 6 28 syl 
 |-  ( ph -> ( H e. ( C Func D ) /\ K e. ( C Func D ) ) )
30 29 simpld 
 |-  ( ph -> H e. ( C Func D ) )
31 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ H e. ( C Func D ) ) -> ( 1st ` H ) ( C Func D ) ( 2nd ` H ) )
32 18 30 31 sylancr 
 |-  ( ph -> ( 1st ` H ) ( C Func D ) ( 2nd ` H ) )
33 17 7 32 funcf1 
 |-  ( ph -> ( 1st ` H ) : ( Base ` C ) --> ( Base ` D ) )
34 33 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` H ) ` x ) e. ( Base ` D ) )
35 2 4 nat1st2nd 
 |-  ( ph -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
36 35 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
37 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
38 2 36 17 8 37 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( R ` x ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` x ) ) )
39 2 5 nat1st2nd 
 |-  ( ph -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. N <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
40 39 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. N <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
41 2 40 17 8 37 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( S ` x ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
42 29 simprd 
 |-  ( ph -> K e. ( C Func D ) )
43 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ K e. ( C Func D ) ) -> ( 1st ` K ) ( C Func D ) ( 2nd ` K ) )
44 18 42 43 sylancr 
 |-  ( ph -> ( 1st ` K ) ( C Func D ) ( 2nd ` K ) )
45 17 7 44 funcf1 
 |-  ( ph -> ( 1st ` K ) : ( Base ` C ) --> ( Base ` D ) )
46 45 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` K ) ` x ) e. ( Base ` D ) )
47 2 6 nat1st2nd 
 |-  ( ph -> T e. ( <. ( 1st ` H ) , ( 2nd ` H ) >. N <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
48 47 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> T e. ( <. ( 1st ` H ) , ( 2nd ` H ) >. N <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
49 2 48 17 8 37 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( T ` x ) e. ( ( ( 1st ` H ) ` x ) ( Hom ` D ) ( ( 1st ` K ) ` x ) ) )
50 7 8 9 16 22 27 34 38 41 46 49 catass 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( T ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( S ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( R ` x ) ) = ( ( T ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
51 5 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> S e. ( G N H ) )
52 6 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> T e. ( H N K ) )
53 1 2 17 9 3 51 52 37 fuccoval 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( T ( <. G , H >. .xb K ) S ) ` x ) = ( ( T ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( S ` x ) ) )
54 53 oveq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( T ( <. G , H >. .xb K ) S ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( R ` x ) ) = ( ( ( T ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( S ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( R ` x ) ) )
55 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( F N G ) )
56 1 2 17 9 3 55 51 37 fuccoval 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( S ( <. F , G >. .xb H ) R ) ` x ) = ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) )
57 56 oveq2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( T ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( ( S ( <. F , G >. .xb H ) R ) ` x ) ) = ( ( T ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
58 50 54 57 3eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( T ( <. G , H >. .xb K ) S ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( R ` x ) ) = ( ( T ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( ( S ( <. F , G >. .xb H ) R ) ` x ) ) )
59 58 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( T ( <. G , H >. .xb K ) S ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( R ` x ) ) ) = ( x e. ( Base ` C ) |-> ( ( T ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( ( S ( <. F , G >. .xb H ) R ) ` x ) ) ) )
60 1 2 3 5 6 fuccocl 
 |-  ( ph -> ( T ( <. G , H >. .xb K ) S ) e. ( G N K ) )
61 1 2 17 9 3 4 60 fucco 
 |-  ( ph -> ( ( T ( <. G , H >. .xb K ) S ) ( <. F , G >. .xb K ) R ) = ( x e. ( Base ` C ) |-> ( ( ( T ( <. G , H >. .xb K ) S ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( R ` x ) ) ) )
62 1 2 3 4 5 fuccocl 
 |-  ( ph -> ( S ( <. F , G >. .xb H ) R ) e. ( F N H ) )
63 1 2 17 9 3 62 6 fucco 
 |-  ( ph -> ( T ( <. F , H >. .xb K ) ( S ( <. F , G >. .xb H ) R ) ) = ( x e. ( Base ` C ) |-> ( ( T ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` K ) ` x ) ) ( ( S ( <. F , G >. .xb H ) R ) ` x ) ) ) )
64 59 61 63 3eqtr4d 
 |-  ( ph -> ( ( T ( <. G , H >. .xb K ) S ) ( <. F , G >. .xb K ) R ) = ( T ( <. F , H >. .xb K ) ( S ( <. F , G >. .xb H ) R ) ) )