Metamath Proof Explorer

Theorem expmhm

Description: Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses expmhm.1 
|- N = ( CCfld |`s NN0 )
expmhm.2 
|- M = ( mulGrp ` CCfld )
Assertion expmhm 
|- ( A e. CC -> ( x e. NN0 |-> ( A ^ x ) ) e. ( N MndHom M ) )

Proof

Step Hyp Ref Expression
1 expmhm.1 
 |-  N = ( CCfld |`s NN0 )
2 expmhm.2 
 |-  M = ( mulGrp ` CCfld )
3 expcl 
 |-  ( ( A e. CC /\ x e. NN0 ) -> ( A ^ x ) e. CC )
4 3 fmpttd 
 |-  ( A e. CC -> ( x e. NN0 |-> ( A ^ x ) ) : NN0 --> CC )
5 expadd 
 |-  ( ( A e. CC /\ y e. NN0 /\ z e. NN0 ) -> ( A ^ ( y + z ) ) = ( ( A ^ y ) x. ( A ^ z ) ) )
6 5 3expb 
 |-  ( ( A e. CC /\ ( y e. NN0 /\ z e. NN0 ) ) -> ( A ^ ( y + z ) ) = ( ( A ^ y ) x. ( A ^ z ) ) )
7 nn0addcl 
 |-  ( ( y e. NN0 /\ z e. NN0 ) -> ( y + z ) e. NN0 )
8 7 adantl 
 |-  ( ( A e. CC /\ ( y e. NN0 /\ z e. NN0 ) ) -> ( y + z ) e. NN0 )
9 oveq2 
 |-  ( x = ( y + z ) -> ( A ^ x ) = ( A ^ ( y + z ) ) )
10 eqid 
 |-  ( x e. NN0 |-> ( A ^ x ) ) = ( x e. NN0 |-> ( A ^ x ) )
11 ovex 
 |-  ( A ^ ( y + z ) ) e. _V
12 9 10 11 fvmpt 
 |-  ( ( y + z ) e. NN0 -> ( ( x e. NN0 |-> ( A ^ x ) ) ` ( y + z ) ) = ( A ^ ( y + z ) ) )
13 8 12 syl 
 |-  ( ( A e. CC /\ ( y e. NN0 /\ z e. NN0 ) ) -> ( ( x e. NN0 |-> ( 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. NN0 -> ( ( x e. NN0 |-> ( 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. NN0 -> ( ( x e. NN0 |-> ( A ^ x ) ) ` z ) = ( A ^ z ) )
20 16 19 oveqan12d 
 |-  ( ( y e. NN0 /\ z e. NN0 ) -> ( ( ( x e. NN0 |-> ( A ^ x ) ) ` y ) x. ( ( x e. NN0 |-> ( A ^ x ) ) ` z ) ) = ( ( A ^ y ) x. ( A ^ z ) ) )
21 20 adantl 
 |-  ( ( A e. CC /\ ( y e. NN0 /\ z e. NN0 ) ) -> ( ( ( x e. NN0 |-> ( A ^ x ) ) ` y ) x. ( ( x e. NN0 |-> ( A ^ x ) ) ` z ) ) = ( ( A ^ y ) x. ( A ^ z ) ) )
22 6 13 21 3eqtr4d 
 |-  ( ( A e. CC /\ ( y e. NN0 /\ z e. NN0 ) ) -> ( ( x e. NN0 |-> ( A ^ x ) ) ` ( y + z ) ) = ( ( ( x e. NN0 |-> ( A ^ x ) ) ` y ) x. ( ( x e. NN0 |-> ( A ^ x ) ) ` z ) ) )
23 22 ralrimivva 
 |-  ( A e. CC -> A. y e. NN0 A. z e. NN0 ( ( x e. NN0 |-> ( A ^ x ) ) ` ( y + z ) ) = ( ( ( x e. NN0 |-> ( A ^ x ) ) ` y ) x. ( ( x e. NN0 |-> ( A ^ x ) ) ` z ) ) )
