| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tgpgrp 24086 | . . 3
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) | 
| 2 |  | tgptps 24088 | . . 3
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp) | 
| 3 |  | tgpsubcn.2 | . . . 4
⊢ 𝐽 = (TopOpen‘𝐺) | 
| 4 |  | tgpsubcn.3 | . . . 4
⊢  − =
(-g‘𝐺) | 
| 5 | 3, 4 | tgpsubcn 24098 | . . 3
⊢ (𝐺 ∈ TopGrp → − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) | 
| 6 | 1, 2, 5 | 3jca 1129 | . 2
⊢ (𝐺 ∈ TopGrp → (𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽))) | 
| 7 |  | simp1 1137 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → 𝐺 ∈ Grp) | 
| 8 |  | grpmnd 18958 | . . . . 5
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | 
| 9 | 8 | 3ad2ant1 1134 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → 𝐺 ∈ Mnd) | 
| 10 |  | simp2 1138 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → 𝐺 ∈ TopSp) | 
| 11 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 12 |  | eqid 2737 | . . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 13 |  | eqid 2737 | . . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 14 | 7 | 3ad2ant1 1134 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝐺 ∈ Grp) | 
| 15 |  | simp2 1138 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑥 ∈ (Base‘𝐺)) | 
| 16 |  | simp3 1139 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → 𝑦 ∈ (Base‘𝐺)) | 
| 17 | 11, 12, 4, 13, 14, 15, 16 | grpsubinv 19030 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥 −
((invg‘𝐺)‘𝑦)) = (𝑥(+g‘𝐺)𝑦)) | 
| 18 | 17 | mpoeq3dva 7510 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 −
((invg‘𝐺)‘𝑦))) = (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥(+g‘𝐺)𝑦))) | 
| 19 |  | eqid 2737 | . . . . . . 7
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) | 
| 20 | 11, 12, 19 | plusffval 18659 | . . . . . 6
⊢
(+𝑓‘𝐺) = (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥(+g‘𝐺)𝑦)) | 
| 21 | 18, 20 | eqtr4di 2795 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 −
((invg‘𝐺)‘𝑦))) = (+𝑓‘𝐺)) | 
| 22 | 11, 3 | istps 22940 | . . . . . . 7
⊢ (𝐺 ∈ TopSp ↔ 𝐽 ∈
(TopOn‘(Base‘𝐺))) | 
| 23 | 10, 22 | sylib 218 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → 𝐽 ∈ (TopOn‘(Base‘𝐺))) | 
| 24 | 23, 23 | cnmpt1st 23676 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ 𝑥) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 25 | 23, 23 | cnmpt2nd 23677 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ 𝑦) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 26 | 11, 13 | grpinvf 19004 | . . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) | 
| 27 | 26 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) | 
| 28 | 27 | feqmptd 6977 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥))) | 
| 29 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 30 | 11, 4, 13, 29 | grpinvval2 19041 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) →
((invg‘𝐺)‘𝑥) = ((0g‘𝐺) − 𝑥)) | 
| 31 | 7, 30 | sylan 580 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = ((0g‘𝐺) − 𝑥)) | 
| 32 | 31 | mpteq2dva 5242 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)) = (𝑥 ∈ (Base‘𝐺) ↦ ((0g‘𝐺) − 𝑥))) | 
| 33 | 28, 32 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ ((0g‘𝐺) − 𝑥))) | 
| 34 | 11, 29 | grpidcl 18983 | . . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (Base‘𝐺)) | 
| 35 | 34 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (0g‘𝐺) ∈ (Base‘𝐺)) | 
| 36 | 23, 23, 35 | cnmptc 23670 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺) ↦ (0g‘𝐺)) ∈ (𝐽 Cn 𝐽)) | 
| 37 | 23 | cnmptid 23669 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺) ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) | 
| 38 |  | simp3 1139 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 39 | 23, 36, 37, 38 | cnmpt12f 23674 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺) ↦ ((0g‘𝐺) − 𝑥)) ∈ (𝐽 Cn 𝐽)) | 
| 40 | 33, 39 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (invg‘𝐺) ∈ (𝐽 Cn 𝐽)) | 
| 41 | 23, 23, 25, 40 | cnmpt21f 23680 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 42 | 23, 23, 24, 41, 38 | cnmpt22f 23683 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 −
((invg‘𝐺)‘𝑦))) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 43 | 21, 42 | eqeltrrd 2842 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → (+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 44 | 19, 3 | istmd 24082 | . . . 4
⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧
(+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) | 
| 45 | 9, 10, 43, 44 | syl3anbrc 1344 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → 𝐺 ∈ TopMnd) | 
| 46 | 3, 13 | istgp 24085 | . . 3
⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧
(invg‘𝐺)
∈ (𝐽 Cn 𝐽))) | 
| 47 | 7, 45, 40, 46 | syl3anbrc 1344 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽)) → 𝐺 ∈ TopGrp) | 
| 48 | 6, 47 | impbii 209 | 1
⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈
((𝐽 ×t
𝐽) Cn 𝐽))) |