Metamath Proof Explorer

Theorem expghm

Description: Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses expghm.m 
|- M = ( mulGrp ` CCfld )
expghm.u 
|- U = ( M |`s ( CC \ { 0 } ) )
Assertion expghm 
|- ( ( A e. CC /\ A =/= 0 ) -> ( x e. ZZ |-> ( A ^ x ) ) e. ( ZZring GrpHom U ) )

Proof

Step Hyp Ref Expression
1 expghm.m 
 |-  M = ( mulGrp ` CCfld )
2 expghm.u 
 |-  U = ( M |`s ( CC \ { 0 } ) )
3 expclzlem 
 |-  ( ( A e. CC /\ A =/= 0 /\ x e. ZZ ) -> ( A ^ x ) e. ( CC \ { 0 } ) )
4 3 3expa 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ZZ ) -> ( A ^ x ) e. ( CC \ { 0 } ) )
5 4 fmpttd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. ZZ |-> ( A ^ x ) ) : ZZ --> ( CC \ { 0 } ) )
6 expaddz 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( A ^ ( y + z ) ) = ( ( A ^ y ) x. ( A ^ z ) ) )
7 zaddcl 
 |-  ( ( y e. ZZ /\ z e. ZZ ) -> ( y + z ) e. ZZ )
8 7 adantl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( y + z ) e. ZZ )
9 oveq2 
 |-  ( x = ( y + z ) -> ( A ^ x ) = ( A ^ ( y + z ) ) )
10 eqid 
 |-  ( x e. ZZ |-> ( A ^ x ) ) = ( x e. ZZ |-> ( A ^ x ) )
11 ovex 
 |-  ( A ^ ( y + z ) ) e. _V
12 9 10 11 fvmpt 
 |-  ( ( y + z ) e. ZZ -> ( ( x e. ZZ |-> ( A ^ x ) ) ` ( y + z ) ) = ( A ^ ( y + z ) ) )
13 8 12 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( x e. ZZ |-> ( A ^ x ) ) ` ( y + z ) ) = ( A ^ ( y + z ) ) )
14 oveq2 
 |-  ( x = y -> ( A ^ x ) = ( A ^ y ) )
15 ovex 
 |-  ( A ^ y ) e. _V
16 14 10 15 fvmpt 
 |-  ( y e. ZZ -> ( ( x e. ZZ |-> ( A ^ x ) ) ` y ) = ( A ^ y ) )
17 oveq2 
 |-  ( x = z -> ( A ^ x ) = ( A ^ z ) )
18 ovex 
 |-  ( A ^ z ) e. _V
19 17 10 18 fvmpt 
 |-  ( z e. ZZ -> ( ( x e. ZZ |-> ( A ^ x ) ) ` z ) = ( A ^ z ) )
20 16 19 oveqan12d 
 |-  ( ( y e. ZZ /\ z e. ZZ ) -> ( ( ( x e. ZZ |-> ( A ^ x ) ) ` y ) x. ( ( x e. ZZ |-> ( A ^ x ) ) ` z ) ) = ( ( A ^ y ) x. ( A ^ z ) ) )
21 20 adantl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( ( x e. ZZ |-> ( A ^ x ) ) ` y ) x. ( ( x e. ZZ |-> ( A ^ x ) ) ` z ) ) = ( ( A ^ y ) x. ( A ^ z ) ) )
22 6 13 21 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( x e. ZZ |-> ( A ^ x ) ) ` ( y + z ) ) = ( ( ( x e. ZZ |-> ( A ^ x ) ) ` y ) x. ( ( x e. ZZ |-> ( A ^ x ) ) ` z ) ) )
23 22 ralrimivva 
 |-  ( ( A e. CC /\ A =/= 0 ) -> A. y e. ZZ A. z e. ZZ ( ( x e. ZZ |-> ( A ^ x ) ) ` ( y + z ) ) = ( ( ( x e. ZZ |-> ( A ^ x ) ) ` y ) x. ( ( x e. ZZ |-> ( A ^ x ) ) ` z ) ) )
24 zringgrp 
 |-  ZZring e. Grp
25 cnring 
 |-  CCfld e. Ring
26 cnfldbas 
 |-  CC = ( Base ` CCfld )
27 cnfld0 
 |-  0 = ( 0g ` CCfld )
28 cndrng 
 |-  CCfld e. DivRing
29 26 27 28 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
30 1 oveq1i 
 |-  ( M |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
31 2 30 eqtri 
 |-  U = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
32 29 31 unitgrp 
 |-  ( CCfld e. Ring -> U e. Grp )
33 25 32 ax-mp 
 |-  U e. Grp
34 24 33 pm3.2i 
 |-  ( ZZring e. Grp /\ U e. Grp )
35 zringbas 
 |-  ZZ = ( Base ` ZZring )
36 difss 
 |-  ( CC \ { 0 } ) C_ CC
37 1 26 mgpbas 
 |-  CC = ( Base ` M )
38 2 37 ressbas2 
 |-  ( ( CC \ { 0 } ) C_ CC -> ( CC \ { 0 } ) = ( Base ` U ) )
39 36 38 ax-mp 
 |-  ( CC \ { 0 } ) = ( Base ` U )
40 zringplusg 
 |-  + = ( +g ` ZZring )
41 29 fvexi 
 |-  ( CC \ { 0 } ) e. _V
42 cnfldmul 
 |-  x. = ( .r ` CCfld )
43 1 42 mgpplusg 
 |-  x. = ( +g ` M )
44 2 43 ressplusg 
 |-  ( ( CC \ { 0 } ) e. _V -> x. = ( +g ` U ) )
45 41 44 ax-mp 
 |-  x. = ( +g ` U )
46 35 39 40 45 isghm 
 |-  ( ( x e. ZZ |-> ( A ^ x ) ) e. ( ZZring GrpHom U ) <-> ( ( ZZring e. Grp /\ U e. Grp ) /\ ( ( x e. ZZ |-> ( A ^ x ) ) : ZZ --> ( CC \ { 0 } ) /\ A. y e. ZZ A. z e. ZZ ( ( x e. ZZ |-> ( A ^ x ) ) ` ( y + z ) ) = ( ( ( x e. ZZ |-> ( A ^ x ) ) ` y ) x. ( ( x e. ZZ |-> ( A ^ x ) ) ` z ) ) ) ) )
47 34 46 mpbiran 
 |-  ( ( x e. ZZ |-> ( A ^ x ) ) e. ( ZZring GrpHom U ) <-> ( ( x e. ZZ |-> ( A ^ x ) ) : ZZ --> ( CC \ { 0 } ) /\ A. y e. ZZ A. z e. ZZ ( ( x e. ZZ |-> ( A ^ x ) ) ` ( y + z ) ) = ( ( ( x e. ZZ |-> ( A ^ x ) ) ` y ) x. ( ( x e. ZZ |-> ( A ^ x ) ) ` z ) ) ) )
48 5 23 47 sylanbrc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. ZZ |-> ( A ^ x ) ) e. ( ZZring GrpHom U ) )