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

Theorem ghmeqker 14709
 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 3652 . . . . . 6
43imaeq2i 5010 . . . . 5
51, 4eqtri 2303 . . . 4
65eleq2i 2347 . . 3
7 ghmeqker.b . . . . . . 7
8 eqid 2283 . . . . . . 7
97, 8ghmf 14687 . . . . . 6
10 ffn 5389 . . . . . 6
119, 10syl 15 . . . . 5
12113ad2ant1 976 . . . 4
13 fniniseg 5646 . . . 4
1412, 13syl 15 . . 3
156, 14syl5bb 248 . 2
16 ghmgrp1 14685 . . . . 5
17 ghmeqker.m . . . . . 6
187, 17grpsubcl 14546 . . . . 5
1916, 18syl3an1 1215 . . . 4
2019biantrurd 494 . . 3
21 eqid 2283 . . . . 5
227, 17, 21ghmsub 14691 . . . 4
2322eqeq1d 2291 . . 3
2420, 23bitr3d 246 . 2
25 ghmgrp2 14686 . . . 4