MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  arwrid Unicode version

Theorem arwrid 14148
Description: Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypotheses
Ref Expression
arwlid.h  |-  H  =  (Homa
`  C )
arwlid.o  |-  .x.  =  (compa `  C )
arwlid.a  |-  .1.  =  (Ida `  C )
arwlid.f  |-  ( ph  ->  F  e.  ( X H Y ) )
Assertion
Ref Expression
arwrid  |-  ( ph  ->  ( F  .x.  (  .1.  `  X ) )  =  F )

Proof of Theorem arwrid
StepHypRef Expression
1 arwlid.a . . . . . 6  |-  .1.  =  (Ida `  C )
2 eqid 2380 . . . . . 6  |-  ( Base `  C )  =  (
Base `  C )
3 arwlid.f . . . . . . 7  |-  ( ph  ->  F  e.  ( X H Y ) )
4 arwlid.h . . . . . . . 8  |-  H  =  (Homa
`  C )
54homarcl 14103 . . . . . . 7  |-  ( F  e.  ( X H Y )  ->  C  e.  Cat )
63, 5syl 16 . . . . . 6  |-  ( ph  ->  C  e.  Cat )
7 eqid 2380 . . . . . 6  |-  ( Id
`  C )  =  ( Id `  C
)
84, 2homarcl2 14110 . . . . . . . 8  |-  ( F  e.  ( X H Y )  ->  ( X  e.  ( Base `  C )  /\  Y  e.  ( Base `  C
) ) )
93, 8syl 16 . . . . . . 7  |-  ( ph  ->  ( X  e.  (
Base `  C )  /\  Y  e.  ( Base `  C ) ) )
109simpld 446 . . . . . 6  |-  ( ph  ->  X  e.  ( Base `  C ) )
111, 2, 6, 7, 10ida2 14134 . . . . 5  |-  ( ph  ->  ( 2nd `  (  .1.  `  X ) )  =  ( ( Id
`  C ) `  X ) )
1211oveq2d 6029 . . . 4  |-  ( ph  ->  ( ( 2nd `  F
) ( <. X ,  X >. (comp `  C
) Y ) ( 2nd `  (  .1.  `  X ) ) )  =  ( ( 2nd `  F ) ( <. X ,  X >. (comp `  C ) Y ) ( ( Id `  C ) `  X
) ) )
13 eqid 2380 . . . . 5  |-  (  Hom  `  C )  =  (  Hom  `  C )
14 eqid 2380 . . . . 5  |-  (comp `  C )  =  (comp `  C )
159simprd 450 . . . . 5  |-  ( ph  ->  Y  e.  ( Base `  C ) )
164, 13homahom 14114 . . . . . 6  |-  ( F  e.  ( X H Y )  ->  ( 2nd `  F )  e.  ( X (  Hom  `  C ) Y ) )
173, 16syl 16 . . . . 5  |-  ( ph  ->  ( 2nd `  F
)  e.  ( X (  Hom  `  C
) Y ) )
182, 13, 7, 6, 10, 14, 15, 17catrid 13829 . . . 4  |-  ( ph  ->  ( ( 2nd `  F
) ( <. X ,  X >. (comp `  C
) Y ) ( ( Id `  C
) `  X )
)  =  ( 2nd `  F ) )
1912, 18eqtrd 2412 . . 3  |-  ( ph  ->  ( ( 2nd `  F
) ( <. X ,  X >. (comp `  C
) Y ) ( 2nd `  (  .1.  `  X ) ) )  =  ( 2nd `  F
) )
2019oteq3d 3933 . 2  |-  ( ph  -> 
<. X ,  Y , 
( ( 2nd `  F
) ( <. X ,  X >. (comp `  C
) Y ) ( 2nd `  (  .1.  `  X ) ) )
>.  =  <. X ,  Y ,  ( 2nd `  F ) >. )
21 arwlid.o . . 3  |-  .x.  =  (compa `  C )
221, 2, 6, 10, 4idahom 14135 . . 3  |-  ( ph  ->  (  .1.  `  X
)  e.  ( X H X ) )
2321, 4, 22, 3, 14coaval 14143 . 2  |-  ( ph  ->  ( F  .x.  (  .1.  `  X ) )  =  <. X ,  Y ,  ( ( 2nd `  F ) ( <. X ,  X >. (comp `  C ) Y ) ( 2nd `  (  .1.  `  X ) ) ) >. )
244homadmcd 14117 . . 3  |-  ( F  e.  ( X H Y )  ->  F  =  <. X ,  Y ,  ( 2nd `  F
) >. )
253, 24syl 16 . 2  |-  ( ph  ->  F  =  <. X ,  Y ,  ( 2nd `  F ) >. )
2620, 23, 253eqtr4d 2422 1  |-  ( ph  ->  ( F  .x.  (  .1.  `  X ) )  =  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   <.cop 3753   <.cotp 3754   ` cfv 5387  (class class class)co 6013   2ndc2nd 6280   Basecbs 13389    Hom chom 13460  compcco 13461   Catccat 13809   Idccid 13810  Homachoma 14098  Idacida 14128  compaccoa 14129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-rep 4254  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-reu 2649  df-rmo 2650  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-op 3759  df-ot 3760  df-uni 3951  df-iun 4030  df-br 4147  df-opab 4201  df-mpt 4202  df-id 4432  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-ov 6016  df-oprab 6017  df-mpt2 6018  df-1st 6281  df-2nd 6282  df-riota 6478  df-cat 13813  df-cid 13814  df-doma 14099  df-coda 14100  df-homa 14101  df-arw 14102  df-ida 14130  df-coa 14131
  Copyright terms: Public domain W3C validator