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 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑁 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 𝐸 𝑋 ) ) )