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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
assamulgscm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
assamulgscm.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
assamulgscm.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
assamulgscm.g ⊢ 𝐺 = ( mulGrp ‘ 𝐹 )
assamulgscm.p ⊢ ↑ = ( .g ‘ 𝐺 )
assamulgscm.h ⊢ 𝐻 = ( mulGrp ‘ 𝑊 )
assamulgscm.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
Assertion assamulgscm ( ( 𝑊 ∈ AssAlg ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 assamulgscm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 assamulgscm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 assamulgscm.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 assamulgscm.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 assamulgscm.g ⊢ 𝐺 = ( mulGrp ‘ 𝐹 )
6 assamulgscm.p ⊢ ↑ = ( .g ‘ 𝐺 )
7 assamulgscm.h ⊢ 𝐻 = ( mulGrp ‘ 𝑊 )
8 assamulgscm.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
9 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( 0 𝐸 ( 𝐴 · 𝑋 ) ) )
10 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 𝐴 ) = ( 0 ↑ 𝐴 ) )
11 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 𝐸 𝑋 ) = ( 0 𝐸 𝑋 ) )
12 10 11 oveq12d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) = ( ( 0 ↑ 𝐴 ) · ( 0 𝐸 𝑋 ) ) )
13 9 12 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) ↔ ( 0 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 0 ↑ 𝐴 ) · ( 0 𝐸 𝑋 ) ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 0 → ( ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) ) ↔ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 0 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 0 ↑ 𝐴 ) · ( 0 𝐸 𝑋 ) ) ) ) )
15 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) )
16 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 𝐴 ) = ( 𝑦 ↑ 𝐴 ) )
17 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐸 𝑋 ) = ( 𝑦 𝐸 𝑋 ) )
18 16 17 oveq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) )
19 15 18 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) ↔ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) ) ↔ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) ) )
21 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) )
22 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ 𝐴 ) = ( ( 𝑦 + 1 ) ↑ 𝐴 ) )
23 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 𝐸 𝑋 ) = ( ( 𝑦 + 1 ) 𝐸 𝑋 ) )
24 22 23 oveq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
25 21 24 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) ↔ ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) )
26 25 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) ) ↔ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) ) )
27 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) )
28 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ 𝐴 ) = ( 𝑁 ↑ 𝐴 ) )
29 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 𝐸 𝑋 ) = ( 𝑁 𝐸 𝑋 ) )
30 28 29 oveq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) )
31 27 30 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) ↔ ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) ) )
32 31 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝑥 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑥 ↑ 𝐴 ) · ( 𝑥 𝐸 𝑋 ) ) ) ↔ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) ) ) )
33 1 2 3 4 5 6 7 8 assamulgscmlem1 ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 0 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 0 ↑ 𝐴 ) · ( 0 𝐸 𝑋 ) ) )
34 1 2 3 4 5 6 7 8 assamulgscmlem2 ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) ) )
35 34 a2d ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) ) )
36 14 20 26 32 33 35 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) ) )
37 36 exp4c ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ 𝐵 → ( 𝑋 ∈ 𝑉 → ( 𝑊 ∈ AssAlg → ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) ) ) ) )
38 37 3imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ∈ AssAlg → ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) ) )
39 38 impcom ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) )