Step | Hyp | Ref
| Expression |
1 | | oveq1 7220 |
. . . . 5
⊢ (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥)) |
2 | | tgpmulg.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
3 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
4 | | tgpmulg.t |
. . . . . 6
⊢ · =
(.g‘𝐺) |
5 | 2, 3, 4 | mulg0 18495 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 → (0 · 𝑥) = (0g‘𝐺)) |
6 | 1, 5 | sylan9eq 2798 |
. . . 4
⊢ ((𝑛 = 0 ∧ 𝑥 ∈ 𝐵) → (𝑛 · 𝑥) = (0g‘𝐺)) |
7 | 6 | mpteq2dva 5150 |
. . 3
⊢ (𝑛 = 0 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (0g‘𝐺))) |
8 | 7 | eleq1d 2822 |
. 2
⊢ (𝑛 = 0 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (0g‘𝐺)) ∈ (𝐽 Cn 𝐽))) |
9 | | oveq1 7220 |
. . . 4
⊢ (𝑛 = 𝑘 → (𝑛 · 𝑥) = (𝑘 · 𝑥)) |
10 | 9 | mpteq2dv 5151 |
. . 3
⊢ (𝑛 = 𝑘 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥))) |
11 | 10 | eleq1d 2822 |
. 2
⊢ (𝑛 = 𝑘 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽))) |
12 | | oveq1 7220 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → (𝑛 · 𝑥) = ((𝑘 + 1) · 𝑥)) |
13 | 12 | mpteq2dv 5151 |
. . 3
⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥))) |
14 | 13 | eleq1d 2822 |
. 2
⊢ (𝑛 = (𝑘 + 1) → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽))) |
15 | | oveq1 7220 |
. . . 4
⊢ (𝑛 = 𝑁 → (𝑛 · 𝑥) = (𝑁 · 𝑥)) |
16 | 15 | mpteq2dv 5151 |
. . 3
⊢ (𝑛 = 𝑁 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥))) |
17 | 16 | eleq1d 2822 |
. 2
⊢ (𝑛 = 𝑁 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽))) |
18 | | tgpmulg.j |
. . . 4
⊢ 𝐽 = (TopOpen‘𝐺) |
19 | 18, 2 | tmdtopon 22978 |
. . 3
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) |
20 | | tmdmnd 22972 |
. . . 4
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) |
21 | 2, 3 | mndidcl 18188 |
. . . 4
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) |
22 | 20, 21 | syl 17 |
. . 3
⊢ (𝐺 ∈ TopMnd →
(0g‘𝐺)
∈ 𝐵) |
23 | 19, 19, 22 | cnmptc 22559 |
. 2
⊢ (𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (0g‘𝐺)) ∈ (𝐽 Cn 𝐽)) |
24 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑘 + 1) · 𝑥) = ((𝑘 + 1) · 𝑦)) |
25 | 24 | cbvmptv 5158 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) = (𝑦 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑦)) |
26 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
27 | 2, 4, 26 | mulgnn0p1 18503 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) |
28 | 20, 27 | syl3an1 1165 |
. . . . . 6
⊢ ((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0
∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) |
29 | 28 | ad4ant124 1175 |
. . . . 5
⊢ ((((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) ∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) |
30 | 29 | mpteq2dva 5150 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝑘 · 𝑦)(+g‘𝐺)𝑦))) |
31 | 25, 30 | syl5eq 2790 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) = (𝑦 ∈ 𝐵 ↦ ((𝑘 · 𝑦)(+g‘𝐺)𝑦))) |
32 | | simpll 767 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → 𝐺 ∈ TopMnd) |
33 | 32, 19 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → 𝐽 ∈ (TopOn‘𝐵)) |
34 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑘 · 𝑥) = (𝑘 · 𝑦)) |
35 | 34 | cbvmptv 5158 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) = (𝑦 ∈ 𝐵 ↦ (𝑘 · 𝑦)) |
36 | | simpr 488 |
. . . . 5
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) |
37 | 35, 36 | eqeltrrid 2843 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ (𝑘 · 𝑦)) ∈ (𝐽 Cn 𝐽)) |
38 | 33 | cnmptid 22558 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ 𝑦) ∈ (𝐽 Cn 𝐽)) |
39 | 18, 26, 32, 33, 37, 38 | cnmpt1plusg 22984 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) ∈ (𝐽 Cn 𝐽)) |
40 | 31, 39 | eqeltrd 2838 |
. 2
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽)) |
41 | 8, 11, 14, 17, 23, 40 | nn0indd 12274 |
1
⊢ ((𝐺 ∈ TopMnd ∧ 𝑁 ∈ ℕ0)
→ (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽)) |