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