| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tgptmd 24088 | . . 3
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd) | 
| 2 |  | tgplacthmeo.1 | . . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥)) | 
| 3 |  | tgplacthmeo.2 | . . . 4
⊢ 𝑋 = (Base‘𝐺) | 
| 4 |  | tgplacthmeo.3 | . . . 4
⊢  + =
(+g‘𝐺) | 
| 5 |  | tgplacthmeo.4 | . . . 4
⊢ 𝐽 = (TopOpen‘𝐺) | 
| 6 | 2, 3, 4, 5 | tmdlactcn 24111 | . . 3
⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐽)) | 
| 7 | 1, 6 | sylan 580 | . 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐽)) | 
| 8 |  | tgpgrp 24087 | . . . . . 6
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) | 
| 9 |  | eqid 2736 | . . . . . . 7
⊢ (𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥))) = (𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥))) | 
| 10 |  | eqid 2736 | . . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 11 | 9, 3, 4, 10 | grplactcnv 19062 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘((invg‘𝐺)‘𝐴)))) | 
| 12 | 8, 11 | sylan 580 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘((invg‘𝐺)‘𝐴)))) | 
| 13 | 12 | simprd 495 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ◡((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘((invg‘𝐺)‘𝐴))) | 
| 14 | 9, 3 | grplactfval 19060 | . . . . . . 7
⊢ (𝐴 ∈ 𝑋 → ((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴) = (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥))) | 
| 15 | 14 | adantl 481 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴) = (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥))) | 
| 16 | 15, 2 | eqtr4di 2794 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴) = 𝐹) | 
| 17 | 16 | cnveqd 5885 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ◡((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘𝐴) = ◡𝐹) | 
| 18 | 3, 10 | grpinvcl 19006 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) | 
| 19 | 8, 18 | sylan 580 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) | 
| 20 | 9, 3 | grplactfval 19060 | . . . . 5
⊢
(((invg‘𝐺)‘𝐴) ∈ 𝑋 → ((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘((invg‘𝐺)‘𝐴)) = (𝑥 ∈ 𝑋 ↦ (((invg‘𝐺)‘𝐴) + 𝑥))) | 
| 21 | 19, 20 | syl 17 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑥 ∈ 𝑋 ↦ (𝑔 + 𝑥)))‘((invg‘𝐺)‘𝐴)) = (𝑥 ∈ 𝑋 ↦ (((invg‘𝐺)‘𝐴) + 𝑥))) | 
| 22 | 13, 17, 21 | 3eqtr3d 2784 | . . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ◡𝐹 = (𝑥 ∈ 𝑋 ↦ (((invg‘𝐺)‘𝐴) + 𝑥))) | 
| 23 |  | eqid 2736 | . . . . 5
⊢ (𝑥 ∈ 𝑋 ↦ (((invg‘𝐺)‘𝐴) + 𝑥)) = (𝑥 ∈ 𝑋 ↦ (((invg‘𝐺)‘𝐴) + 𝑥)) | 
| 24 | 23, 3, 4, 5 | tmdlactcn 24111 | . . . 4
⊢ ((𝐺 ∈ TopMnd ∧
((invg‘𝐺)‘𝐴) ∈ 𝑋) → (𝑥 ∈ 𝑋 ↦ (((invg‘𝐺)‘𝐴) + 𝑥)) ∈ (𝐽 Cn 𝐽)) | 
| 25 | 1, 19, 24 | syl2an2r 685 | . . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑥 ∈ 𝑋 ↦ (((invg‘𝐺)‘𝐴) + 𝑥)) ∈ (𝐽 Cn 𝐽)) | 
| 26 | 22, 25 | eqeltrd 2840 | . 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ◡𝐹 ∈ (𝐽 Cn 𝐽)) | 
| 27 |  | ishmeo 23768 | . 2
⊢ (𝐹 ∈ (𝐽Homeo𝐽) ↔ (𝐹 ∈ (𝐽 Cn 𝐽) ∧ ◡𝐹 ∈ (𝐽 Cn 𝐽))) | 
| 28 | 7, 26, 27 | sylanbrc 583 | 1
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ (𝐽Homeo𝐽)) |