Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  snclseqg Structured version   Visualization version   GIF version

Theorem snclseqg 22829
 Description: The coset of the closure of the identity is the closure of a point. (Contributed by Mario Carneiro, 22-Sep-2015.)
Hypotheses
Ref Expression
snclseqg.x 𝑋 = (Base‘𝐺)
snclseqg.j 𝐽 = (TopOpen‘𝐺)
snclseqg.z 0 = (0g𝐺)
snclseqg.r = (𝐺 ~QG 𝑆)
snclseqg.s 𝑆 = ((cls‘𝐽)‘{ 0 })
Assertion
Ref Expression
snclseqg ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] = ((cls‘𝐽)‘{𝐴}))

Proof of Theorem snclseqg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snclseqg.s . . . 4 𝑆 = ((cls‘𝐽)‘{ 0 })
21imaeq2i 5904 . . 3 ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ 𝑆) = ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ ((cls‘𝐽)‘{ 0 }))
3 tgpgrp 22791 . . . . 5 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
43adantr 484 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐺 ∈ Grp)
5 snclseqg.j . . . . . . . . . 10 𝐽 = (TopOpen‘𝐺)
6 snclseqg.x . . . . . . . . . 10 𝑋 = (Base‘𝐺)
75, 6tgptopon 22795 . . . . . . . . 9 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
87adantr 484 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐽 ∈ (TopOn‘𝑋))
9 topontop 21626 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
108, 9syl 17 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐽 ∈ Top)
11 snclseqg.z . . . . . . . . . . 11 0 = (0g𝐺)
126, 11grpidcl 18211 . . . . . . . . . 10 (𝐺 ∈ Grp → 0𝑋)
134, 12syl 17 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 0𝑋)
1413snssd 4702 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → { 0 } ⊆ 𝑋)
15 toponuni 21627 . . . . . . . . 9 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
168, 15syl 17 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝑋 = 𝐽)
1714, 16sseqtrd 3934 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → { 0 } ⊆ 𝐽)
18 eqid 2758 . . . . . . . 8 𝐽 = 𝐽
1918clsss3 21772 . . . . . . 7 ((𝐽 ∈ Top ∧ { 0 } ⊆ 𝐽) → ((cls‘𝐽)‘{ 0 }) ⊆ 𝐽)
2010, 17, 19syl2anc 587 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((cls‘𝐽)‘{ 0 }) ⊆ 𝐽)
2120, 16sseqtrrd 3935 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((cls‘𝐽)‘{ 0 }) ⊆ 𝑋)
221, 21eqsstrid 3942 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝑆𝑋)
23 simpr 488 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐴𝑋)
24 snclseqg.r . . . . 5 = (𝐺 ~QG 𝑆)
25 eqid 2758 . . . . 5 (+g𝐺) = (+g𝐺)
266, 24, 25eqglact 18411 . . . 4 ((𝐺 ∈ Grp ∧ 𝑆𝑋𝐴𝑋) → [𝐴] = ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ 𝑆))
274, 22, 23, 26syl3anc 1368 . . 3 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] = ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ 𝑆))
28 eqid 2758 . . . . 5 (𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) = (𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥))
2928, 6, 25, 5tgplacthmeo 22816 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) ∈ (𝐽Homeo𝐽))
3018hmeocls 22481 . . . 4 (((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) ∈ (𝐽Homeo𝐽) ∧ { 0 } ⊆ 𝐽) → ((cls‘𝐽)‘((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ { 0 })) = ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ ((cls‘𝐽)‘{ 0 })))
3129, 17, 30syl2anc 587 . . 3 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((cls‘𝐽)‘((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ { 0 })) = ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ ((cls‘𝐽)‘{ 0 })))
322, 27, 313eqtr4a 2819 . 2 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] = ((cls‘𝐽)‘((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ { 0 })))
33 df-ima 5541 . . . . 5 ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ { 0 }) = ran ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) ↾ { 0 })
3414resmptd 5885 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) ↾ { 0 }) = (𝑥 ∈ { 0 } ↦ (𝐴(+g𝐺)𝑥)))
3534rneqd 5784 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ran ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) ↾ { 0 }) = ran (𝑥 ∈ { 0 } ↦ (𝐴(+g𝐺)𝑥)))
3633, 35syl5eq 2805 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ { 0 }) = ran (𝑥 ∈ { 0 } ↦ (𝐴(+g𝐺)𝑥)))
3711fvexi 6677 . . . . . . . 8 0 ∈ V
38 oveq2 7164 . . . . . . . . 9 (𝑥 = 0 → (𝐴(+g𝐺)𝑥) = (𝐴(+g𝐺) 0 ))
3938eqeq2d 2769 . . . . . . . 8 (𝑥 = 0 → (𝑦 = (𝐴(+g𝐺)𝑥) ↔ 𝑦 = (𝐴(+g𝐺) 0 )))
4037, 39rexsn 4580 . . . . . . 7 (∃𝑥 ∈ { 0 }𝑦 = (𝐴(+g𝐺)𝑥) ↔ 𝑦 = (𝐴(+g𝐺) 0 ))
416, 25, 11grprid 18214 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝐴𝑋) → (𝐴(+g𝐺) 0 ) = 𝐴)
423, 41sylan 583 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐴(+g𝐺) 0 ) = 𝐴)
4342eqeq2d 2769 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝑦 = (𝐴(+g𝐺) 0 ) ↔ 𝑦 = 𝐴))
4440, 43syl5bb 286 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (∃𝑥 ∈ { 0 }𝑦 = (𝐴(+g𝐺)𝑥) ↔ 𝑦 = 𝐴))
4544abbidv 2822 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → {𝑦 ∣ ∃𝑥 ∈ { 0 }𝑦 = (𝐴(+g𝐺)𝑥)} = {𝑦𝑦 = 𝐴})
46 eqid 2758 . . . . . 6 (𝑥 ∈ { 0 } ↦ (𝐴(+g𝐺)𝑥)) = (𝑥 ∈ { 0 } ↦ (𝐴(+g𝐺)𝑥))
4746rnmpt 5801 . . . . 5 ran (𝑥 ∈ { 0 } ↦ (𝐴(+g𝐺)𝑥)) = {𝑦 ∣ ∃𝑥 ∈ { 0 }𝑦 = (𝐴(+g𝐺)𝑥)}
48 df-sn 4526 . . . . 5 {𝐴} = {𝑦𝑦 = 𝐴}
4945, 47, 483eqtr4g 2818 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ran (𝑥 ∈ { 0 } ↦ (𝐴(+g𝐺)𝑥)) = {𝐴})
5036, 49eqtrd 2793 . . 3 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ { 0 }) = {𝐴})
5150fveq2d 6667 . 2 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((cls‘𝐽)‘((𝑥𝑋 ↦ (𝐴(+g𝐺)𝑥)) “ { 0 })) = ((cls‘𝐽)‘{𝐴}))
5232, 51eqtrd 2793 1 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] = ((cls‘𝐽)‘{𝐴}))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2735  ∃wrex 3071   ⊆ wss 3860  {csn 4525  ∪ cuni 4801   ↦ cmpt 5116  ran crn 5529   ↾ cres 5530   “ cima 5531  ‘cfv 6340  (class class class)co 7156  [cec 8303  Basecbs 16554  +gcplusg 16636  TopOpenctopn 16766  0gc0g 16784  Grpcgrp 18182   ~QG cqg 18355  Topctop 21606  TopOnctopon 21623  clsccl 21731  Homeochmeo 22466  TopGrpctgp 22784 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7699  df-2nd 7700  df-ec 8307  df-map 8424  df-0g 16786  df-topgen 16788  df-plusf 17930  df-mgm 17931  df-sgrp 17980  df-mnd 17991  df-grp 18185  df-minusg 18186  df-eqg 18358  df-top 21607  df-topon 21624  df-topsp 21646  df-bases 21659  df-cld 21732  df-cls 21734  df-cn 21940  df-cnp 21941  df-tx 22275  df-hmeo 22468  df-tmd 22785  df-tgp 22786 This theorem is referenced by:  tgptsmscls  22863
 Copyright terms: Public domain W3C validator