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

Theorem mulgrhmOLD 18049
 Description: The powers of the element give a ring homomorphism from to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) Obsolete version of mulgrhm 18046 as of 12-Jun-2019. (New usage is discouraged.)
Hypotheses
Ref Expression
mulgghm2OLD.1 flds
mulgghm2OLD.2 .g
mulgghm2OLD.3
mulgrhmOLD.4
Assertion
Ref Expression
mulgrhmOLD RingHom
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem mulgrhmOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zsubrg 17986 . . 3 SubRingfld
2 mulgghm2OLD.1 . . . 4 flds
32subrgbas 16992 . . 3 SubRingfld
41, 3ax-mp 5 . 2
5 cnfld1 17961 . . . 4 fld
62, 5subrg1 16993 . . 3 SubRingfld
71, 6ax-mp 5 . 2
8 mulgrhmOLD.4 . 2
9 cnfldmul 17944 . . . 4 fld
102, 9ressmulr 14405 . . 3 SubRingfld
111, 10ax-mp 5 . 2
12 eqid 2452 . 2
132subrgrng 16986 . . 3 SubRingfld
141, 13mp1i 12 . 2
15 id 22 . 2
16 1z 10782 . . . 4
17 oveq1 6202 . . . . 5
18 mulgghm2OLD.3 . . . . 5
19 ovex 6220 . . . . 5
2017, 18, 19fvmpt 5878 . . . 4
2116, 20ax-mp 5 . . 3
22 eqid 2452 . . . . 5
2322, 8rngidcl 16783 . . . 4
24 mulgghm2OLD.2 . . . . 5 .g
2522, 24mulg1 15748 . . . 4
2623, 25syl 16 . . 3
2721, 26syl5eq 2505 . 2
28 rnggrp 16768 . . . . . . . 8
2928adantr 465 . . . . . . 7
30 simprr 756 . . . . . . 7
3123adantr 465 . . . . . . 7
3222, 24mulgcl 15758 . . . . . . 7
3329, 30, 31, 32syl3anc 1219 . . . . . 6
3422, 12, 8rnglidm 16786 . . . . . 6
3533, 34syldan 470 . . . . 5
3635oveq2d 6211 . . . 4
37 simpl 457 . . . . 5
38 simprl 755 . . . . 5
3922, 24, 12mulgass2 16810 . . . . 5
4037, 38, 31, 33, 39syl13anc 1221 . . . 4
4122, 24mulgass 15771 . . . . 5
4229, 38, 30, 31, 41syl13anc 1221 . . . 4
4336, 40, 423eqtr4rd 2504 . . 3
44 zmulcl 10799 . . . . 5
4544adantl 466 . . . 4
46 oveq1 6202 . . . . 5
47 ovex 6220 . . . . 5
4846, 18, 47fvmpt 5878 . . . 4
4945, 48syl 16 . . 3
50 oveq1 6202 . . . . . 6
51 ovex 6220 . . . . . 6
5250, 18, 51fvmpt 5878 . . . . 5
53 oveq1 6202 . . . . . 6
54 ovex 6220 . . . . . 6
5553, 18, 54fvmpt 5878 . . . . 5
5652, 55oveqan12d 6214 . . . 4