# 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}={\mathrm{Base}}_{{S}}$
ghmsub.m
ghmsub.n ${⊢}{N}={-}_{{T}}$
Assertion ghmsub

### Proof

Step Hyp Ref Expression
1 ghmsub.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
2 ghmsub.m
3 ghmsub.n ${⊢}{N}={-}_{{T}}$
4 ghmgrp1 ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {S}\in \mathrm{Grp}$
5 4 3ad2ant1 ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to {S}\in \mathrm{Grp}$
6 simp3 ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to {V}\in {B}$
7 eqid ${⊢}{inv}_{g}\left({S}\right)={inv}_{g}\left({S}\right)$
8 1 7 grpinvcl ${⊢}\left({S}\in \mathrm{Grp}\wedge {V}\in {B}\right)\to {inv}_{g}\left({S}\right)\left({V}\right)\in {B}$
9 5 6 8 syl2anc ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to {inv}_{g}\left({S}\right)\left({V}\right)\in {B}$
10 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
11 eqid ${⊢}{+}_{{T}}={+}_{{T}}$
12 1 10 11 ghmlin ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {inv}_{g}\left({S}\right)\left({V}\right)\in {B}\right)\to {F}\left({U}{+}_{{S}}{inv}_{g}\left({S}\right)\left({V}\right)\right)={F}\left({U}\right){+}_{{T}}{F}\left({inv}_{g}\left({S}\right)\left({V}\right)\right)$
13 9 12 syld3an3 ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to {F}\left({U}{+}_{{S}}{inv}_{g}\left({S}\right)\left({V}\right)\right)={F}\left({U}\right){+}_{{T}}{F}\left({inv}_{g}\left({S}\right)\left({V}\right)\right)$
14 eqid ${⊢}{inv}_{g}\left({T}\right)={inv}_{g}\left({T}\right)$
15 1 7 14 ghminv ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {V}\in {B}\right)\to {F}\left({inv}_{g}\left({S}\right)\left({V}\right)\right)={inv}_{g}\left({T}\right)\left({F}\left({V}\right)\right)$
16 15 3adant2 ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to {F}\left({inv}_{g}\left({S}\right)\left({V}\right)\right)={inv}_{g}\left({T}\right)\left({F}\left({V}\right)\right)$
17 16 oveq2d ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to {F}\left({U}\right){+}_{{T}}{F}\left({inv}_{g}\left({S}\right)\left({V}\right)\right)={F}\left({U}\right){+}_{{T}}{inv}_{g}\left({T}\right)\left({F}\left({V}\right)\right)$
18 13 17 eqtrd ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to {F}\left({U}{+}_{{S}}{inv}_{g}\left({S}\right)\left({V}\right)\right)={F}\left({U}\right){+}_{{T}}{inv}_{g}\left({T}\right)\left({F}\left({V}\right)\right)$
19 1 10 7 2 grpsubval
20 19 fveq2d
22 eqid ${⊢}{\mathrm{Base}}_{{T}}={\mathrm{Base}}_{{T}}$
23 1 22 ghmf ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {F}:{B}⟶{\mathrm{Base}}_{{T}}$
24 ffvelrn ${⊢}\left({F}:{B}⟶{\mathrm{Base}}_{{T}}\wedge {U}\in {B}\right)\to {F}\left({U}\right)\in {\mathrm{Base}}_{{T}}$
25 ffvelrn ${⊢}\left({F}:{B}⟶{\mathrm{Base}}_{{T}}\wedge {V}\in {B}\right)\to {F}\left({V}\right)\in {\mathrm{Base}}_{{T}}$
26 24 25 anim12dan ${⊢}\left({F}:{B}⟶{\mathrm{Base}}_{{T}}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\to \left({F}\left({U}\right)\in {\mathrm{Base}}_{{T}}\wedge {F}\left({V}\right)\in {\mathrm{Base}}_{{T}}\right)$
27 23 26 sylan ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\to \left({F}\left({U}\right)\in {\mathrm{Base}}_{{T}}\wedge {F}\left({V}\right)\in {\mathrm{Base}}_{{T}}\right)$
28 27 3impb ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to \left({F}\left({U}\right)\in {\mathrm{Base}}_{{T}}\wedge {F}\left({V}\right)\in {\mathrm{Base}}_{{T}}\right)$
29 22 11 14 3 grpsubval ${⊢}\left({F}\left({U}\right)\in {\mathrm{Base}}_{{T}}\wedge {F}\left({V}\right)\in {\mathrm{Base}}_{{T}}\right)\to {F}\left({U}\right){N}{F}\left({V}\right)={F}\left({U}\right){+}_{{T}}{inv}_{g}\left({T}\right)\left({F}\left({V}\right)\right)$
30 28 29 syl ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {U}\in {B}\wedge {V}\in {B}\right)\to {F}\left({U}\right){N}{F}\left({V}\right)={F}\left({U}\right){+}_{{T}}{inv}_{g}\left({T}\right)\left({F}\left({V}\right)\right)$