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 𝐽 = ( TopOpen ‘ 𝐺 )
tgpsubcn.3 = ( -g𝐺 )
Assertion istgp2 ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )

Proof

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