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={\mathrm{Base}}_S$$
	ghmeqker.z	$$⊢\underset{\dot{}}{0}=0_T$$
	ghmeqker.k	$$⊢K=F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
	ghmeqker.m	$$⊢\underset{\dot{}}{-}={-}_S$$
Assertion	ghmeqker	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to \left(F\left(U\right)=F\left(V\right)\leftrightarrow U\underset{\dot{}}{-}V\in K\right)$$

Proof

Step	Hyp	Ref	Expression
1		ghmeqker.b	$$⊢B={\mathrm{Base}}_S$$
2		ghmeqker.z	$$⊢\underset{\dot{}}{0}=0_T$$
3		ghmeqker.k	$$⊢K=F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
4		ghmeqker.m	$$⊢\underset{\dot{}}{-}={-}_S$$
5	2	sneqi	$$⊢\left\{\underset{\dot{}}{0}\right\}=\left\{0_T\right\}$$
6	5	imaeq2i	$$⊢F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=F^{-1}\left[\left\{0_T\right\}\right]$$
7	3 6	eqtri	$$⊢K=F^{-1}\left[\left\{0_T\right\}\right]$$
8	7	eleq2i	$$⊢U\underset{\dot{}}{-}V\in K\leftrightarrow U\underset{\dot{}}{-}V\in F^{-1}\left[\left\{0_T\right\}\right]$$
9		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
10	1 9	ghmf	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F:B⟶{\mathrm{Base}}_T$$
11	10	ffnd	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to FFnB$$
12	11	3ad2ant1	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to FFnB$$
13		fniniseg	$$⊢FFnB\to \left(U\underset{\dot{}}{-}V\in F^{-1}\left[\left\{0_T\right\}\right]\leftrightarrow \left(U\underset{\dot{}}{-}V\in B\wedge F\left(U\underset{\dot{}}{-}V\right)=0_T\right)\right)$$
14	12 13	syl	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to \left(U\underset{\dot{}}{-}V\in F^{-1}\left[\left\{0_T\right\}\right]\leftrightarrow \left(U\underset{\dot{}}{-}V\in B\wedge F\left(U\underset{\dot{}}{-}V\right)=0_T\right)\right)$$
15	8 14	bitrid	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to \left(U\underset{\dot{}}{-}V\in K\leftrightarrow \left(U\underset{\dot{}}{-}V\in B\wedge F\left(U\underset{\dot{}}{-}V\right)=0_T\right)\right)$$
16		ghmgrp1	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to S\in \mathrm{Grp}$$
17	1 4	grpsubcl	$$⊢\left(S\in \mathrm{Grp}\wedge U\in B\wedge V\in B\right)\to U\underset{\dot{}}{-}V\in B$$
18	16 17	syl3an1	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to U\underset{\dot{}}{-}V\in B$$
19	18	biantrurd	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to \left(F\left(U\underset{\dot{}}{-}V\right)=0_T\leftrightarrow \left(U\underset{\dot{}}{-}V\in B\wedge F\left(U\underset{\dot{}}{-}V\right)=0_T\right)\right)$$
20		eqid	$$⊢{-}_T={-}_T$$
21	1 4 20	ghmsub	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to F\left(U\underset{\dot{}}{-}V\right)=F\left(U\right){-}_{T}F\left(V\right)$$
22	21	eqeq1d	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to \left(F\left(U\underset{\dot{}}{-}V\right)=0_T\leftrightarrow F\left(U\right){-}_{T}F\left(V\right)=0_T\right)$$
23	19 22	bitr3d	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to \left(\left(U\underset{\dot{}}{-}V\in B\wedge F\left(U\underset{\dot{}}{-}V\right)=0_T\right)\leftrightarrow F\left(U\right){-}_{T}F\left(V\right)=0_T\right)$$
24		ghmgrp2	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to T\in \mathrm{Grp}$$
25	24	3ad2ant1	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to T\in \mathrm{Grp}$$
26	10	3ad2ant1	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to F:B⟶{\mathrm{Base}}_T$$
27		simp2	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to U\in B$$
28	26 27	ffvelcdmd	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to F\left(U\right)\in {\mathrm{Base}}_T$$
29		simp3	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to V\in B$$
30	26 29	ffvelcdmd	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to F\left(V\right)\in {\mathrm{Base}}_T$$
31		eqid	$$⊢0_T=0_T$$
32	9 31 20	grpsubeq0	$$⊢\left(T\in \mathrm{Grp}\wedge F\left(U\right)\in {\mathrm{Base}}_T\wedge F\left(V\right)\in {\mathrm{Base}}_T\right)\to \left(F\left(U\right){-}_{T}F\left(V\right)=0_T\leftrightarrow F\left(U\right)=F\left(V\right)\right)$$
33	25 28 30 32	syl3anc	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to \left(F\left(U\right){-}_{T}F\left(V\right)=0_T\leftrightarrow F\left(U\right)=F\left(V\right)\right)$$
34	15 23 33	3bitrrd	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in B\wedge V\in B\right)\to \left(F\left(U\right)=F\left(V\right)\leftrightarrow U\underset{\dot{}}{-}V\in K\right)$$