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

Metamath Proof Explorer

Theorem mulgrhm

Description: The powers of the element 1 give a ring homomorphism from ZZ to a ring. (Contributed by Mario Carneiro, 14-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. ) )
mulgrhm.1 
|- .1. = ( 1r ` R )
Assertion mulgrhm 
|- ( R e. Ring -> F e. ( ZZring RingHom R ) )

Proof

Step Hyp Ref Expression
1 mulgghm2.m 
 |-  .x. = ( .g ` R )
2 mulgghm2.f 
 |-  F = ( n e. ZZ |-> ( n .x. .1. ) )
3 mulgrhm.1 
 |-  .1. = ( 1r ` R )
4 zringbas 
 |-  ZZ = ( Base ` ZZring )
5 zring1 
 |-  1 = ( 1r ` ZZring )
6 zringmulr 
 |-  x. = ( .r ` ZZring )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 zringring 
 |-  ZZring e. Ring
9 8 a1i 
 |-  ( R e. Ring -> ZZring e. Ring )
10 id 
 |-  ( R e. Ring -> R e. Ring )
11 1z 
 |-  1 e. ZZ
12 oveq1 
 |-  ( n = 1 -> ( n .x. .1. ) = ( 1 .x. .1. ) )
13 ovex 
 |-  ( 1 .x. .1. ) e. _V
14 12 2 13 fvmpt 
 |-  ( 1 e. ZZ -> ( F ` 1 ) = ( 1 .x. .1. ) )
15 11 14 ax-mp 
 |-  ( F ` 1 ) = ( 1 .x. .1. )
16 eqid 
 |-  ( Base ` R ) = ( Base ` R )
17 16 3 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
18 16 1 mulg1 
 |-  ( .1. e. ( Base ` R ) -> ( 1 .x. .1. ) = .1. )
19 17 18 syl 
 |-  ( R e. Ring -> ( 1 .x. .1. ) = .1. )
20 15 19 eqtrid 
 |-  ( R e. Ring -> ( F ` 1 ) = .1. )
21 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
22 21 adantr 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> R e. Grp )
23 simprr 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. ZZ )
24 17 adantr 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> .1. e. ( Base ` R ) )
25 16 1 mulgcl 
 |-  ( ( R e. Grp /\ y e. ZZ /\ .1. e. ( Base ` R ) ) -> ( y .x. .1. ) e. ( Base ` R ) )
26 22 23 24 25 syl3anc 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( y .x. .1. ) e. ( Base ` R ) )
27 16 7 3 ringlidm 
 |-  ( ( R e. Ring /\ ( y .x. .1. ) e. ( Base ` R ) ) -> ( .1. ( .r ` R ) ( y .x. .1. ) ) = ( y .x. .1. ) )
28 26 27 syldan 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( .1. ( .r ` R ) ( y .x. .1. ) ) = ( y .x. .1. ) )
29 28 oveq2d 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x .x. ( .1. ( .r ` R ) ( y .x. .1. ) ) ) = ( x .x. ( y .x. .1. ) ) )
30 simpl 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> R e. Ring )
31 simprl 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. ZZ )
32 16 1 7 mulgass2 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ .1. e. ( Base ` R ) /\ ( y .x. .1. ) e. ( Base ` R ) ) ) -> ( ( x .x. .1. ) ( .r ` R ) ( y .x. .1. ) ) = ( x .x. ( .1. ( .r ` R ) ( y .x. .1. ) ) ) )
33 30 31 24 26 32 syl13anc 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x .x. .1. ) ( .r ` R ) ( y .x. .1. ) ) = ( x .x. ( .1. ( .r ` R ) ( y .x. .1. ) ) ) )
34 16 1 mulgass 
 |-  ( ( R e. Grp /\ ( x e. ZZ /\ y e. ZZ /\ .1. e. ( Base ` R ) ) ) -> ( ( x x. y ) .x. .1. ) = ( x .x. ( y .x. .1. ) ) )
35 22 31 23 24 34 syl13anc 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x x. y ) .x. .1. ) = ( x .x. ( y .x. .1. ) ) )
36 29 33 35 3eqtr4rd 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x x. y ) .x. .1. ) = ( ( x .x. .1. ) ( .r ` R ) ( y .x. .1. ) ) )
37 zmulcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ )
38 37 adantl 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x x. y ) e. ZZ )
39 oveq1 
 |-  ( n = ( x x. y ) -> ( n .x. .1. ) = ( ( x x. y ) .x. .1. ) )
40 ovex 
 |-  ( ( x x. y ) .x. .1. ) e. _V
41 39 2 40 fvmpt 
 |-  ( ( x x. y ) e. ZZ -> ( F ` ( x x. y ) ) = ( ( x x. y ) .x. .1. ) )
42 38 41 syl 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( F ` ( x x. y ) ) = ( ( x x. y ) .x. .1. ) )
43 oveq1 
 |-  ( n = x -> ( n .x. .1. ) = ( x .x. .1. ) )
44 ovex 
 |-  ( x .x. .1. ) e. _V
45 43 2 44 fvmpt 
 |-  ( x e. ZZ -> ( F ` x ) = ( x .x. .1. ) )
46 oveq1 
 |-  ( n = y -> ( n .x. .1. ) = ( y .x. .1. ) )
47 ovex 
 |-  ( y .x. .1. ) e. _V
48 46 2 47 fvmpt 
 |-  ( y e. ZZ -> ( F ` y ) = ( y .x. .1. ) )
49 45 48 oveqan12d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( F ` x ) ( .r ` R ) ( F ` y ) ) = ( ( x .x. .1. ) ( .r ` R ) ( y .x. .1. ) ) )
50 49 adantl 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( F ` x ) ( .r ` R ) ( F ` y ) ) = ( ( x .x. .1. ) ( .r ` R ) ( y .x. .1. ) ) )
51 36 42 50 3eqtr4d 
 |-  ( ( R e. Ring /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( F ` ( x x. y ) ) = ( ( F ` x ) ( .r ` R ) ( F ` y ) ) )
52 1 2 16 mulgghm2 
 |-  ( ( R e. Grp /\ .1. e. ( Base ` R ) ) -> F e. ( ZZring GrpHom R ) )
53 21 17 52 syl2anc 
 |-  ( R e. Ring -> F e. ( ZZring GrpHom R ) )
54 4 5 3 6 7 9 10 20 51 53 isrhm2d 
 |-  ( R e. Ring -> F e. ( ZZring RingHom R ) )