Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥)) |
2 | | tgpmulg.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
3 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
4 | | tgpmulg.t |
. . . . . . . 8
⊢ · =
(.g‘𝐺) |
5 | 2, 3, 4 | mulg0 17369 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → (0 · 𝑥) = (0g‘𝐺)) |
6 | 1, 5 | sylan9eq 2664 |
. . . . . 6
⊢ ((𝑛 = 0 ∧ 𝑥 ∈ 𝐵) → (𝑛 · 𝑥) = (0g‘𝐺)) |
7 | 6 | mpteq2dva 4672 |
. . . . 5
⊢ (𝑛 = 0 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (0g‘𝐺))) |
8 | 7 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = 0 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (0g‘𝐺)) ∈ (𝐽 Cn 𝐽))) |
9 | 8 | imbi2d 329 |
. . 3
⊢ (𝑛 = 0 → ((𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽)) ↔ (𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (0g‘𝐺)) ∈ (𝐽 Cn 𝐽)))) |
10 | | oveq1 6556 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 · 𝑥) = (𝑘 · 𝑥)) |
11 | 10 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥))) |
12 | 11 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = 𝑘 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽))) |
13 | 12 | imbi2d 329 |
. . 3
⊢ (𝑛 = 𝑘 → ((𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽)) ↔ (𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)))) |
14 | | oveq1 6556 |
. . . . . 6
⊢ (𝑛 = (𝑘 + 1) → (𝑛 · 𝑥) = ((𝑘 + 1) · 𝑥)) |
15 | 14 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥))) |
16 | 15 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽))) |
17 | 16 | imbi2d 329 |
. . 3
⊢ (𝑛 = (𝑘 + 1) → ((𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽)) ↔ (𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽)))) |
18 | | oveq1 6556 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 · 𝑥) = (𝑁 · 𝑥)) |
19 | 18 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥))) |
20 | 19 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽))) |
21 | 20 | imbi2d 329 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽)) ↔ (𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽)))) |
22 | | tgpmulg.j |
. . . . 5
⊢ 𝐽 = (TopOpen‘𝐺) |
23 | 22, 2 | tmdtopon 21695 |
. . . 4
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) |
24 | | tmdmnd 21689 |
. . . . 5
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) |
25 | 2, 3 | mndidcl 17131 |
. . . . 5
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) |
26 | 24, 25 | syl 17 |
. . . 4
⊢ (𝐺 ∈ TopMnd →
(0g‘𝐺)
∈ 𝐵) |
27 | 23, 23, 26 | cnmptc 21275 |
. . 3
⊢ (𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (0g‘𝐺)) ∈ (𝐽 Cn 𝐽)) |
28 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑘 + 1) · 𝑥) = ((𝑘 + 1) · 𝑦)) |
29 | 28 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) = (𝑦 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑦)) |
30 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(+g‘𝐺) = (+g‘𝐺) |
31 | 2, 4, 30 | mulgnn0p1 17375 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) |
32 | 24, 31 | syl3an1 1351 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0
∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) |
33 | 32 | 3expa 1257 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) |
34 | 33 | adantlr 747 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) ∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) |
35 | 34 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝑘 · 𝑦)(+g‘𝐺)𝑦))) |
36 | 29, 35 | syl5eq 2656 |
. . . . . . 7
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) = (𝑦 ∈ 𝐵 ↦ ((𝑘 · 𝑦)(+g‘𝐺)𝑦))) |
37 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → 𝐺 ∈ TopMnd) |
38 | 37, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → 𝐽 ∈ (TopOn‘𝐵)) |
39 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑘 · 𝑥) = (𝑘 · 𝑦)) |
40 | 39 | cbvmptv 4678 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) = (𝑦 ∈ 𝐵 ↦ (𝑘 · 𝑦)) |
41 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) |
42 | 40, 41 | syl5eqelr 2693 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ (𝑘 · 𝑦)) ∈ (𝐽 Cn 𝐽)) |
43 | 38 | cnmptid 21274 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ 𝑦) ∈ (𝐽 Cn 𝐽)) |
44 | 22, 30, 37, 38, 42, 43 | cnmpt1plusg 21701 |
. . . . . . 7
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) ∈ (𝐽 Cn 𝐽)) |
45 | 36, 44 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽)) |
46 | 45 | ex 449 |
. . . . 5
⊢ ((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
→ ((𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽) → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽))) |
47 | 46 | expcom 450 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐺 ∈ TopMnd
→ ((𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽) → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽)))) |
48 | 47 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝐺 ∈ TopMnd
→ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽)))) |
49 | 9, 13, 17, 21, 27, 48 | nn0ind 11348 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐺 ∈ TopMnd
→ (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽))) |
50 | 49 | impcom 445 |
1
⊢ ((𝐺 ∈ TopMnd ∧ 𝑁 ∈ ℕ0)
→ (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽)) |