# Metamath Proof Explorer

## Theorem assamulgscm

Description: Exponentiation of a scalar multiplication in an associative algebra: ( a .x. X ) ^ N = ( a ^ N ) .X. ( X ^ N ) . (Contributed by AV, 26-Aug-2019)

Ref Expression
Hypotheses assamulgscm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
assamulgscm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
assamulgscm.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
assamulgscm.s
assamulgscm.g ${⊢}{G}={\mathrm{mulGrp}}_{{F}}$
assamulgscm.p
assamulgscm.h ${⊢}{H}={\mathrm{mulGrp}}_{{W}}$
assamulgscm.e ${⊢}{E}={\cdot }_{{H}}$
Assertion assamulgscm

### Proof

Step Hyp Ref Expression
1 assamulgscm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 assamulgscm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 assamulgscm.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
4 assamulgscm.s
5 assamulgscm.g ${⊢}{G}={\mathrm{mulGrp}}_{{F}}$
6 assamulgscm.p
7 assamulgscm.h ${⊢}{H}={\mathrm{mulGrp}}_{{W}}$
8 assamulgscm.e ${⊢}{E}={\cdot }_{{H}}$
9 oveq1
10 oveq1
11 oveq1 ${⊢}{x}=0\to {x}{E}{X}=0{E}{X}$
12 10 11 oveq12d
13 9 12 eqeq12d
14 13 imbi2d
15 oveq1
16 oveq1
17 oveq1 ${⊢}{x}={y}\to {x}{E}{X}={y}{E}{X}$
18 16 17 oveq12d
19 15 18 eqeq12d
20 19 imbi2d
21 oveq1
22 oveq1
23 oveq1 ${⊢}{x}={y}+1\to {x}{E}{X}=\left({y}+1\right){E}{X}$
24 22 23 oveq12d
25 21 24 eqeq12d
26 25 imbi2d
27 oveq1
28 oveq1
29 oveq1 ${⊢}{x}={N}\to {x}{E}{X}={N}{E}{X}$
30 28 29 oveq12d
31 27 30 eqeq12d
32 31 imbi2d
33 1 2 3 4 5 6 7 8 assamulgscmlem1
34 1 2 3 4 5 6 7 8 assamulgscmlem2
35 34 a2d
36 14 20 26 32 33 35 nn0ind
37 36 exp4c
38 37 3imp
39 38 impcom