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

Theorem rngrghm 17028
 Description: Right-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
rngrghm
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem rngrghm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rnglghm.b . 2
2 eqid 2460 . 2
3 rnggrp 16984 . . 3
5 rnglghm.t . . . . . 6
61, 5rngcl 16992 . . . . 5
763expa 1191 . . . 4
87an32s 802 . . 3
9 eqid 2460 . . 3
108, 9fmptd 6036 . 2
11 df-3an 970 . . . . 5
121, 2, 5rngdir 16998 . . . . 5
1311, 12sylan2br 476 . . . 4
1413anass1rs 805 . . 3
151, 2rngacl 17006 . . . . . 6
16153expb 1192 . . . . 5
1716adantlr 714 . . . 4
18 oveq1 6282 . . . . 5
19 ovex 6300 . . . . 5
2018, 9, 19fvmpt 5941 . . . 4
2117, 20syl 16 . . 3
22 oveq1 6282 . . . . . 6
23 ovex 6300 . . . . . 6
2422, 9, 23fvmpt 5941 . . . . 5
25 oveq1 6282 . . . . . 6
26 ovex 6300 . . . . . 6
2725, 9, 26fvmpt 5941 . . . . 5
2824, 27oveqan12d 6294 . . . 4