This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem homfeqval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses homfeqval.b 
|- B = ( Base ` C )
homfeqval.h 
|- H = ( Hom ` C )
homfeqval.j 
|- J = ( Hom ` D )
homfeqval.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
homfeqval.x 
|- ( ph -> X e. B )
homfeqval.y 
|- ( ph -> Y e. B )
Assertion homfeqval 
|- ( ph -> ( X H Y ) = ( X J Y ) )

Proof

Step Hyp Ref Expression
1 homfeqval.b 
 |-  B = ( Base ` C )
2 homfeqval.h 
 |-  H = ( Hom ` C )
3 homfeqval.j 
 |-  J = ( Hom ` D )
4 homfeqval.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
5 homfeqval.x 
 |-  ( ph -> X e. B )
6 homfeqval.y 
 |-  ( ph -> Y e. B )
7 4 oveqd 
 |-  ( ph -> ( X ( Homf ` C ) Y ) = ( X ( Homf ` D ) Y ) )
8 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
9 8 1 2 5 6 homfval 
 |-  ( ph -> ( X ( Homf ` C ) Y ) = ( X H Y ) )
10 eqid 
 |-  ( Homf ` D ) = ( Homf ` D )
11 eqid 
 |-  ( Base ` D ) = ( Base ` D )
12 4 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
13 1 12 eqtrid 
 |-  ( ph -> B = ( Base ` D ) )
14 5 13 eleqtrd 
 |-  ( ph -> X e. ( Base ` D ) )
15 6 13 eleqtrd 
 |-  ( ph -> Y e. ( Base ` D ) )
16 10 11 3 14 15 homfval 
 |-  ( ph -> ( X ( Homf ` D ) Y ) = ( X J Y ) )
17 7 9 16 3eqtr3d 
 |-  ( ph -> ( X H Y ) = ( X J Y ) )