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

Metamath Proof Explorer

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