Step | Hyp | Ref
| Expression |
1 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑥𝐸(𝐴 · 𝑋)) = (0𝐸(𝐴 · 𝑋))) |
2 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑥 ↑ 𝐴) = (0 ↑ 𝐴)) |
3 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑥𝐸𝑋) = (0𝐸𝑋)) |
4 | 2, 3 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋)) = ((0 ↑ 𝐴) · (0𝐸𝑋))) |
5 | 1, 4 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑥𝐸(𝐴 · 𝑋)) = ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋)) ↔ (0𝐸(𝐴 · 𝑋)) = ((0 ↑ 𝐴) · (0𝐸𝑋)))) |
6 | 5 | imbi2d 344 |
. . . . 5
⊢ (𝑥 = 0 → ((((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (𝑥𝐸(𝐴 · 𝑋)) = ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋))) ↔ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (0𝐸(𝐴 · 𝑋)) = ((0 ↑ 𝐴) · (0𝐸𝑋))))) |
7 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥𝐸(𝐴 · 𝑋)) = (𝑦𝐸(𝐴 · 𝑋))) |
8 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ↑ 𝐴) = (𝑦 ↑ 𝐴)) |
9 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥𝐸𝑋) = (𝑦𝐸𝑋)) |
10 | 8, 9 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) |
11 | 7, 10 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥𝐸(𝐴 · 𝑋)) = ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋)) ↔ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)))) |
12 | 11 | imbi2d 344 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (𝑥𝐸(𝐴 · 𝑋)) = ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋))) ↔ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))))) |
13 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑥𝐸(𝐴 · 𝑋)) = ((𝑦 + 1)𝐸(𝐴 · 𝑋))) |
14 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ↑ 𝐴) = ((𝑦 + 1) ↑ 𝐴)) |
15 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝑥𝐸𝑋) = ((𝑦 + 1)𝐸𝑋)) |
16 | 14, 15 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) |
17 | 13, 16 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝑥𝐸(𝐴 · 𝑋)) = ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋)) ↔ ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋)))) |
18 | 17 | imbi2d 344 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (𝑥𝐸(𝐴 · 𝑋)) = ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋))) ↔ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))))) |
19 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑥𝐸(𝐴 · 𝑋)) = (𝑁𝐸(𝐴 · 𝑋))) |
20 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑥 ↑ 𝐴) = (𝑁 ↑ 𝐴)) |
21 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑥𝐸𝑋) = (𝑁𝐸𝑋)) |
22 | 20, 21 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋)) = ((𝑁 ↑ 𝐴) · (𝑁𝐸𝑋))) |
23 | 19, 22 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝑥𝐸(𝐴 · 𝑋)) = ((𝑥 ↑ 𝐴) · (𝑥𝐸𝑋)) ↔ (𝑁𝐸(𝐴 · 𝑋)) = ((𝑁 ↑ 𝐴) · (𝑁𝐸𝑋)))) |
24 | 23 | imbi2d 344 |
. . . . 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 20859 |
. . . . 5
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (0𝐸(𝐴 · 𝑋)) = ((0 ↑ 𝐴) · (0𝐸𝑋))) |
34 | 25, 26, 27, 28, 29, 30, 31, 32 | assamulgscmlem2 20860 |
. . . . . 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 12272 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (𝑁𝐸(𝐴 · 𝑋)) = ((𝑁 ↑ 𝐴) · (𝑁𝐸𝑋)))) |
37 | 36 | exp4c 436 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ 𝐵 → (𝑋 ∈ 𝑉 → (𝑊 ∈ AssAlg → (𝑁𝐸(𝐴 · 𝑋)) = ((𝑁 ↑ 𝐴) · (𝑁𝐸𝑋)))))) |
38 | 37 | 3imp 1113 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝑊 ∈ AssAlg → (𝑁𝐸(𝐴 · 𝑋)) = ((𝑁 ↑ 𝐴) · (𝑁𝐸𝑋)))) |
39 | 38 | impcom 411 |
1
⊢ ((𝑊 ∈ AssAlg ∧ (𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉)) → (𝑁𝐸(𝐴 · 𝑋)) = ((𝑁 ↑ 𝐴) · (𝑁𝐸𝑋))) |