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

Metamath Proof Explorer

Theorem ghmmulg

Description: A group homomorphism preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses ghmmulg.b 
|- B = ( Base ` G )
ghmmulg.s 
|- .x. = ( .g ` G )
ghmmulg.t 
|- .X. = ( .g ` H )
Assertion ghmmulg 
|- ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )

Proof

Step Hyp Ref Expression
1 ghmmulg.b 
 |-  B = ( Base ` G )
2 ghmmulg.s 
 |-  .x. = ( .g ` G )
3 ghmmulg.t 
 |-  .X. = ( .g ` H )
4 ghmmhm 
 |-  ( F e. ( G GrpHom H ) -> F e. ( G MndHom H ) )
5 1 2 3 mhmmulg 
 |-  ( ( F e. ( G MndHom H ) /\ N e. NN0 /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
6 4 5 syl3an1 
 |-  ( ( F e. ( G GrpHom H ) /\ N e. NN0 /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
7 6 3expa 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. NN0 ) /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
8 7 an32s 
 |-  ( ( ( F e. ( G GrpHom H ) /\ X e. B ) /\ N e. NN0 ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
9 8 3adantl2 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ N e. NN0 ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
10 simpl1 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> F e. ( G GrpHom H ) )
11 10 4 syl 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> F e. ( G MndHom H ) )
12 nnnn0 
 |-  ( -u N e. NN -> -u N e. NN0 )
13 12 ad2antll 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN0 )
14 simpl3 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> X e. B )
15 1 2 3 mhmmulg 
 |-  ( ( F e. ( G MndHom H ) /\ -u N e. NN0 /\ X e. B ) -> ( F ` ( -u N .x. X ) ) = ( -u N .X. ( F ` X ) ) )
16 11 13 14 15 syl3anc 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( F ` ( -u N .x. X ) ) = ( -u N .X. ( F ` X ) ) )
17 16 fveq2d 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( invg ` H ) ` ( F ` ( -u N .x. X ) ) ) = ( ( invg ` H ) ` ( -u N .X. ( F ` X ) ) ) )
18 ghmgrp1 
 |-  ( F e. ( G GrpHom H ) -> G e. Grp )
19 10 18 syl 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> G e. Grp )
20 nnz 
 |-  ( -u N e. NN -> -u N e. ZZ )
21 20 ad2antll 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. ZZ )
22 1 2 mulgcl 
 |-  ( ( G e. Grp /\ -u N e. ZZ /\ X e. B ) -> ( -u N .x. X ) e. B )
23 19 21 14 22 syl3anc 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u N .x. X ) e. B )
24 eqid 
 |-  ( invg ` G ) = ( invg ` G )
25 eqid 
 |-  ( invg ` H ) = ( invg ` H )
26 1 24 25 ghminv 
 |-  ( ( F e. ( G GrpHom H ) /\ ( -u N .x. X ) e. B ) -> ( F ` ( ( invg ` G ) ` ( -u N .x. X ) ) ) = ( ( invg ` H ) ` ( F ` ( -u N .x. X ) ) ) )
27 10 23 26 syl2anc 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( F ` ( ( invg ` G ) ` ( -u N .x. X ) ) ) = ( ( invg ` H ) ` ( F ` ( -u N .x. X ) ) ) )
28 ghmgrp2 
 |-  ( F e. ( G GrpHom H ) -> H e. Grp )
29 10 28 syl 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> H e. Grp )
30 eqid 
 |-  ( Base ` H ) = ( Base ` H )
31 1 30 ghmf 
 |-  ( F e. ( G GrpHom H ) -> F : B --> ( Base ` H ) )
32 10 31 syl 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> F : B --> ( Base ` H ) )
33 32 14 ffvelcdmd 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( F ` X ) e. ( Base ` H ) )
34 30 3 25 mulgneg 
 |-  ( ( H e. Grp /\ -u N e. ZZ /\ ( F ` X ) e. ( Base ` H ) ) -> ( -u -u N .X. ( F ` X ) ) = ( ( invg ` H ) ` ( -u N .X. ( F ` X ) ) ) )
35 29 21 33 34 syl3anc 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .X. ( F ` X ) ) = ( ( invg ` H ) ` ( -u N .X. ( F ` X ) ) ) )
36 17 27 35 3eqtr4d 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( F ` ( ( invg ` G ) ` ( -u N .x. X ) ) ) = ( -u -u N .X. ( F ` X ) ) )
37 1 2 24 mulgneg 
 |-  ( ( G e. Grp /\ -u N e. ZZ /\ X e. B ) -> ( -u -u N .x. X ) = ( ( invg ` G ) ` ( -u N .x. X ) ) )
38 19 21 14 37 syl3anc 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .x. X ) = ( ( invg ` G ) ` ( -u N .x. X ) ) )
39 simprl 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. RR )
40 39 recnd 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. CC )
41 40 negnegd 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u -u N = N )
42 41 oveq1d 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .x. X ) = ( N .x. X ) )
43 38 42 eqtr3d 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( invg ` G ) ` ( -u N .x. X ) ) = ( N .x. X ) )
44 43 fveq2d 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( F ` ( ( invg ` G ) ` ( -u N .x. X ) ) ) = ( F ` ( N .x. X ) ) )
45 36 44 eqtr3d 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .X. ( F ` X ) ) = ( F ` ( N .x. X ) ) )
46 41 oveq1d 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .X. ( F ` X ) ) = ( N .X. ( F ` X ) ) )
47 45 46 eqtr3d 
 |-  ( ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )
48 simp2 
 |-  ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) -> N e. ZZ )
49 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
50 48 49 sylib 
 |-  ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) -> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
51 9 47 50 mpjaodan 
 |-  ( ( F e. ( G GrpHom H ) /\ N e. ZZ /\ X e. B ) -> ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) )