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

Metamath Proof Explorer

Theorem isohom

Description: An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses isohom.b 
|- B = ( Base ` C )
isohom.h 
|- H = ( Hom ` C )
isohom.i 
|- I = ( Iso ` C )
isohom.c 
|- ( ph -> C e. Cat )
isohom.x 
|- ( ph -> X e. B )
isohom.y 
|- ( ph -> Y e. B )
Assertion isohom 
|- ( ph -> ( X I Y ) C_ ( X H Y ) )

Proof

Step Hyp Ref Expression
1 isohom.b 
 |-  B = ( Base ` C )
2 isohom.h 
 |-  H = ( Hom ` C )
3 isohom.i 
 |-  I = ( Iso ` C )
4 isohom.c 
 |-  ( ph -> C e. Cat )
5 isohom.x 
 |-  ( ph -> X e. B )
6 isohom.y 
 |-  ( ph -> Y e. B )
7 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
8 1 7 4 5 6 3 isoval 
 |-  ( ph -> ( X I Y ) = dom ( X ( Inv ` C ) Y ) )
9 1 7 4 5 6 2 invss 
 |-  ( ph -> ( X ( Inv ` C ) Y ) C_ ( ( X H Y ) X. ( Y H X ) ) )
10 dmss 
 |-  ( ( X ( Inv ` C ) Y ) C_ ( ( X H Y ) X. ( Y H X ) ) -> dom ( X ( Inv ` C ) Y ) C_ dom ( ( X H Y ) X. ( Y H X ) ) )
11 9 10 syl 
 |-  ( ph -> dom ( X ( Inv ` C ) Y ) C_ dom ( ( X H Y ) X. ( Y H X ) ) )
12 8 11 eqsstrd 
 |-  ( ph -> ( X I Y ) C_ dom ( ( X H Y ) X. ( Y H X ) ) )
13 dmxpss 
 |-  dom ( ( X H Y ) X. ( Y H X ) ) C_ ( X H Y )
14 12 13 sstrdi 
 |-  ( ph -> ( X I Y ) C_ ( X H Y ) )