Metamath Proof Explorer

Theorem ghmsub

Description: Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Hypotheses ghmsub.b ⊢ B = Base S
ghmsub.m ⊢ - ˙ = - S
ghmsub.n ⊢ N = - T
Assertion ghmsub ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U - ˙ V = F ⁡ U N F ⁡ V

Proof

Step Hyp Ref Expression
1 ghmsub.b ⊢ B = Base S
2 ghmsub.m ⊢ - ˙ = - S
3 ghmsub.n ⊢ N = - T
4 ghmgrp1 ⊢ F ∈ S GrpHom T → S ∈ Grp
5 4 3ad2ant1 ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → S ∈ Grp
6 simp3 ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → V ∈ B
7 eqid ⊢ inv g ⁡ S = inv g ⁡ S
8 1 7 grpinvcl ⊢ S ∈ Grp ∧ V ∈ B → inv g ⁡ S ⁡ V ∈ B
9 5 6 8 syl2anc ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → inv g ⁡ S ⁡ V ∈ B
10 eqid ⊢ + S = + S
11 eqid ⊢ + T = + T
12 1 10 11 ghmlin ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ inv g ⁡ S ⁡ V ∈ B → F ⁡ U + S inv g ⁡ S ⁡ V = F ⁡ U + T F ⁡ inv g ⁡ S ⁡ V
13 9 12 syld3an3 ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U + S inv g ⁡ S ⁡ V = F ⁡ U + T F ⁡ inv g ⁡ S ⁡ V
14 eqid ⊢ inv g ⁡ T = inv g ⁡ T
15 1 7 14 ghminv ⊢ F ∈ S GrpHom T ∧ V ∈ B → F ⁡ inv g ⁡ S ⁡ V = inv g ⁡ T ⁡ F ⁡ V
16 15 3adant2 ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ inv g ⁡ S ⁡ V = inv g ⁡ T ⁡ F ⁡ V
17 16 oveq2d ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U + T F ⁡ inv g ⁡ S ⁡ V = F ⁡ U + T inv g ⁡ T ⁡ F ⁡ V
18 13 17 eqtrd ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U + S inv g ⁡ S ⁡ V = F ⁡ U + T inv g ⁡ T ⁡ F ⁡ V
19 1 10 7 2 grpsubval ⊢ U ∈ B ∧ V ∈ B → U - ˙ V = U + S inv g ⁡ S ⁡ V
20 19 fveq2d ⊢ U ∈ B ∧ V ∈ B → F ⁡ U - ˙ V = F ⁡ U + S inv g ⁡ S ⁡ V
21 20 3adant1 ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U - ˙ V = F ⁡ U + S inv g ⁡ S ⁡ V
22 eqid ⊢ Base T = Base T
23 1 22 ghmf ⊢ F ∈ S GrpHom T → F : B ⟶ Base T
24 ffvelrn ⊢ F : B ⟶ Base T ∧ U ∈ B → F ⁡ U ∈ Base T
25 ffvelrn ⊢ F : B ⟶ Base T ∧ V ∈ B → F ⁡ V ∈ Base T
26 24 25 anim12dan ⊢ F : B ⟶ Base T ∧ U ∈ B ∧ V ∈ B → F ⁡ U ∈ Base T ∧ F ⁡ V ∈ Base T
27 23 26 sylan ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U ∈ Base T ∧ F ⁡ V ∈ Base T
28 27 3impb ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U ∈ Base T ∧ F ⁡ V ∈ Base T
29 22 11 14 3 grpsubval ⊢ F ⁡ U ∈ Base T ∧ F ⁡ V ∈ Base T → F ⁡ U N F ⁡ V = F ⁡ U + T inv g ⁡ T ⁡ F ⁡ V
30 28 29 syl ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U N F ⁡ V = F ⁡ U + T inv g ⁡ T ⁡ F ⁡ V
31 18 21 30 3eqtr4d ⊢ F ∈ S GrpHom T ∧ U ∈ B ∧ V ∈ B → F ⁡ U - ˙ V = F ⁡ U N F ⁡ V