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 = ( Base ` S )
ghmeqker.z 
|- .0. = ( 0g ` T )
ghmeqker.k 
|- K = ( `' F " { .0. } )
ghmeqker.m 
|- .- = ( -g ` S )
Assertion ghmeqker 
|- ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( F ` U ) = ( F ` V ) <-> ( U .- V ) e. K ) )

Proof

Step Hyp Ref Expression
1 ghmeqker.b 
 |-  B = ( Base ` S )
2 ghmeqker.z 
 |-  .0. = ( 0g ` T )
3 ghmeqker.k 
 |-  K = ( `' F " { .0. } )
4 ghmeqker.m 
 |-  .- = ( -g ` S )
5 2 sneqi 
 |-  { .0. } = { ( 0g ` T ) }
6 5 imaeq2i 
 |-  ( `' F " { .0. } ) = ( `' F " { ( 0g ` T ) } )
7 3 6 eqtri 
 |-  K = ( `' F " { ( 0g ` T ) } )
8 7 eleq2i 
 |-  ( ( U .- V ) e. K <-> ( U .- V ) e. ( `' F " { ( 0g ` T ) } ) )
9 eqid 
 |-  ( Base ` T ) = ( Base ` T )
10 1 9 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : B --> ( Base ` T ) )
11 10 ffnd 
 |-  ( F e. ( S GrpHom T ) -> F Fn B )
12 11 3ad2ant1 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> F Fn B )
13 fniniseg 
 |-  ( F Fn B -> ( ( U .- V ) e. ( `' F " { ( 0g ` T ) } ) <-> ( ( U .- V ) e. B /\ ( F ` ( U .- V ) ) = ( 0g ` T ) ) ) )
14 12 13 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( U .- V ) e. ( `' F " { ( 0g ` T ) } ) <-> ( ( U .- V ) e. B /\ ( F ` ( U .- V ) ) = ( 0g ` T ) ) ) )
15 8 14 syl5bb 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( U .- V ) e. K <-> ( ( U .- V ) e. B /\ ( F ` ( U .- V ) ) = ( 0g ` T ) ) ) )
16 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
17 1 4 grpsubcl 
 |-  ( ( S e. Grp /\ U e. B /\ V e. B ) -> ( U .- V ) e. B )
18 16 17 syl3an1 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( U .- V ) e. B )
19 18 biantrurd 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( F ` ( U .- V ) ) = ( 0g ` T ) <-> ( ( U .- V ) e. B /\ ( F ` ( U .- V ) ) = ( 0g ` T ) ) ) )
20 eqid 
 |-  ( -g ` T ) = ( -g ` T )
21 1 4 20 ghmsub 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` ( U .- V ) ) = ( ( F ` U ) ( -g ` T ) ( F ` V ) ) )
22 21 eqeq1d 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( F ` ( U .- V ) ) = ( 0g ` T ) <-> ( ( F ` U ) ( -g ` T ) ( F ` V ) ) = ( 0g ` T ) ) )
23 19 22 bitr3d 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( ( U .- V ) e. B /\ ( F ` ( U .- V ) ) = ( 0g ` T ) ) <-> ( ( F ` U ) ( -g ` T ) ( F ` V ) ) = ( 0g ` T ) ) )
24 ghmgrp2 
 |-  ( F e. ( S GrpHom T ) -> T e. Grp )
25 24 3ad2ant1 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> T e. Grp )
26 10 3ad2ant1 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> F : B --> ( Base ` T ) )
27 simp2 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> U e. B )
28 26 27 ffvelrnd 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` U ) e. ( Base ` T ) )
29 simp3 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> V e. B )
30 26 29 ffvelrnd 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` V ) e. ( Base ` T ) )
31 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
32 9 31 20 grpsubeq0 
 |-  ( ( T e. Grp /\ ( F ` U ) e. ( Base ` T ) /\ ( F ` V ) e. ( Base ` T ) ) -> ( ( ( F ` U ) ( -g ` T ) ( F ` V ) ) = ( 0g ` T ) <-> ( F ` U ) = ( F ` V ) ) )
33 25 28 30 32 syl3anc 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( ( F ` U ) ( -g ` T ) ( F ` V ) ) = ( 0g ` T ) <-> ( F ` U ) = ( F ` V ) ) )
34 15 23 33 3bitrrd 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( F ` U ) = ( F ` V ) <-> ( U .- V ) e. K ) )