Metamath Proof Explorer

Theorem fucco

Description: Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fucco.q 
|- Q = ( C FuncCat D )
fucco.n 
|- N = ( C Nat D )
fucco.a 
|- A = ( Base ` C )
fucco.o 
|- .x. = ( comp ` D )
fucco.x 
|- .xb = ( comp ` Q )
fucco.f 
|- ( ph -> R e. ( F N G ) )
fucco.g 
|- ( ph -> S e. ( G N H ) )
Assertion fucco 
|- ( ph -> ( S ( <. F , G >. .xb H ) R ) = ( x e. A |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 fucco.q 
 |-  Q = ( C FuncCat D )
2 fucco.n 
 |-  N = ( C Nat D )
3 fucco.a 
 |-  A = ( Base ` C )
4 fucco.o 
 |-  .x. = ( comp ` D )
5 fucco.x 
 |-  .xb = ( comp ` Q )
6 fucco.f 
 |-  ( ph -> R e. ( F N G ) )
7 fucco.g 
 |-  ( ph -> S e. ( G N H ) )
8 eqid 
 |-  ( C Func D ) = ( C Func D )
9 2 natrcl 
 |-  ( R e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
10 6 9 syl 
 |-  ( ph -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
11 10 simpld 
 |-  ( ph -> F e. ( C Func D ) )
12 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
13 11 12 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
14 13 simpld 
 |-  ( ph -> C e. Cat )
15 13 simprd 
 |-  ( ph -> D e. Cat )
16 1 8 2 3 4 14 15 5 fuccofval 
 |-  ( ph -> .xb = ( v e. ( ( C Func D ) X. ( C Func D ) ) , h e. ( C Func D ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) )
17 fvexd 
 |-  ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) -> ( 1st ` v ) e. _V )
18 simprl 
 |-  ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) -> v = <. F , G >. )
19 18 fveq2d 
 |-  ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) -> ( 1st ` v ) = ( 1st ` <. F , G >. ) )
20 op1stg 
 |-  ( ( F e. ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` <. F , G >. ) = F )
21 10 20 syl 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
22 21 adantr 
 |-  ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) -> ( 1st ` <. F , G >. ) = F )
23 19 22 eqtrd 
 |-  ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) -> ( 1st ` v ) = F )
24 fvexd 
 |-  ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) -> ( 2nd ` v ) e. _V )
25 18 adantr 
 |-  ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) -> v = <. F , G >. )
26 25 fveq2d 
 |-  ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) -> ( 2nd ` v ) = ( 2nd ` <. F , G >. ) )
27 op2ndg 
 |-  ( ( F e. ( C Func D ) /\ G e. ( C Func D ) ) -> ( 2nd ` <. F , G >. ) = G )
28 10 27 syl 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
29 28 ad2antrr 
 |-  ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) -> ( 2nd ` <. F , G >. ) = G )
30 26 29 eqtrd 
 |-  ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) -> ( 2nd ` v ) = G )
31 simpr 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> g = G )
32 simprr 
 |-  ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) -> h = H )
33 32 ad2antrr 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> h = H )
34 31 33 oveq12d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( g N h ) = ( G N H ) )
35 simplr 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> f = F )
36 35 31 oveq12d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( f N g ) = ( F N G ) )
37 35 fveq2d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( 1st ` f ) = ( 1st ` F ) )
38 37 fveq1d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` F ) ` x ) )
39 31 fveq2d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( 1st ` g ) = ( 1st ` G ) )
40 39 fveq1d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( ( 1st ` g ) ` x ) = ( ( 1st ` G ) ` x ) )
41 38 40 opeq12d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. = <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. )
42 33 fveq2d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( 1st ` h ) = ( 1st ` H ) )
43 42 fveq1d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( ( 1st ` h ) ` x ) = ( ( 1st ` H ) ` x ) )
44 41 43 oveq12d 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) = ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) )
45 44 oveqd 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) = ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) )
46 45 mpteq2dv 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) = ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) ) )
47 34 36 46 mpoeq123dv 
 |-  ( ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) /\ g = G ) -> ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) = ( b e. ( G N H ) , a e. ( F N G ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) ) ) )
48 24 30 47 csbied2 
 |-  ( ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) /\ f = F ) -> [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) = ( b e. ( G N H ) , a e. ( F N G ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) ) ) )
49 17 23 48 csbied2 
 |-  ( ( ph /\ ( v = <. F , G >. /\ h = H ) ) -> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) = ( b e. ( G N H ) , a e. ( F N G ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) ) ) )
50 opelxpi 
 |-  ( ( F e. ( C Func D ) /\ G e. ( C Func D ) ) -> <. F , G >. e. ( ( C Func D ) X. ( C Func D ) ) )
51 10 50 syl 
 |-  ( ph -> <. F , G >. e. ( ( C Func D ) X. ( C Func D ) ) )
52 2 natrcl 
 |-  ( S e. ( G N H ) -> ( G e. ( C Func D ) /\ H e. ( C Func D ) ) )
53 7 52 syl 
 |-  ( ph -> ( G e. ( C Func D ) /\ H e. ( C Func D ) ) )
54 53 simprd 
 |-  ( ph -> H e. ( C Func D ) )
55 ovex 
 |-  ( G N H ) e. _V
56 ovex 
 |-  ( F N G ) e. _V
57 55 56 mpoex 
 |-  ( b e. ( G N H ) , a e. ( F N G ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) ) ) e. _V
58 57 a1i 
 |-  ( ph -> ( b e. ( G N H ) , a e. ( F N G ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) ) ) e. _V )
59 16 49 51 54 58 ovmpod 
 |-  ( ph -> ( <. F , G >. .xb H ) = ( b e. ( G N H ) , a e. ( F N G ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) ) ) )
60 simprl 
 |-  ( ( ph /\ ( b = S /\ a = R ) ) -> b = S )
61 60 fveq1d 
 |-  ( ( ph /\ ( b = S /\ a = R ) ) -> ( b ` x ) = ( S ` x ) )
62 simprr 
 |-  ( ( ph /\ ( b = S /\ a = R ) ) -> a = R )
63 62 fveq1d 
 |-  ( ( ph /\ ( b = S /\ a = R ) ) -> ( a ` x ) = ( R ` x ) )
64 61 63 oveq12d 
 |-  ( ( ph /\ ( b = S /\ a = R ) ) -> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) = ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) )
65 64 mpteq2dv 
 |-  ( ( ph /\ ( b = S /\ a = R ) ) -> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( a ` x ) ) ) = ( x e. A |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
66 3 fvexi 
 |-  A e. _V
67 66 mptex 
 |-  ( x e. A |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) e. _V
68 67 a1i 
 |-  ( ph -> ( x e. A |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) e. _V )
69 59 65 7 6 68 ovmpod 
 |-  ( ph -> ( S ( <. F , G >. .xb H ) R ) = ( x e. A |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )