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=BaseS
ghmsub.m ⊢-˙=-S
ghmsub.n ⊢N=-T
Assertion ghmsub ⊢F∈SGrpHomT∧U∈B∧V∈B→F⁡U-˙V=F⁡UNF⁡V

Proof

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