Metamath Proof Explorer

Theorem snclseqg

Description: The coset of the closure of the identity is the closure of a point. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses snclseqg.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
snclseqg.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
snclseqg.z ⊢ 0 = ( 0g ‘ 𝐺 )
snclseqg.r ⊢ ∼ = ( 𝐺 ~QG 𝑆 )
snclseqg.s ⊢ 𝑆 = ( ( cls ‘ 𝐽 ) ‘ { 0 } )
Assertion snclseqg ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 snclseqg.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 snclseqg.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 snclseqg.z ⊢ 0 = ( 0g ‘ 𝐺 )
4 snclseqg.r ⊢ ∼ = ( 𝐺 ~QG 𝑆 )
5 snclseqg.s ⊢ 𝑆 = ( ( cls ‘ 𝐽 ) ‘ { 0 } )
6 5 imaeq2i ⊢ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ ( ( cls ‘ 𝐽 ) ‘ { 0 } ) )
7 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
8 7 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐺 ∈ Grp )
9 2 1 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 9 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
12 10 11 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ Top )
13 1 3 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝑋 )
14 8 13 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ∈ 𝑋 )
15 14 snssd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → { 0 } ⊆ 𝑋 )
16 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
17 10 16 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝑋 = ∪ 𝐽 )
18 15 17 sseqtrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → { 0 } ⊆ ∪ 𝐽 )
19 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
20 19 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ { 0 } ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ { 0 } ) ⊆ ∪ 𝐽 )
21 12 18 20 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ { 0 } ) ⊆ ∪ 𝐽 )
22 21 17 sseqtrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ { 0 } ) ⊆ 𝑋 )
23 5 22 eqsstrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ⊆ 𝑋 )
24 simpr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
25 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
26 1 4 25 eqglact ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑆 ) )
27 8 23 24 26 syl3anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑆 ) )
28 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) )
29 28 1 25 2 tgplacthmeo ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
30 19 hmeocls ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) ∈ ( 𝐽 Homeo 𝐽 ) ∧ { 0 } ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ { 0 } ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ ( ( cls ‘ 𝐽 ) ‘ { 0 } ) ) )
31 29 18 30 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ { 0 } ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ ( ( cls ‘ 𝐽 ) ‘ { 0 } ) ) )
32 6 27 31 3eqtr4a ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ { 0 } ) ) )
33 df-ima ⊢ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ { 0 } ) = ran ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) ↾ { 0 } )
34 15 resmptd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) ↾ { 0 } ) = ( 𝑥 ∈ { 0 } ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) )
35 34 rneqd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ran ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) ↾ { 0 } ) = ran ( 𝑥 ∈ { 0 } ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) )
36 33 35 syl5eq ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ { 0 } ) = ran ( 𝑥 ∈ { 0 } ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) )
37 3 fvexi ⊢ 0 ∈ V
38 oveq2 ⊢ ( 𝑥 = 0 → ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝐴 ( +g ‘ 𝐺 ) 0 ) )
39 38 eqeq2d ⊢ ( 𝑥 = 0 → ( 𝑦 = ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ↔ 𝑦 = ( 𝐴 ( +g ‘ 𝐺 ) 0 ) ) )
40 37 39 rexsn ⊢ ( ∃ 𝑥 ∈ { 0 } 𝑦 = ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ↔ 𝑦 = ( 𝐴 ( +g ‘ 𝐺 ) 0 ) )
41 1 25 3 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +g ‘ 𝐺 ) 0 ) = 𝐴 )
42 7 41 sylan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +g ‘ 𝐺 ) 0 ) = 𝐴 )
43 42 eqeq2d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑦 = ( 𝐴 ( +g ‘ 𝐺 ) 0 ) ↔ 𝑦 = 𝐴 ) )
44 40 43 syl5bb ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ { 0 } 𝑦 = ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ↔ 𝑦 = 𝐴 ) )
45 44 abbidv ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → { 𝑦 ∣ ∃ 𝑥 ∈ { 0 } 𝑦 = ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) } = { 𝑦 ∣ 𝑦 = 𝐴 } )
46 eqid ⊢ ( 𝑥 ∈ { 0 } ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑥 ∈ { 0 } ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) )
47 46 rnmpt ⊢ ran ( 𝑥 ∈ { 0 } ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ { 0 } 𝑦 = ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) }
48 df-sn ⊢ { 𝐴 } = { 𝑦 ∣ 𝑦 = 𝐴 }
49 45 47 48 3eqtr4g ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ran ( 𝑥 ∈ { 0 } ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) = { 𝐴 } )
50 36 49 eqtrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ { 0 } ) = { 𝐴 } )
51 50 fveq2d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑥 ) ) “ { 0 } ) ) = ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) )
52 32 51 eqtrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( cls ‘ 𝐽 ) ‘ { 𝐴 } ) )