Metamath Proof Explorer

Theorem ghmeqker

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)

Ref Expression
Hypotheses ghmeqker.b ⊢B=BaseS
ghmeqker.z ⊢0˙=0T
ghmeqker.k ⊢K=F-10˙
ghmeqker.m ⊢-˙=-S
Assertion ghmeqker ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡U=F⁡V↔U-˙V∈K

Proof

Step Hyp Ref Expression
1 ghmeqker.b ⊢B=BaseS
2 ghmeqker.z ⊢0˙=0T
3 ghmeqker.k ⊢K=F-10˙
4 ghmeqker.m ⊢-˙=-S
5 2 sneqi ⊢0˙=0T
6 5 imaeq2i ⊢F-10˙=F-10T
7 3 6 eqtri ⊢K=F-10T
8 7 eleq2i ⊢U-˙V∈K↔U-˙V∈F-10T
9 eqid ⊢BaseT=BaseT
10 1 9 ghmf ⊢F∈SGrpHomT→F:B⟶BaseT
11 10 ffnd ⊢F∈SGrpHomT→FFnB
12 11 3ad2ant1 ⊢F∈SGrpHomT∧U∈B∧V∈B→FFnB
13 fniniseg ⊢FFnB→U-˙V∈F-10T↔U-˙V∈B∧F⁡U-˙V=0T
14 12 13 syl ⊢F∈SGrpHomT∧U∈B∧V∈B→U-˙V∈F-10T↔U-˙V∈B∧F⁡U-˙V=0T
15 8 14 bitrid ⊢F∈SGrpHomT∧U∈B∧V∈B→U-˙V∈K↔U-˙V∈B∧F⁡U-˙V=0T
16 ghmgrp1 ⊢F∈SGrpHomT→S∈Grp
17 1 4 grpsubcl ⊢S∈Grp∧U∈B∧V∈B→U-˙V∈B
18 16 17 syl3an1 ⊢F∈SGrpHomT∧U∈B∧V∈B→U-˙V∈B
19 18 biantrurd ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡U-˙V=0T↔U-˙V∈B∧F⁡U-˙V=0T
20 eqid ⊢-T=-T
21 1 4 20 ghmsub ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡U-˙V=F⁡U-TF⁡V
22 21 eqeq1d ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡U-˙V=0T↔F⁡U-TF⁡V=0T
23 19 22 bitr3d ⊢F∈SGrpHomT∧U∈B∧V∈B→U-˙V∈B∧F⁡U-˙V=0T↔F⁡U-TF⁡V=0T
24 ghmgrp2 ⊢F∈SGrpHomT→T∈Grp
25 24 3ad2ant1 ⊢F∈SGrpHomT∧U∈B∧V∈B→T∈Grp
26 10 3ad2ant1 ⊢F∈SGrpHomT∧U∈B∧V∈B→F:B⟶BaseT
27 simp2 ⊢F∈SGrpHomT∧U∈B∧V∈B→U∈B
28 26 27 ffvelcdmd ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡U∈BaseT
29 simp3 ⊢F∈SGrpHomT∧U∈B∧V∈B→V∈B
30 26 29 ffvelcdmd ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡V∈BaseT
31 eqid ⊢0T=0T
32 9 31 20 grpsubeq0 ⊢T∈Grp∧F⁡U∈BaseT∧F⁡V∈BaseT→F⁡U-TF⁡V=0T↔F⁡U=F⁡V
33 25 28 30 32 syl3anc ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡U-TF⁡V=0T↔F⁡U=F⁡V
34 15 23 33 3bitrrd ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡U=F⁡V↔U-˙V∈K