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=BaseG
Assertion idghm GGrpIBGGrpHomG

Proof

Step Hyp Ref Expression
1 idghm.b B=BaseG
2 id GGrpGGrp
3 eqid +G=+G
4 1 3 grpcl GGrpaBbBa+GbB
5 4 3expb GGrpaBbBa+GbB
6 fvresi a+GbBIBa+Gb=a+Gb
7 5 6 syl GGrpaBbBIBa+Gb=a+Gb
8 fvresi aBIBa=a
9 fvresi bBIBb=b
10 8 9 oveqan12d aBbBIBa+GIBb=a+Gb
11 10 adantl GGrpaBbBIBa+GIBb=a+Gb
12 7 11 eqtr4d GGrpaBbBIBa+Gb=IBa+GIBb
13 12 ralrimivva GGrpaBbBIBa+Gb=IBa+GIBb
14 f1oi IB:B1-1 ontoB
15 f1of IB:B1-1 ontoBIB:BB
16 14 15 ax-mp IB:BB
17 13 16 jctil GGrpIB:BBaBbBIBa+Gb=IBa+GIBb
18 1 1 3 3 isghm IBGGrpHomGGGrpGGrpIB:BBaBbBIBa+Gb=IBa+GIBb
19 2 2 17 18 syl21anbrc GGrpIBGGrpHomG