Metamath Proof Explorer

Theorem istgp2

Description: A group with a topology is a topological group iff the subtraction operation is continuous. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tgpsubcn.2 ⊢ J = TopOpen ⁡ G
tgpsubcn.3 ⊢ - ˙ = - G
Assertion istgp2 ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J

Proof

Step Hyp Ref Expression
1 tgpsubcn.2 ⊢ J = TopOpen ⁡ G
2 tgpsubcn.3 ⊢ - ˙ = - G
3 tgpgrp ⊢ G ∈ TopGrp → G ∈ Grp
4 tgptps ⊢ G ∈ TopGrp → G ∈ TopSp
5 1 2 tgpsubcn ⊢ G ∈ TopGrp → - ˙ ∈ J × t J Cn J
6 3 4 5 3jca ⊢ G ∈ TopGrp → G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J
7 simp1 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → G ∈ Grp
8 grpmnd ⊢ G ∈ Grp → G ∈ Mnd
9 8 3ad2ant1 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → G ∈ Mnd
10 simp2 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → G ∈ TopSp
11 eqid ⊢ Base G = Base G
12 eqid ⊢ + G = + G
13 eqid ⊢ inv g ⁡ G = inv g ⁡ G
14 7 3ad2ant1 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J ∧ x ∈ Base G ∧ y ∈ Base G → G ∈ Grp
15 simp2 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J ∧ x ∈ Base G ∧ y ∈ Base G → x ∈ Base G
16 simp3 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J ∧ x ∈ Base G ∧ y ∈ Base G → y ∈ Base G
17 11 12 2 13 14 15 16 grpsubinv ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J ∧ x ∈ Base G ∧ y ∈ Base G → x - ˙ inv g ⁡ G ⁡ y = x + G y
18 17 mpoeq3dva ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G , y ∈ Base G ⟼ x - ˙ inv g ⁡ G ⁡ y = x ∈ Base G , y ∈ Base G ⟼ x + G y
19 eqid ⊢ + 𝑓 ⁡ G = + 𝑓 ⁡ G
20 11 12 19 plusffval ⊢ + 𝑓 ⁡ G = x ∈ Base G , y ∈ Base G ⟼ x + G y
21 18 20 eqtr4di ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G , y ∈ Base G ⟼ x - ˙ inv g ⁡ G ⁡ y = + 𝑓 ⁡ G
22 11 1 istps ⊢ G ∈ TopSp ↔ J ∈ TopOn ⁡ Base G
23 10 22 sylib ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → J ∈ TopOn ⁡ Base G
24 23 23 cnmpt1st ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G , y ∈ Base G ⟼ x ∈ J × t J Cn J
25 23 23 cnmpt2nd ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G , y ∈ Base G ⟼ y ∈ J × t J Cn J
26 11 13 grpinvf ⊢ G ∈ Grp → inv g ⁡ G : Base G ⟶ Base G
27 26 3ad2ant1 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → inv g ⁡ G : Base G ⟶ Base G
28 27 feqmptd ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → inv g ⁡ G = x ∈ Base G ⟼ inv g ⁡ G ⁡ x
29 eqid ⊢ 0 G = 0 G
30 11 2 13 29 grpinvval2 ⊢ G ∈ Grp ∧ x ∈ Base G → inv g ⁡ G ⁡ x = 0 G - ˙ x
31 7 30 sylan ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J ∧ x ∈ Base G → inv g ⁡ G ⁡ x = 0 G - ˙ x
32 31 mpteq2dva ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G ⟼ inv g ⁡ G ⁡ x = x ∈ Base G ⟼ 0 G - ˙ x
33 28 32 eqtrd ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → inv g ⁡ G = x ∈ Base G ⟼ 0 G - ˙ x
34 11 29 grpidcl ⊢ G ∈ Grp → 0 G ∈ Base G
35 34 3ad2ant1 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → 0 G ∈ Base G
36 23 23 35 cnmptc ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G ⟼ 0 G ∈ J Cn J
37 23 cnmptid ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G ⟼ x ∈ J Cn J
38 simp3 ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → - ˙ ∈ J × t J Cn J
39 23 36 37 38 cnmpt12f ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G ⟼ 0 G - ˙ x ∈ J Cn J
40 33 39 eqeltrd ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → inv g ⁡ G ∈ J Cn J
41 23 23 25 40 cnmpt21f ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G , y ∈ Base G ⟼ inv g ⁡ G ⁡ y ∈ J × t J Cn J
42 23 23 24 41 38 cnmpt22f ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → x ∈ Base G , y ∈ Base G ⟼ x - ˙ inv g ⁡ G ⁡ y ∈ J × t J Cn J
43 21 42 eqeltrrd ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → + 𝑓 ⁡ G ∈ J × t J Cn J
44 19 1 istmd ⊢ G ∈ TopMnd ↔ G ∈ Mnd ∧ G ∈ TopSp ∧ + 𝑓 ⁡ G ∈ J × t J Cn J
45 9 10 43 44 syl3anbrc ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → G ∈ TopMnd
46 1 13 istgp ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopMnd ∧ inv g ⁡ G ∈ J Cn J
47 7 45 40 46 syl3anbrc ⊢ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J → G ∈ TopGrp
48 6 47 impbii ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopSp ∧ - ˙ ∈ J × t J Cn J