| Step | Hyp | Ref
| Expression |
| 1 | | snclseqg.s |
. . . 4
⊢ 𝑆 = ((cls‘𝐽)‘{ 0 }) |
| 2 | 1 | imaeq2i 6076 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ 𝑆) = ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ ((cls‘𝐽)‘{ 0 })) |
| 3 | | tgpgrp 24086 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
| 4 | 3 | adantr 480 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐺 ∈ Grp) |
| 5 | | snclseqg.j |
. . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝐺) |
| 6 | | snclseqg.x |
. . . . . . . . . 10
⊢ 𝑋 = (Base‘𝐺) |
| 7 | 5, 6 | tgptopon 24090 |
. . . . . . . . 9
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
| 8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
| 9 | | topontop 22919 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ Top) |
| 11 | | snclseqg.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝐺) |
| 12 | 6, 11 | grpidcl 18983 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
| 13 | 4, 12 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑋) |
| 14 | 13 | snssd 4809 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → { 0 } ⊆ 𝑋) |
| 15 | | toponuni 22920 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 16 | 8, 15 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑋 = ∪ 𝐽) |
| 17 | 14, 16 | sseqtrd 4020 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → { 0 } ⊆ ∪ 𝐽) |
| 18 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 19 | 18 | clsss3 23067 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ { 0 } ⊆
∪ 𝐽) → ((cls‘𝐽)‘{ 0 }) ⊆ ∪ 𝐽) |
| 20 | 10, 17, 19 | syl2anc 584 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((cls‘𝐽)‘{ 0 }) ⊆ ∪ 𝐽) |
| 21 | 20, 16 | sseqtrrd 4021 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((cls‘𝐽)‘{ 0 }) ⊆ 𝑋) |
| 22 | 1, 21 | eqsstrid 4022 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ 𝑋) |
| 23 | | simpr 484 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋) |
| 24 | | snclseqg.r |
. . . . 5
⊢ ∼ =
(𝐺 ~QG
𝑆) |
| 25 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 26 | 6, 24, 25 | eqglact 19197 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ 𝑆)) |
| 27 | 4, 22, 23, 26 | syl3anc 1373 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ 𝑆)) |
| 28 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) |
| 29 | 28, 6, 25, 5 | tgplacthmeo 24111 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) ∈ (𝐽Homeo𝐽)) |
| 30 | 18 | hmeocls 23776 |
. . . 4
⊢ (((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) ∈ (𝐽Homeo𝐽) ∧ { 0 } ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ { 0 })) = ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ ((cls‘𝐽)‘{ 0 }))) |
| 31 | 29, 17, 30 | syl2anc 584 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((cls‘𝐽)‘((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ { 0 })) = ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ ((cls‘𝐽)‘{ 0 }))) |
| 32 | 2, 27, 31 | 3eqtr4a 2803 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((cls‘𝐽)‘((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ { 0 }))) |
| 33 | | df-ima 5698 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ { 0 }) = ran ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) ↾ { 0 }) |
| 34 | 14 | resmptd 6058 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) ↾ { 0 }) = (𝑥 ∈ { 0 } ↦ (𝐴(+g‘𝐺)𝑥))) |
| 35 | 34 | rneqd 5949 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ran ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) ↾ { 0 }) = ran (𝑥 ∈ { 0 } ↦ (𝐴(+g‘𝐺)𝑥))) |
| 36 | 33, 35 | eqtrid 2789 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ { 0 }) = ran (𝑥 ∈ { 0 } ↦ (𝐴(+g‘𝐺)𝑥))) |
| 37 | 11 | fvexi 6920 |
. . . . . . . 8
⊢ 0 ∈
V |
| 38 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝐴(+g‘𝐺)𝑥) = (𝐴(+g‘𝐺) 0 )) |
| 39 | 38 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑦 = (𝐴(+g‘𝐺)𝑥) ↔ 𝑦 = (𝐴(+g‘𝐺) 0 ))) |
| 40 | 37, 39 | rexsn 4682 |
. . . . . . 7
⊢
(∃𝑥 ∈ {
0 }𝑦 = (𝐴(+g‘𝐺)𝑥) ↔ 𝑦 = (𝐴(+g‘𝐺) 0 )) |
| 41 | 6, 25, 11 | grprid 18986 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴) |
| 42 | 3, 41 | sylan 580 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴) |
| 43 | 42 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑦 = (𝐴(+g‘𝐺) 0 ) ↔ 𝑦 = 𝐴)) |
| 44 | 40, 43 | bitrid 283 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (∃𝑥 ∈ { 0 }𝑦 = (𝐴(+g‘𝐺)𝑥) ↔ 𝑦 = 𝐴)) |
| 45 | 44 | abbidv 2808 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → {𝑦 ∣ ∃𝑥 ∈ { 0 }𝑦 = (𝐴(+g‘𝐺)𝑥)} = {𝑦 ∣ 𝑦 = 𝐴}) |
| 46 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ { 0 } ↦ (𝐴(+g‘𝐺)𝑥)) = (𝑥 ∈ { 0 } ↦ (𝐴(+g‘𝐺)𝑥)) |
| 47 | 46 | rnmpt 5968 |
. . . . 5
⊢ ran
(𝑥 ∈ { 0 } ↦
(𝐴(+g‘𝐺)𝑥)) = {𝑦 ∣ ∃𝑥 ∈ { 0 }𝑦 = (𝐴(+g‘𝐺)𝑥)} |
| 48 | | df-sn 4627 |
. . . . 5
⊢ {𝐴} = {𝑦 ∣ 𝑦 = 𝐴} |
| 49 | 45, 47, 48 | 3eqtr4g 2802 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ran (𝑥 ∈ { 0 } ↦ (𝐴(+g‘𝐺)𝑥)) = {𝐴}) |
| 50 | 36, 49 | eqtrd 2777 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ { 0 }) = {𝐴}) |
| 51 | 50 | fveq2d 6910 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((cls‘𝐽)‘((𝑥 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑥)) “ { 0 })) = ((cls‘𝐽)‘{𝐴})) |
| 52 | 32, 51 | eqtrd 2777 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((cls‘𝐽)‘{𝐴})) |