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	⊢ 𝐵 = ( Base ‘ 𝑆 )
	ghmeqker.z	⊢ 0 = ( 0g ‘ 𝑇 )
	ghmeqker.k	⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
	ghmeqker.m	⊢ − = ( -g ‘ 𝑆 )
Assertion	ghmeqker	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) ↔ ( 𝑈 − 𝑉 ) ∈ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		ghmeqker.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
2		ghmeqker.z	⊢ 0 = ( 0g ‘ 𝑇 )
3		ghmeqker.k	⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4		ghmeqker.m	⊢ − = ( -g ‘ 𝑆 )
5	2	sneqi	⊢ { 0 } = { ( 0g ‘ 𝑇 ) }
6	5	imaeq2i	⊢ ( ◡ 𝐹 “ { 0 } ) = ( ◡ 𝐹 “ { ( 0g ‘ 𝑇 ) } )
7	3 6	eqtri	⊢ 𝐾 = ( ◡ 𝐹 “ { ( 0g ‘ 𝑇 ) } )
8	7	eleq2i	⊢ ( ( 𝑈 − 𝑉 ) ∈ 𝐾 ↔ ( 𝑈 − 𝑉 ) ∈ ( ◡ 𝐹 “ { ( 0g ‘ 𝑇 ) } ) )
9		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
10	1 9	ghmf	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
11	10	ffnd	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 Fn 𝐵 )
12	11	3ad2ant1	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → 𝐹 Fn 𝐵 )
13		fniniseg	⊢ ( 𝐹 Fn 𝐵 → ( ( 𝑈 − 𝑉 ) ∈ ( ◡ 𝐹 “ { ( 0g ‘ 𝑇 ) } ) ↔ ( ( 𝑈 − 𝑉 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝑈 − 𝑉 ) ) = ( 0g ‘ 𝑇 ) ) ) )
14	12 13	syl	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝑈 − 𝑉 ) ∈ ( ◡ 𝐹 “ { ( 0g ‘ 𝑇 ) } ) ↔ ( ( 𝑈 − 𝑉 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝑈 − 𝑉 ) ) = ( 0g ‘ 𝑇 ) ) ) )
15	8 14	bitrid	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝑈 − 𝑉 ) ∈ 𝐾 ↔ ( ( 𝑈 − 𝑉 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝑈 − 𝑉 ) ) = ( 0g ‘ 𝑇 ) ) ) )
16		ghmgrp1	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
17	1 4	grpsubcl	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑈 − 𝑉 ) ∈ 𝐵 )
18	16 17	syl3an1	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑈 − 𝑉 ) ∈ 𝐵 )
19	18	biantrurd	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝑈 − 𝑉 ) ) = ( 0g ‘ 𝑇 ) ↔ ( ( 𝑈 − 𝑉 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝑈 − 𝑉 ) ) = ( 0g ‘ 𝑇 ) ) ) )
20		eqid	⊢ ( -g ‘ 𝑇 ) = ( -g ‘ 𝑇 )
21	1 4 20	ghmsub	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑈 − 𝑉 ) ) = ( ( 𝐹 ‘ 𝑈 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑉 ) ) )
22	21	eqeq1d	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝑈 − 𝑉 ) ) = ( 0g ‘ 𝑇 ) ↔ ( ( 𝐹 ‘ 𝑈 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑉 ) ) = ( 0g ‘ 𝑇 ) ) )
23	19 22	bitr3d	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( ( 𝑈 − 𝑉 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝑈 − 𝑉 ) ) = ( 0g ‘ 𝑇 ) ) ↔ ( ( 𝐹 ‘ 𝑈 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑉 ) ) = ( 0g ‘ 𝑇 ) ) )
24		ghmgrp2	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑇 ∈ Grp )
25	24	3ad2ant1	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → 𝑇 ∈ Grp )
26	10	3ad2ant1	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
27		simp2	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → 𝑈 ∈ 𝐵 )
28	26 27	ffvelcdmd	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑈 ) ∈ ( Base ‘ 𝑇 ) )
29		simp3	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → 𝑉 ∈ 𝐵 )
30	26 29	ffvelcdmd	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑉 ) ∈ ( Base ‘ 𝑇 ) )
31		eqid	⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
32	9 31 20	grpsubeq0	⊢ ( ( 𝑇 ∈ Grp ∧ ( 𝐹 ‘ 𝑈 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐹 ‘ 𝑉 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( ( 𝐹 ‘ 𝑈 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑉 ) ) = ( 0g ‘ 𝑇 ) ↔ ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) ) )
33	25 28 30 32	syl3anc	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑈 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝑉 ) ) = ( 0g ‘ 𝑇 ) ↔ ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) ) )
34	15 23 33	3bitrrd	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) ↔ ( 𝑈 − 𝑉 ) ∈ 𝐾 ) )