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

Theorem rnglghm 15713
 Description: Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
Hypotheses
Ref Expression
rnglghm.b
rnglghm.t
Assertion
Ref Expression
rnglghm
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem rnglghm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rnglghm.b . 2
2 eqid 2438 . 2
3 rnggrp 15671 . . 3
5 rnglghm.t . . . . 5
61, 5rngcl 15679 . . . 4
763expa 1154 . . 3
8 eqid 2438 . . 3
97, 8fmptd 5895 . 2
10 3anass 941 . . . . 5
111, 2, 5rngdi 15684 . . . . 5
1210, 11sylan2br 464 . . . 4
1312anassrs 631 . . 3
141, 2rngacl 15693 . . . . . 6
15143expb 1155 . . . . 5
1615adantlr 697 . . . 4
17 oveq2 6091 . . . . 5
18 ovex 6108 . . . . 5
1917, 8, 18fvmpt 5808 . . . 4
2016, 19syl 16 . . 3
21 oveq2 6091 . . . . . 6
22 ovex 6108 . . . . . 6
2321, 8, 22fvmpt 5808 . . . . 5
24 oveq2 6091 . . . . . 6
25 ovex 6108 . . . . . 6
2624, 8, 25fvmpt 5808 . . . . 5
2723, 26oveqan12d 6102 . . . 4