Metamath Proof Explorer


Theorem fuclid

Description: Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fuclid.q
|- Q = ( C FuncCat D )
fuclid.n
|- N = ( C Nat D )
fuclid.x
|- .xb = ( comp ` Q )
fuclid.1
|- .1. = ( Id ` D )
fuclid.r
|- ( ph -> R e. ( F N G ) )
Assertion fuclid
|- ( ph -> ( ( .1. o. ( 1st ` G ) ) ( <. F , G >. .xb G ) R ) = R )

Proof

Step Hyp Ref Expression
1 fuclid.q
 |-  Q = ( C FuncCat D )
2 fuclid.n
 |-  N = ( C Nat D )
3 fuclid.x
 |-  .xb = ( comp ` Q )
4 fuclid.1
 |-  .1. = ( Id ` D )
5 fuclid.r
 |-  ( ph -> R e. ( F N G ) )
6 eqid
 |-  ( Base ` C ) = ( Base ` C )
7 eqid
 |-  ( Base ` D ) = ( Base ` D )
8 relfunc
 |-  Rel ( C Func D )
9 2 natrcl
 |-  ( R e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
10 5 9 syl
 |-  ( ph -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
11 10 simprd
 |-  ( ph -> G e. ( C Func D ) )
12 1st2ndbr
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
13 8 11 12 sylancr
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
14 6 7 13 funcf1
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
15 fvco3
 |-  ( ( ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) /\ x e. ( Base ` C ) ) -> ( ( .1. o. ( 1st ` G ) ) ` x ) = ( .1. ` ( ( 1st ` G ) ` x ) ) )
16 14 15 sylan
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( .1. o. ( 1st ` G ) ) ` x ) = ( .1. ` ( ( 1st ` G ) ` x ) ) )
17 16 oveq1d
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( .1. o. ( 1st ` G ) ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) = ( ( .1. ` ( ( 1st ` G ) ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) )
18 eqid
 |-  ( Hom ` D ) = ( Hom ` D )
19 10 simpld
 |-  ( ph -> F e. ( C Func D ) )
20 funcrcl
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
21 19 20 syl
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
22 21 simprd
 |-  ( ph -> D e. Cat )
23 22 adantr
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
24 1st2ndbr
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
25 8 19 24 sylancr
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
26 6 7 25 funcf1
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
27 26 ffvelrnda
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
28 eqid
 |-  ( comp ` D ) = ( comp ` D )
29 14 ffvelrnda
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
30 2 5 nat1st2nd
 |-  ( ph -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
31 30 adantr
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
32 simpr
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
33 2 31 6 18 32 natcl
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( R ` x ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` x ) ) )
34 7 18 4 23 27 28 29 33 catlid
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( .1. ` ( ( 1st ` G ) ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) = ( R ` x ) )
35 17 34 eqtrd
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( .1. o. ( 1st ` G ) ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) = ( R ` x ) )
36 35 mpteq2dva
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( .1. o. ( 1st ` G ) ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) ) = ( x e. ( Base ` C ) |-> ( R ` x ) ) )
37 1 2 4 11 fucidcl
 |-  ( ph -> ( .1. o. ( 1st ` G ) ) e. ( G N G ) )
38 1 2 6 28 3 5 37 fucco
 |-  ( ph -> ( ( .1. o. ( 1st ` G ) ) ( <. F , G >. .xb G ) R ) = ( x e. ( Base ` C ) |-> ( ( ( .1. o. ( 1st ` G ) ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) ) )
39 2 30 6 natfn
 |-  ( ph -> R Fn ( Base ` C ) )
40 dffn5
 |-  ( R Fn ( Base ` C ) <-> R = ( x e. ( Base ` C ) |-> ( R ` x ) ) )
41 39 40 sylib
 |-  ( ph -> R = ( x e. ( Base ` C ) |-> ( R ` x ) ) )
42 36 38 41 3eqtr4d
 |-  ( ph -> ( ( .1. o. ( 1st ` G ) ) ( <. F , G >. .xb G ) R ) = R )