# 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
`|- .- = ( -g ` S )`
ghmsub.n
`|- N = ( -g ` T )`
Assertion ghmsub
`|- ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` ( U .- V ) ) = ( ( F ` U ) N ( F ` V ) ) )`

### Proof

Step Hyp Ref Expression
1 ghmsub.b
` |-  B = ( Base ` S )`
2 ghmsub.m
` |-  .- = ( -g ` S )`
3 ghmsub.n
` |-  N = ( -g ` T )`
4 ghmgrp1
` |-  ( F e. ( S GrpHom T ) -> S e. Grp )`
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> S e. Grp )`
6 simp3
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> V e. B )`
7 eqid
` |-  ( invg ` S ) = ( invg ` S )`
8 1 7 grpinvcl
` |-  ( ( S e. Grp /\ V e. B ) -> ( ( invg ` S ) ` V ) e. B )`
9 5 6 8 syl2anc
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( invg ` S ) ` V ) e. B )`
10 eqid
` |-  ( +g ` S ) = ( +g ` S )`
11 eqid
` |-  ( +g ` T ) = ( +g ` T )`
12 1 10 11 ghmlin
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ ( ( invg ` S ) ` V ) e. B ) -> ( F ` ( U ( +g ` S ) ( ( invg ` S ) ` V ) ) ) = ( ( F ` U ) ( +g ` T ) ( F ` ( ( invg ` S ) ` V ) ) ) )`
13 9 12 syld3an3
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` ( U ( +g ` S ) ( ( invg ` S ) ` V ) ) ) = ( ( F ` U ) ( +g ` T ) ( F ` ( ( invg ` S ) ` V ) ) ) )`
14 eqid
` |-  ( invg ` T ) = ( invg ` T )`
15 1 7 14 ghminv
` |-  ( ( F e. ( S GrpHom T ) /\ V e. B ) -> ( F ` ( ( invg ` S ) ` V ) ) = ( ( invg ` T ) ` ( F ` V ) ) )`
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` ( ( invg ` S ) ` V ) ) = ( ( invg ` T ) ` ( F ` V ) ) )`
17 16 oveq2d
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( F ` U ) ( +g ` T ) ( F ` ( ( invg ` S ) ` V ) ) ) = ( ( F ` U ) ( +g ` T ) ( ( invg ` T ) ` ( F ` V ) ) ) )`
18 13 17 eqtrd
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` ( U ( +g ` S ) ( ( invg ` S ) ` V ) ) ) = ( ( F ` U ) ( +g ` T ) ( ( invg ` T ) ` ( F ` V ) ) ) )`
19 1 10 7 2 grpsubval
` |-  ( ( U e. B /\ V e. B ) -> ( U .- V ) = ( U ( +g ` S ) ( ( invg ` S ) ` V ) ) )`
20 19 fveq2d
` |-  ( ( U e. B /\ V e. B ) -> ( F ` ( U .- V ) ) = ( F ` ( U ( +g ` S ) ( ( invg ` S ) ` V ) ) ) )`
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` ( U .- V ) ) = ( F ` ( U ( +g ` S ) ( ( invg ` S ) ` V ) ) ) )`
22 eqid
` |-  ( Base ` T ) = ( Base ` T )`
23 1 22 ghmf
` |-  ( F e. ( S GrpHom T ) -> F : B --> ( Base ` T ) )`
24 ffvelrn
` |-  ( ( F : B --> ( Base ` T ) /\ U e. B ) -> ( F ` U ) e. ( Base ` T ) )`
25 ffvelrn
` |-  ( ( F : B --> ( Base ` T ) /\ V e. B ) -> ( F ` V ) e. ( Base ` T ) )`
26 24 25 anim12dan
` |-  ( ( F : B --> ( Base ` T ) /\ ( U e. B /\ V e. B ) ) -> ( ( F ` U ) e. ( Base ` T ) /\ ( F ` V ) e. ( Base ` T ) ) )`
27 23 26 sylan
` |-  ( ( F e. ( S GrpHom T ) /\ ( U e. B /\ V e. B ) ) -> ( ( F ` U ) e. ( Base ` T ) /\ ( F ` V ) e. ( Base ` T ) ) )`
28 27 3impb
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( F ` U ) e. ( Base ` T ) /\ ( F ` V ) e. ( Base ` T ) ) )`
29 22 11 14 3 grpsubval
` |-  ( ( ( F ` U ) e. ( Base ` T ) /\ ( F ` V ) e. ( Base ` T ) ) -> ( ( F ` U ) N ( F ` V ) ) = ( ( F ` U ) ( +g ` T ) ( ( invg ` T ) ` ( F ` V ) ) ) )`
30 28 29 syl
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( ( F ` U ) N ( F ` V ) ) = ( ( F ` U ) ( +g ` T ) ( ( invg ` T ) ` ( F ` V ) ) ) )`
31 18 21 30 3eqtr4d
` |-  ( ( F e. ( S GrpHom T ) /\ U e. B /\ V e. B ) -> ( F ` ( U .- V ) ) = ( ( F ` U ) N ( F ` V ) ) )`