Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ghmeqker Structured version   Unicode version

Theorem ghmeqker 15034
 Description: Two source points map to the same destination point under a group homomorphism iff their difference belongs to the kernel. (Contributed by Stefan O'Rear, 31-Dec-2014.)
Hypotheses
Ref Expression
ghmeqker.b
ghmeqker.z
ghmeqker.k
ghmeqker.m
Assertion
Ref Expression
ghmeqker

Proof of Theorem ghmeqker
StepHypRef Expression
1 ghmeqker.k . . . . 5
2 ghmeqker.z . . . . . . 7
32sneqi 3828 . . . . . 6
43imaeq2i 5203 . . . . 5
51, 4eqtri 2458 . . . 4
65eleq2i 2502 . . 3
7 ghmeqker.b . . . . . . 7
8 eqid 2438 . . . . . . 7
97, 8ghmf 15012 . . . . . 6
10 ffn 5593 . . . . . 6
119, 10syl 16 . . . . 5
12113ad2ant1 979 . . . 4
13 fniniseg 5853 . . . 4
1412, 13syl 16 . . 3
156, 14syl5bb 250 . 2
16 ghmgrp1 15010 . . . . 5
17 ghmeqker.m . . . . . 6
187, 17grpsubcl 14871 . . . . 5
1916, 18syl3an1 1218 . . . 4
2019biantrurd 496 . . 3
21 eqid 2438 . . . . 5
227, 17, 21ghmsub 15016 . . . 4
2322eqeq1d 2446 . . 3
2420, 23bitr3d 248 . 2
25 ghmgrp2 15011 . . . 4