| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7438 | . . . . 5
⊢ (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥)) | 
| 2 |  | tgpmulg.b | . . . . . 6
⊢ 𝐵 = (Base‘𝐺) | 
| 3 |  | eqid 2737 | . . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 4 |  | tgpmulg.t | . . . . . 6
⊢  · =
(.g‘𝐺) | 
| 5 | 2, 3, 4 | mulg0 19092 | . . . . 5
⊢ (𝑥 ∈ 𝐵 → (0 · 𝑥) = (0g‘𝐺)) | 
| 6 | 1, 5 | sylan9eq 2797 | . . . 4
⊢ ((𝑛 = 0 ∧ 𝑥 ∈ 𝐵) → (𝑛 · 𝑥) = (0g‘𝐺)) | 
| 7 | 6 | mpteq2dva 5242 | . . 3
⊢ (𝑛 = 0 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (0g‘𝐺))) | 
| 8 | 7 | eleq1d 2826 | . 2
⊢ (𝑛 = 0 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (0g‘𝐺)) ∈ (𝐽 Cn 𝐽))) | 
| 9 |  | oveq1 7438 | . . . 4
⊢ (𝑛 = 𝑘 → (𝑛 · 𝑥) = (𝑘 · 𝑥)) | 
| 10 | 9 | mpteq2dv 5244 | . . 3
⊢ (𝑛 = 𝑘 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥))) | 
| 11 | 10 | eleq1d 2826 | . 2
⊢ (𝑛 = 𝑘 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽))) | 
| 12 |  | oveq1 7438 | . . . 4
⊢ (𝑛 = (𝑘 + 1) → (𝑛 · 𝑥) = ((𝑘 + 1) · 𝑥)) | 
| 13 | 12 | mpteq2dv 5244 | . . 3
⊢ (𝑛 = (𝑘 + 1) → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥))) | 
| 14 | 13 | eleq1d 2826 | . 2
⊢ (𝑛 = (𝑘 + 1) → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽))) | 
| 15 |  | oveq1 7438 | . . . 4
⊢ (𝑛 = 𝑁 → (𝑛 · 𝑥) = (𝑁 · 𝑥)) | 
| 16 | 15 | mpteq2dv 5244 | . . 3
⊢ (𝑛 = 𝑁 → (𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥))) | 
| 17 | 16 | eleq1d 2826 | . 2
⊢ (𝑛 = 𝑁 → ((𝑥 ∈ 𝐵 ↦ (𝑛 · 𝑥)) ∈ (𝐽 Cn 𝐽) ↔ (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽))) | 
| 18 |  | tgpmulg.j | . . . 4
⊢ 𝐽 = (TopOpen‘𝐺) | 
| 19 | 18, 2 | tmdtopon 24089 | . . 3
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) | 
| 20 |  | tmdmnd 24083 | . . . 4
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) | 
| 21 | 2, 3 | mndidcl 18762 | . . . 4
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) | 
| 22 | 20, 21 | syl 17 | . . 3
⊢ (𝐺 ∈ TopMnd →
(0g‘𝐺)
∈ 𝐵) | 
| 23 | 19, 19, 22 | cnmptc 23670 | . 2
⊢ (𝐺 ∈ TopMnd → (𝑥 ∈ 𝐵 ↦ (0g‘𝐺)) ∈ (𝐽 Cn 𝐽)) | 
| 24 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 𝑦 → ((𝑘 + 1) · 𝑥) = ((𝑘 + 1) · 𝑦)) | 
| 25 | 24 | cbvmptv 5255 | . . . 4
⊢ (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) = (𝑦 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑦)) | 
| 26 |  | eqid 2737 | . . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 27 | 2, 4, 26 | mulgnn0p1 19103 | . . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0
∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) | 
| 28 | 20, 27 | syl3an1 1164 | . . . . . 6
⊢ ((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0
∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) | 
| 29 | 28 | ad4ant124 1174 | . . . . 5
⊢ ((((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) ∧ 𝑦 ∈ 𝐵) → ((𝑘 + 1) · 𝑦) = ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) | 
| 30 | 29 | mpteq2dva 5242 | . . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝑘 · 𝑦)(+g‘𝐺)𝑦))) | 
| 31 | 25, 30 | eqtrid 2789 | . . 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 7439 | . . . . . 6
⊢ (𝑥 = 𝑦 → (𝑘 · 𝑥) = (𝑘 · 𝑦)) | 
| 35 | 34 | cbvmptv 5255 | . . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) = (𝑦 ∈ 𝐵 ↦ (𝑘 · 𝑦)) | 
| 36 |  | simpr 484 | . . . . 5
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) | 
| 37 | 35, 36 | eqeltrrid 2846 | . . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ (𝑘 · 𝑦)) ∈ (𝐽 Cn 𝐽)) | 
| 38 | 33 | cnmptid 23669 | . . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ 𝑦) ∈ (𝐽 Cn 𝐽)) | 
| 39 | 18, 26, 32, 33, 37, 38 | cnmpt1plusg 24095 | . . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑦 ∈ 𝐵 ↦ ((𝑘 · 𝑦)(+g‘𝐺)𝑦)) ∈ (𝐽 Cn 𝐽)) | 
| 40 | 31, 39 | eqeltrd 2841 | . 2
⊢ (((𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0)
∧ (𝑥 ∈ 𝐵 ↦ (𝑘 · 𝑥)) ∈ (𝐽 Cn 𝐽)) → (𝑥 ∈ 𝐵 ↦ ((𝑘 + 1) · 𝑥)) ∈ (𝐽 Cn 𝐽)) | 
| 41 | 8, 11, 14, 17, 23, 40 | nn0indd 12715 | 1
⊢ ((𝐺 ∈ TopMnd ∧ 𝑁 ∈ ℕ0)
→ (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽)) |