Metamath Proof Explorer

Theorem mulgghm2

Description: The powers of a group element give a homomorphism from ZZ to a group. (Contributed by Mario Carneiro, 13-Jun-2015) (Revised by AV, 12-Jun-2019)

Ref Expression
Hypotheses mulgghm2.m 
|- .x. = ( .g ` R )
mulgghm2.f 
|- F = ( n e. ZZ |-> ( n .x. .1. ) )
mulgghm2.b 
|- B = ( Base ` R )
Assertion mulgghm2 
|- ( ( R e. Grp /\ .1. e. B ) -> F e. ( ZZring GrpHom R ) )

Proof

Step Hyp Ref Expression
1 mulgghm2.m 
 |-  .x. = ( .g ` R )
2 mulgghm2.f 
 |-  F = ( n e. ZZ |-> ( n .x. .1. ) )
3 mulgghm2.b 
 |-  B = ( Base ` R )
4 simpl 
 |-  ( ( R e. Grp /\ .1. e. B ) -> R e. Grp )
5 zringgrp 
 |-  ZZring e. Grp
6 4 5 jctil 
 |-  ( ( R e. Grp /\ .1. e. B ) -> ( ZZring e. Grp /\ R e. Grp ) )
7 3 1 mulgcl 
 |-  ( ( R e. Grp /\ n e. ZZ /\ .1. e. B ) -> ( n .x. .1. ) e. B )
8 7 3expa 
 |-  ( ( ( R e. Grp /\ n e. ZZ ) /\ .1. e. B ) -> ( n .x. .1. ) e. B )
9 8 an32s 
 |-  ( ( ( R e. Grp /\ .1. e. B ) /\ n e. ZZ ) -> ( n .x. .1. ) e. B )
10 9 2 fmptd 
 |-  ( ( R e. Grp /\ .1. e. B ) -> F : ZZ --> B )
11 eqid 
 |-  ( +g ` R ) = ( +g ` R )
12 3 1 11 mulgdir 
 |-  ( ( R e. Grp /\ ( x e. ZZ /\ y e. ZZ /\ .1. e. B ) ) -> ( ( x + y ) .x. .1. ) = ( ( x .x. .1. ) ( +g ` R ) ( y .x. .1. ) ) )
13 12 3exp2 
 |-  ( R e. Grp -> ( x e. ZZ -> ( y e. ZZ -> ( .1. e. B -> ( ( x + y ) .x. .1. ) = ( ( x .x. .1. ) ( +g ` R ) ( y .x. .1. ) ) ) ) ) )
14 13 imp42 
 |-  ( ( ( R e. Grp /\ ( x e. ZZ /\ y e. ZZ ) ) /\ .1. e. B ) -> ( ( x + y ) .x. .1. ) = ( ( x .x. .1. ) ( +g ` R ) ( y .x. .1. ) ) )
15 14 an32s 
 |-  ( ( ( R e. Grp /\ .1. e. B ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x + y ) .x. .1. ) = ( ( x .x. .1. ) ( +g ` R ) ( y .x. .1. ) ) )
16 zaddcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) e. ZZ )
17 16 adantl 
 |-  ( ( ( R e. Grp /\ .1. e. B ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x + y ) e. ZZ )
18 oveq1 
 |-  ( n = ( x + y ) -> ( n .x. .1. ) = ( ( x + y ) .x. .1. ) )
19 ovex 
 |-  ( ( x + y ) .x. .1. ) e. _V
20 18 2 19 fvmpt 
 |-  ( ( x + y ) e. ZZ -> ( F ` ( x + y ) ) = ( ( x + y ) .x. .1. ) )
21 17 20 syl 
 |-  ( ( ( R e. Grp /\ .1. e. B ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( F ` ( x + y ) ) = ( ( x + y ) .x. .1. ) )
22 oveq1 
 |-  ( n = x -> ( n .x. .1. ) = ( x .x. .1. ) )
23 ovex 
 |-  ( x .x. .1. ) e. _V
24 22 2 23 fvmpt 
 |-  ( x e. ZZ -> ( F ` x ) = ( x .x. .1. ) )
25 oveq1 
 |-  ( n = y -> ( n .x. .1. ) = ( y .x. .1. ) )
26 ovex 
 |-  ( y .x. .1. ) e. _V
27 25 2 26 fvmpt 
 |-  ( y e. ZZ -> ( F ` y ) = ( y .x. .1. ) )
28 24 27 oveqan12d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( F ` x ) ( +g ` R ) ( F ` y ) ) = ( ( x .x. .1. ) ( +g ` R ) ( y .x. .1. ) ) )
29 28 adantl 
 |-  ( ( ( R e. Grp /\ .1. e. B ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( F ` x ) ( +g ` R ) ( F ` y ) ) = ( ( x .x. .1. ) ( +g ` R ) ( y .x. .1. ) ) )
30 15 21 29 3eqtr4d 
 |-  ( ( ( R e. Grp /\ .1. e. B ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( F ` ( x + y ) ) = ( ( F ` x ) ( +g ` R ) ( F ` y ) ) )
31 30 ralrimivva 
 |-  ( ( R e. Grp /\ .1. e. B ) -> A. x e. ZZ A. y e. ZZ ( F ` ( x + y ) ) = ( ( F ` x ) ( +g ` R ) ( F ` y ) ) )
32 10 31 jca 
 |-  ( ( R e. Grp /\ .1. e. B ) -> ( F : ZZ --> B /\ A. x e. ZZ A. y e. ZZ ( F ` ( x + y ) ) = ( ( F ` x ) ( +g ` R ) ( F ` y ) ) ) )
33 zringbas 
 |-  ZZ = ( Base ` ZZring )
34 zringplusg 
 |-  + = ( +g ` ZZring )
35 33 3 34 11 isghm 
 |-  ( F e. ( ZZring GrpHom R ) <-> ( ( ZZring e. Grp /\ R e. Grp ) /\ ( F : ZZ --> B /\ A. x e. ZZ A. y e. ZZ ( F ` ( x + y ) ) = ( ( F ` x ) ( +g ` R ) ( F ` y ) ) ) ) )
36 6 32 35 sylanbrc 
 |-  ( ( R e. Grp /\ .1. e. B ) -> F e. ( ZZring GrpHom R ) )