24 0nn0 
 |-  0 e. NN0
25 oveq2 
 |-  ( x = 0 -> ( A ^ x ) = ( A ^ 0 ) )
26 ovex 
 |-  ( A ^ 0 ) e. _V
27 25 10 26 fvmpt 
 |-  ( 0 e. NN0 -> ( ( x e. NN0 |-> ( A ^ x ) ) ` 0 ) = ( A ^ 0 ) )
28 24 27 ax-mp 
 |-  ( ( x e. NN0 |-> ( A ^ x ) ) ` 0 ) = ( A ^ 0 )
29 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
30 28 29 syl5eq 
 |-  ( A e. CC -> ( ( x e. NN0 |-> ( A ^ x ) ) ` 0 ) = 1 )
31 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
32 1 submmnd 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> N e. Mnd )
33 31 32 ax-mp 
 |-  N e. Mnd
34 cnring 
 |-  CCfld e. Ring
35 2 ringmgp 
 |-  ( CCfld e. Ring -> M e. Mnd )
36 34 35 ax-mp 
 |-  M e. Mnd
37 33 36 pm3.2i 
 |-  ( N e. Mnd /\ M e. Mnd )
38 1 submbas 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> NN0 = ( Base ` N ) )
39 31 38 ax-mp 
 |-  NN0 = ( Base ` N )
40 cnfldbas 
 |-  CC = ( Base ` CCfld )
41 2 40 mgpbas 
 |-  CC = ( Base ` M )
42 cnfldadd 
 |-  + = ( +g ` CCfld )
43 1 42 ressplusg 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> + = ( +g ` N ) )
44 31 43 ax-mp 
 |-  + = ( +g ` N )
45 cnfldmul 
 |-  x. = ( .r ` CCfld )
46 2 45 mgpplusg 
 |-  x. = ( +g ` M )
47 cnfld0 
 |-  0 = ( 0g ` CCfld )
48 1 47 subm0 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> 0 = ( 0g ` N ) )
49 31 48 ax-mp 
 |-  0 = ( 0g ` N )
50 cnfld1 
 |-  1 = ( 1r ` CCfld )
51 2 50 ringidval 
 |-  1 = ( 0g ` M )
52 39 41 44 46 49 51 ismhm 
 |-  ( ( x e. NN0 |-> ( A ^ x ) ) e. ( N MndHom M ) <-> ( ( N e. Mnd /\ M e. Mnd ) /\ ( ( x e. NN0 |-> ( A ^ x ) ) : NN0 --> CC /\ A. y e. NN0 A. z e. NN0 ( ( x e. NN0 |-> ( A ^ x ) ) ` ( y + z ) ) = ( ( ( x e. NN0 |-> ( A ^ x ) ) ` y ) x. ( ( x e. NN0 |-> ( A ^ x ) ) ` z ) ) /\ ( ( x e. NN0 |-> ( A ^ x ) ) ` 0 ) = 1 ) ) )
53 37 52 mpbiran 
 |-  ( ( x e. NN0 |-> ( A ^ x ) ) e. ( N MndHom M ) <-> ( ( x e. NN0 |-> ( A ^ x ) ) : NN0 --> CC /\ A. y e. NN0 A. z e. NN0 ( ( x e. NN0 |-> ( A ^ x ) ) ` ( y + z ) ) = ( ( ( x e. NN0 |-> ( A ^ x ) ) ` y ) x. ( ( x e. NN0 |-> ( A ^ x ) ) ` z ) ) /\ ( ( x e. NN0 |-> ( A ^ x ) ) ` 0 ) = 1 ) )
54 4 23 30 53 syl3anbrc 
 |-  ( A e. CC -> ( x e. NN0 |-> ( A ^ x ) ) e. ( N MndHom M ) )