Metamath Proof Explorer

Theorem nati

Description: Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natrcl.1 
|- N = ( C Nat D )
natixp.2 
|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
natixp.b 
|- B = ( Base ` C )
nati.h 
|- H = ( Hom ` C )
nati.o 
|- .x. = ( comp ` D )
nati.x 
|- ( ph -> X e. B )
nati.y 
|- ( ph -> Y e. B )
nati.r 
|- ( ph -> R e. ( X H Y ) )
Assertion nati 
|- ( ph -> ( ( A ` Y ) ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) ( ( X G Y ) ` R ) ) = ( ( ( X L Y ) ` R ) ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) ( A ` X ) ) )

Proof

Step Hyp Ref Expression
1 natrcl.1 
 |-  N = ( C Nat D )
2 natixp.2 
 |-  ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
3 natixp.b 
 |-  B = ( Base ` C )
4 nati.h 
 |-  H = ( Hom ` C )
5 nati.o 
 |-  .x. = ( comp ` D )
6 nati.x 
 |-  ( ph -> X e. B )
7 nati.y 
 |-  ( ph -> Y e. B )
8 nati.r 
 |-  ( ph -> R e. ( X H Y ) )
9 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
10 1 natrcl 
 |-  ( A e. ( <. F , G >. N <. K , L >. ) -> ( <. F , G >. e. ( C Func D ) /\ <. K , L >. e. ( C Func D ) ) )
11 2 10 syl 
 |-  ( ph -> ( <. F , G >. e. ( C Func D ) /\ <. K , L >. e. ( C Func D ) ) )
12 11 simpld 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
13 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
14 12 13 sylibr 
 |-  ( ph -> F ( C Func D ) G )
15 11 simprd 
 |-  ( ph -> <. K , L >. e. ( C Func D ) )
16 df-br 
 |-  ( K ( C Func D ) L <-> <. K , L >. e. ( C Func D ) )
17 15 16 sylibr 
 |-  ( ph -> K ( C Func D ) L )
18 1 3 4 9 5 14 17 isnat 
 |-  ( ph -> ( A e. ( <. F , G >. N <. K , L >. ) <-> ( A e. X_ x e. B ( ( F ` x ) ( Hom ` D ) ( K ` x ) ) /\ A. x e. B A. y e. B A. f e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` f ) ) = ( ( ( x L y ) ` f ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) ) )
19 2 18 mpbid 
 |-  ( ph -> ( A e. X_ x e. B ( ( F ` x ) ( Hom ` D ) ( K ` x ) ) /\ A. x e. B A. y e. B A. f e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` f ) ) = ( ( ( x L y ) ` f ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) )
20 19 simprd 
 |-  ( ph -> A. x e. B A. y e. B A. f e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` f ) ) = ( ( ( x L y ) ` f ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) )
21 7 adantr 
 |-  ( ( ph /\ x = X ) -> Y e. B )
22 8 ad2antrr 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> R e. ( X H Y ) )
23 simplr 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> x = X )
24 simpr 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> y = Y )
25 23 24 oveq12d 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( x H y ) = ( X H Y ) )
26 22 25 eleqtrrd 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> R e. ( x H y ) )
27 simpllr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> x = X )
28 27 fveq2d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( F ` x ) = ( F ` X ) )
29 simplr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> y = Y )
30 29 fveq2d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( F ` y ) = ( F ` Y ) )
31 28 30 opeq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> <. ( F ` x ) , ( F ` y ) >. = <. ( F ` X ) , ( F ` Y ) >. )
32 29 fveq2d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( K ` y ) = ( K ` Y ) )
33 31 32 oveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) = ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) )
34 29 fveq2d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( A ` y ) = ( A ` Y ) )
35 27 29 oveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( x G y ) = ( X G Y ) )
36 simpr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> f = R )
37 35 36 fveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( ( x G y ) ` f ) = ( ( X G Y ) ` R ) )
38 33 34 37 oveq123d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` f ) ) = ( ( A ` Y ) ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) ( ( X G Y ) ` R ) ) )
39 27 fveq2d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( K ` x ) = ( K ` X ) )
40 28 39 opeq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> <. ( F ` x ) , ( K ` x ) >. = <. ( F ` X ) , ( K ` X ) >. )
41 40 32 oveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) = ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) )
42 27 29 oveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( x L y ) = ( X L Y ) )
43 42 36 fveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( ( x L y ) ` f ) = ( ( X L Y ) ` R ) )
44 27 fveq2d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( A ` x ) = ( A ` X ) )
45 41 43 44 oveq123d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( ( ( x L y ) ` f ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) = ( ( ( X L Y ) ` R ) ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) ( A ` X ) ) )
46 38 45 eqeq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ f = R ) -> ( ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` f ) ) = ( ( ( x L y ) ` f ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) <-> ( ( A ` Y ) ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) ( ( X G Y ) ` R ) ) = ( ( ( X L Y ) ` R ) ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) ( A ` X ) ) ) )
47 26 46 rspcdv 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( A. f e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` f ) ) = ( ( ( x L y ) ` f ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) -> ( ( A ` Y ) ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) ( ( X G Y ) ` R ) ) = ( ( ( X L Y ) ` R ) ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) ( A ` X ) ) ) )
48 21 47 rspcimdv 
 |-  ( ( ph /\ x = X ) -> ( A. y e. B A. f e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` f ) ) = ( ( ( x L y ) ` f ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) -> ( ( A ` Y ) ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) ( ( X G Y ) ` R ) ) = ( ( ( X L Y ) ` R ) ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) ( A ` X ) ) ) )
49 6 48 rspcimdv 
 |-  ( ph -> ( A. x e. B A. y e. B A. f e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` f ) ) = ( ( ( x L y ) ` f ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) -> ( ( A ` Y ) ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) ( ( X G Y ) ` R ) ) = ( ( ( X L Y ) ` R ) ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) ( A ` X ) ) ) )
50 20 49 mpd 
 |-  ( ph -> ( ( A ` Y ) ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) ( ( X G Y ) ` R ) ) = ( ( ( X L Y ) ` R ) ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) ( A ` X ) ) )