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 ) )