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

Theorem lmodvsghm 15997
 Description: Scalar multiplication of the vector space by a fixed scalar is an automorphism of the addiive group of vectors. (Contributed by Mario Carneiro, 5-May-2015.)
Hypotheses
Ref Expression
lmodvsghm.v
lmodvsghm.f Scalar
lmodvsghm.s
lmodvsghm.k
Assertion
Ref Expression
lmodvsghm
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem lmodvsghm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmodvsghm.v . 2
2 eqid 2435 . 2
3 lmodgrp 15949 . . 3
5 lmodvsghm.f . . . . 5 Scalar
6 lmodvsghm.s . . . . 5
7 lmodvsghm.k . . . . 5
81, 5, 6, 7lmodvscl 15959 . . . 4
983expa 1153 . . 3
10 eqid 2435 . . 3
119, 10fmptd 5885 . 2
121, 2, 5, 6, 7lmodvsdi 15965 . . . . 5
13123exp2 1171 . . . 4
1413imp43 579 . . 3
151, 2lmodvacl 15956 . . . . . 6
16153expb 1154 . . . . 5
1716adantlr 696 . . . 4
18 oveq2 6081 . . . . 5
19 ovex 6098 . . . . 5
2018, 10, 19fvmpt 5798 . . . 4
2117, 20syl 16 . . 3
22 oveq2 6081 . . . . . 6
23 ovex 6098 . . . . . 6
2422, 10, 23fvmpt 5798 . . . . 5
25 oveq2 6081 . . . . . 6
26 ovex 6098 . . . . . 6
2725, 10, 26fvmpt 5798 . . . . 5
2824, 27oveqan12d 6092 . . . 4