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

Theorem mulgrhm 16788
 Description: The powers of the element give a ring homomorphism from to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
Hypotheses
Ref Expression
mulgghm2.1 flds
mulgghm2.2 .g
mulgghm2.3
mulgrhm.4
Assertion
Ref Expression
mulgrhm 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 zsubrg 16753 . . 3 SubRingfld
2 mulgghm2.1 . . . 4 flds
32subrgbas 15878 . . 3 SubRingfld
41, 3ax-mp 8 . 2
5 cnfld1 16727 . . . 4 fld
62, 5subrg1 15879 . . 3 SubRingfld
71, 6ax-mp 8 . 2
8 mulgrhm.4 . 2
9 cnfldmul 16710 . . . 4 fld
102, 9ressmulr 13583 . . 3 SubRingfld
111, 10ax-mp 8 . 2
12 eqid 2437 . 2
132subrgrng 15872 . . 3 SubRingfld
141, 13mp1i 12 . 2
15 id 21 . 2
16 1z 10312 . . . 4
17 oveq1 6089 . . . . 5
18 mulgghm2.3 . . . . 5
19 ovex 6107 . . . . 5
2017, 18, 19fvmpt 5807 . . . 4
2116, 20ax-mp 8 . . 3
22 eqid 2437 . . . . 5
2322, 8rngidcl 15685 . . . 4
24 mulgghm2.2 . . . . 5 .g
2522, 24mulg1 14898 . . . 4
2623, 25syl 16 . . 3
2721, 26syl5eq 2481 . 2
28 rnggrp 15670 . . . . . . . 8
2928adantr 453 . . . . . . 7
30 simprr 735 . . . . . . 7
3123adantr 453 . . . . . . 7
3222, 24mulgcl 14908 . . . . . . 7
3329, 30, 31, 32syl3anc 1185 . . . . . 6
3422, 12, 8rnglidm 15688 . . . . . 6
3533, 34syldan 458 . . . . 5
3635oveq2d 6098 . . . 4
37 simpl 445 . . . . 5
38 simprl 734 . . . . 5
3922, 24, 12mulgass2 15711 . . . . 5
4037, 38, 31, 33, 39syl13anc 1187 . . . 4
4122, 24mulgass 14921 . . . . 5
4229, 38, 30, 31, 41syl13anc 1187 . . . 4
4336, 40, 423eqtr4rd 2480 . . 3
44 zmulcl 10325 . . . . 5
4544adantl 454 . . . 4
46 oveq1 6089 . . . . 5
47 ovex 6107 . . . . 5
4846, 18, 47fvmpt 5807 . . . 4
4945, 48syl 16 . . 3
50 oveq1 6089 . . . . . 6
51 ovex 6107 . . . . . 6
5250, 18, 51fvmpt 5807 . . . . 5
53 oveq1 6089 . . . . . 6
54 ovex 6107 . . . . . 6
5553, 18, 54fvmpt 5807 . . . . 5
5652, 55oveqan12d 6101 . . . 4