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

Metamath Proof Explorer

Theorem mulgrhm2

Description: The powers of the element 1 give the unique 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 mulgrhm2 
|- ( R e. Ring -> ( ZZring RingHom R ) = { F } )

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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 4 5 rhmf 
 |-  ( f e. ( ZZring RingHom R ) -> f : ZZ --> ( Base ` R ) )
7 6 adantl 
 |-  ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) -> f : ZZ --> ( Base ` R ) )
8 7 feqmptd 
 |-  ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) -> f = ( n e. ZZ |-> ( f ` n ) ) )
9 rhmghm 
 |-  ( f e. ( ZZring RingHom R ) -> f e. ( ZZring GrpHom R ) )
10 9 ad2antlr 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> f e. ( ZZring GrpHom R ) )
11 simpr 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> n e. ZZ )
12 1zzd 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> 1 e. ZZ )
13 eqid 
 |-  ( .g ` ZZring ) = ( .g ` ZZring )
14 4 13 1 ghmmulg 
 |-  ( ( f e. ( ZZring GrpHom R ) /\ n e. ZZ /\ 1 e. ZZ ) -> ( f ` ( n ( .g ` ZZring ) 1 ) ) = ( n .x. ( f ` 1 ) ) )
15 10 11 12 14 syl3anc 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> ( f ` ( n ( .g ` ZZring ) 1 ) ) = ( n .x. ( f ` 1 ) ) )
16 ax-1cn 
 |-  1 e. CC
17 cnfldmulg 
 |-  ( ( n e. ZZ /\ 1 e. CC ) -> ( n ( .g ` CCfld ) 1 ) = ( n x. 1 ) )
18 16 17 mpan2 
 |-  ( n e. ZZ -> ( n ( .g ` CCfld ) 1 ) = ( n x. 1 ) )
19 1z 
 |-  1 e. ZZ
20 18 adantr 
 |-  ( ( n e. ZZ /\ 1 e. ZZ ) -> ( n ( .g ` CCfld ) 1 ) = ( n x. 1 ) )
21 zringmulg 
 |-  ( ( n e. ZZ /\ 1 e. ZZ ) -> ( n ( .g ` ZZring ) 1 ) = ( n x. 1 ) )
22 20 21 eqtr4d 
 |-  ( ( n e. ZZ /\ 1 e. ZZ ) -> ( n ( .g ` CCfld ) 1 ) = ( n ( .g ` ZZring ) 1 ) )
23 19 22 mpan2 
 |-  ( n e. ZZ -> ( n ( .g ` CCfld ) 1 ) = ( n ( .g ` ZZring ) 1 ) )
24 zcn 
 |-  ( n e. ZZ -> n e. CC )
25 24 mulridd 
 |-  ( n e. ZZ -> ( n x. 1 ) = n )
26 18 23 25 3eqtr3d 
 |-  ( n e. ZZ -> ( n ( .g ` ZZring ) 1 ) = n )
27 26 adantl 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> ( n ( .g ` ZZring ) 1 ) = n )
28 27 fveq2d 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> ( f ` ( n ( .g ` ZZring ) 1 ) ) = ( f ` n ) )
29 zring1 
 |-  1 = ( 1r ` ZZring )
30 29 3 rhm1 
 |-  ( f e. ( ZZring RingHom R ) -> ( f ` 1 ) = .1. )
31 30 ad2antlr 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> ( f ` 1 ) = .1. )
32 31 oveq2d 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> ( n .x. ( f ` 1 ) ) = ( n .x. .1. ) )
33 15 28 32 3eqtr3d 
 |-  ( ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) /\ n e. ZZ ) -> ( f ` n ) = ( n .x. .1. ) )
34 33 mpteq2dva 
 |-  ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) -> ( n e. ZZ |-> ( f ` n ) ) = ( n e. ZZ |-> ( n .x. .1. ) ) )
35 8 34 eqtrd 
 |-  ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) -> f = ( n e. ZZ |-> ( n .x. .1. ) ) )
36 35 2 eqtr4di 
 |-  ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) -> f = F )
37 velsn 
 |-  ( f e. { F } <-> f = F )
38 36 37 sylibr 
 |-  ( ( R e. Ring /\ f e. ( ZZring RingHom R ) ) -> f e. { F } )
39 38 ex 
 |-  ( R e. Ring -> ( f e. ( ZZring RingHom R ) -> f e. { F } ) )
40 39 ssrdv 
 |-  ( R e. Ring -> ( ZZring RingHom R ) C_ { F } )
41 1 2 3 mulgrhm 
 |-  ( R e. Ring -> F e. ( ZZring RingHom R ) )
42 41 snssd 
 |-  ( R e. Ring -> { F } C_ ( ZZring RingHom R ) )
43 40 42 eqssd 
 |-  ( R e. Ring -> ( ZZring RingHom R ) = { F } )