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 𝐽 ) ) )