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