Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgpsubcn Unicode version

Theorem tgpsubcn 18059
 Description: In a topological group, the "subtraction" (or "division") is continuous. Axiom GT' of [BourbakiTop1] p. III.1 (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 19-Mar-2015.)
Hypotheses
Ref Expression
tgpsubcn.2
tgpsubcn.3
Assertion
Ref Expression
tgpsubcn

Proof of Theorem tgpsubcn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2401 . . 3
2 eqid 2401 . . 3
3 eqid 2401 . . 3
4 tgpsubcn.3 . . 3
51, 2, 3, 4grpsubfval 14788 . 2
6 tgpsubcn.2 . . 3
7 tgptmd 18048 . . 3 TopMnd
86, 1tgptopon 18051 . . 3 TopOn
98, 8cnmpt1st 17639 . . 3
108, 8cnmpt2nd 17640 . . . 4
116, 3tgpinv 18054 . . . 4
128, 8, 10, 11cnmpt21f 17643 . . 3
136, 2, 7, 8, 8, 9, 12cnmpt2plusg 18057 . 2
145, 13syl5eqel 2485 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1649   wcel 1721  cfv 5408  (class class class)co 6034   cmpt2 6036  cbs 13410   cplusg 13470  ctopn 13590  cminusg 14627  csg 14629   ccn 17228   ctx 17531  ctgp 18040 This theorem is referenced by:  istgp2  18060  clssubg  18077  clsnsg  18078  tgphaus  18085  tgpt0  18087  divstgplem  18089 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-reu 2670  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-op 3780  df-uni 3972  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-id 4453  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-map 6970  df-topgen 13608  df-plusf 14632  df-sbg 14755  df-top 16904  df-bases 16906  df-topon 16907  df-topsp 16908  df-cn 17231  df-tx 17533  df-tmd 18041  df-tgp 18042
 Copyright terms: Public domain W3C validator