Theorem idghm

Description: The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014)

	Ref	Expression
Hypothesis	idghm.b	|- B = ( Base ` G )
Assertion	idghm	|- ( G e. Grp -> ( _I |` B ) e. ( G GrpHom G ) )

Proof

Step	Hyp	Ref	Expression
1		idghm.b	|- B = ( Base ` G )
2		id	|- ( G e. Grp -> G e. Grp )
3		eqid	|- ( +g ` G ) = ( +g ` G )
4	1 3	grpcl	|- ( ( G e. Grp /\ a e. B /\ b e. B ) -> ( a ( +g ` G ) b ) e. B )
5	4	3expb	|- ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` G ) b ) e. B )
6		fvresi	|- ( ( a ( +g ` G ) b ) e. B -> ( ( _I |` B ) ` ( a ( +g ` G ) b ) ) = ( a ( +g ` G ) b ) )
7	5 6	syl	|- ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` B ) ` ( a ( +g ` G ) b ) ) = ( a ( +g ` G ) b ) )
8		fvresi	|- ( a e. B -> ( ( _I |` B ) ` a ) = a )
9		fvresi	|- ( b e. B -> ( ( _I |` B ) ` b ) = b )
10	8 9	oveqan12d	|- ( ( a e. B /\ b e. B ) -> ( ( ( _I |` B ) ` a ) ( +g ` G ) ( ( _I |` B ) ` b ) ) = ( a ( +g ` G ) b ) )
11	10	adantl	|- ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> ( ( ( _I |` B ) ` a ) ( +g ` G ) ( ( _I |` B ) ` b ) ) = ( a ( +g ` G ) b ) )
12	7 11	eqtr4d	|- ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` B ) ` ( a ( +g ` G ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` G ) ( ( _I |` B ) ` b ) ) )
13	12	ralrimivva	|- ( G e. Grp -> A. a e. B A. b e. B ( ( _I |` B ) ` ( a ( +g ` G ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` G ) ( ( _I |` B ) ` b ) ) )
14		f1oi	|- ( _I |` B ) : B -1-1-onto-> B
15		f1of	|- ( ( _I |` B ) : B -1-1-onto-> B -> ( _I |` B ) : B --> B )
16	14 15	ax-mp	|- ( _I |` B ) : B --> B
17	13 16	jctil	|- ( G e. Grp -> ( ( _I |` B ) : B --> B /\ A. a e. B A. b e. B ( ( _I |` B ) ` ( a ( +g ` G ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` G ) ( ( _I |` B ) ` b ) ) ) )
18	1 1 3 3	isghm	|- ( ( _I |` B ) e. ( G GrpHom G ) <-> ( ( G e. Grp /\ G e. Grp ) /\ ( ( _I |` B ) : B --> B /\ A. a e. B A. b e. B ( ( _I |` B ) ` ( a ( +g ` G ) b ) ) = ( ( ( _I |` B ) ` a ) ( +g ` G ) ( ( _I |` B ) ` b ) ) ) ) )
19	2 2 17 18	syl21anbrc	|- ( G e. Grp -> ( _I |` B ) e. ( G GrpHom G ) )