Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulgrhm Structured version   Unicode version

Theorem mulgrhm 18399
 Description: The powers of the element give a ring homomorphism from to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.)
Hypotheses
Ref Expression
mulgghm2.m .g
mulgghm2.f
mulgrhm.1
Assertion
Ref Expression
mulgrhm ring RingHom
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem mulgrhm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zringbas 18362 . 2 ring
2 zring1 18367 . 2 ring
3 mulgrhm.1 . 2
4 zringmulr 18365 . 2 ring
5 eqid 2441 . 2
6 zringring 18359 . . 3 ring
76a1i 11 . 2 ring
8 id 22 . 2
9 1z 10895 . . . 4
10 oveq1 6284 . . . . 5
11 mulgghm2.f . . . . 5
12 ovex 6305 . . . . 5
1310, 11, 12fvmpt 5937 . . . 4
149, 13ax-mp 5 . . 3
15 eqid 2441 . . . . 5
1615, 3ringidcl 17087 . . . 4
17 mulgghm2.m . . . . 5 .g
1815, 17mulg1 16018 . . . 4
1916, 18syl 16 . . 3
2014, 19syl5eq 2494 . 2
21 ringgrp 17071 . . . . . . . 8
2221adantr 465 . . . . . . 7
23 simprr 756 . . . . . . 7
2416adantr 465 . . . . . . 7
2515, 17mulgcl 16028 . . . . . . 7
2622, 23, 24, 25syl3anc 1227 . . . . . 6
2715, 5, 3ringlidm 17090 . . . . . 6
2826, 27syldan 470 . . . . 5
2928oveq2d 6293 . . . 4
30 simpl 457 . . . . 5
31 simprl 755 . . . . 5
3215, 17, 5mulgass2 17115 . . . . 5
3330, 31, 24, 26, 32syl13anc 1229 . . . 4
3415, 17mulgass 16041 . . . . 5
3522, 31, 23, 24, 34syl13anc 1229 . . . 4
3629, 33, 353eqtr4rd 2493 . . 3
37 zmulcl 10913 . . . . 5
3837adantl 466 . . . 4
39 oveq1 6284 . . . . 5
40 ovex 6305 . . . . 5
4139, 11, 40fvmpt 5937 . . . 4
4238, 41syl 16 . . 3
43 oveq1 6284 . . . . . 6
44 ovex 6305 . . . . . 6
4543, 11, 44fvmpt 5937 . . . . 5
46 oveq1 6284 . . . . . 6
47 ovex 6305 . . . . . 6
4846, 11, 47fvmpt 5937 . . . . 5
4945, 48oveqan12d 6296 . . . 4