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

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 )
5 4 3ad2ant1 
 |-  ( ( 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 ) ) )
16 15 3adant2 
 |-  ( ( 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 ) ) ) )
21 20 3adant1 
 |-  ( ( 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 ffvelcdm 
 |-  ( ( F : B --> ( Base ` T ) /\ U e. B ) -> ( F ` U ) e. ( Base ` T ) )
25 ffvelcdm 
 |-  ( ( 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 ) ) )