Metamath Proof Explorer


Theorem isghmd

Description: Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015)

Ref Expression
Hypotheses isghmd.x X=BaseS
isghmd.y Y=BaseT
isghmd.a +˙=+S
isghmd.b ˙=+T
isghmd.s φSGrp
isghmd.t φTGrp
isghmd.f φF:XY
isghmd.l φxXyXFx+˙y=Fx˙Fy
Assertion isghmd φFSGrpHomT

Proof

Step Hyp Ref Expression
1 isghmd.x X=BaseS
2 isghmd.y Y=BaseT
3 isghmd.a +˙=+S
4 isghmd.b ˙=+T
5 isghmd.s φSGrp
6 isghmd.t φTGrp
7 isghmd.f φF:XY
8 isghmd.l φxXyXFx+˙y=Fx˙Fy
9 8 ralrimivva φxXyXFx+˙y=Fx˙Fy
10 7 9 jca φF:XYxXyXFx+˙y=Fx˙Fy
11 1 2 3 4 isghm FSGrpHomTSGrpTGrpF:XYxXyXFx+˙y=Fx˙Fy
12 5 6 10 11 syl21anbrc φFSGrpHomT