This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( 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 𝑇 ) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) ↔ ( 𝑈 − 𝑉 ) ∈ 𝐾 ) )