Step | Hyp | Ref
| Expression |
1 | | tgpconncomp.s |
. . . . 5
⊢ 𝑆 = ∪
{𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} |
2 | | ssrab2 3969 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 |
3 | | sspwuni 4985 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋) |
4 | 2, 3 | mpbi 233 |
. . . . 5
⊢ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋 |
5 | 1, 4 | eqsstri 3911 |
. . . 4
⊢ 𝑆 ⊆ 𝑋 |
6 | 5 | a1i 11 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝑆 ⊆ 𝑋) |
7 | | tgpconncomp.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
8 | | tgpconncomp.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
9 | 7, 8 | tgptopon 22835 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
10 | | tgpgrp 22831 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
11 | | tgpconncomp.z |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
12 | 8, 11 | grpidcl 18251 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
13 | 10, 12 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 0 ∈ 𝑋) |
14 | 1 | conncompid 22184 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆) |
15 | 9, 13, 14 | syl2anc 587 |
. . . 4
⊢ (𝐺 ∈ TopGrp → 0 ∈ 𝑆) |
16 | 15 | ne0d 4224 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝑆 ≠ ∅) |
17 | | df-ima 5538 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) = ran ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) |
18 | | resmpt 5879 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
19 | 5, 18 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
20 | 19 | rneqi 5780 |
. . . . . . . 8
⊢ ran
((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
21 | 17, 20 | eqtri 2761 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) = ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
22 | | imassrn 5914 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) |
23 | 10 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝐺 ∈ Grp) |
24 | 23 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝐺 ∈ Grp) |
25 | 6 | sselda 3877 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑋) |
26 | 25 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
27 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
28 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(-g‘𝐺) = (-g‘𝐺) |
29 | 8, 28 | grpsubcl 18299 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) ∈ 𝑋) |
30 | 24, 26, 27, 29 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) ∈ 𝑋) |
31 | 30 | fmpttd 6891 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)):𝑋⟶𝑋) |
32 | 31 | frnd 6512 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑋) |
33 | 22, 32 | sstrid 3888 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑋) |
34 | 8, 11, 28 | grpsubid 18303 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑦) = 0 ) |
35 | 23, 25, 34 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑦(-g‘𝐺)𝑦) = 0 ) |
36 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
37 | | ovex 7205 |
. . . . . . . . . . 11
⊢ (𝑦(-g‘𝐺)𝑦) ∈ V |
38 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
39 | | oveq2 7180 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑦(-g‘𝐺)𝑧) = (𝑦(-g‘𝐺)𝑦)) |
40 | 38, 39 | elrnmpt1s 5800 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑆 ∧ (𝑦(-g‘𝐺)𝑦) ∈ V) → (𝑦(-g‘𝐺)𝑦) ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
41 | 36, 37, 40 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑦(-g‘𝐺)𝑦) ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
42 | 35, 41 | eqeltrrd 2834 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 0 ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
43 | 42, 21 | eleqtrrdi 2844 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 0 ∈ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) |
44 | | eqid 2738 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
45 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝐺) = (+g‘𝐺) |
46 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(invg‘𝐺) = (invg‘𝐺) |
47 | 8, 45, 46, 28 | grpsubval 18269 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
48 | 25, 47 | sylan 583 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
49 | 48 | mpteq2dva 5125 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧)))) |
50 | 8, 46 | grpinvcl 18271 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
51 | 23, 50 | sylan 583 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
52 | 8, 46 | grpinvf 18270 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):𝑋⟶𝑋) |
53 | 10, 52 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺):𝑋⟶𝑋) |
54 | 53 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺):𝑋⟶𝑋) |
55 | 54 | feqmptd 6739 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺) = (𝑧 ∈ 𝑋 ↦ ((invg‘𝐺)‘𝑧))) |
56 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤))) |
57 | | oveq2 7180 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((invg‘𝐺)‘𝑧) → (𝑦(+g‘𝐺)𝑤) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
58 | 51, 55, 56, 57 | fmptco 6903 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧)))) |
59 | 49, 58 | eqtr4d 2776 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺))) |
60 | 7, 46 | grpinvhmeo 22839 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ (𝐽Homeo𝐽)) |
61 | 60 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺) ∈ (𝐽Homeo𝐽)) |
62 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) |
63 | 62, 8, 45, 7 | tgplacthmeo 22856 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑋) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) |
64 | 25, 63 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) |
65 | | hmeoco 22525 |
. . . . . . . . . . . 12
⊢
(((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
66 | 61, 64, 65 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
67 | 59, 66 | eqeltrd 2833 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽)) |
68 | | hmeocn 22513 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
69 | 67, 68 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
70 | | toponuni 21667 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
71 | 9, 70 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝑋 = ∪
𝐽) |
72 | 71 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑋 = ∪ 𝐽) |
73 | 5, 72 | sseqtrid 3929 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝐽) |
74 | 1 | conncompconn 22185 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn) |
75 | 9, 13, 74 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝐺 ∈ TopGrp → (𝐽 ↾t 𝑆) ∈ Conn) |
76 | 75 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝐽 ↾t 𝑆) ∈ Conn) |
77 | 44, 69, 73, 76 | connima 22178 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn) |
78 | 1 | conncompss 22186 |
. . . . . . . 8
⊢ ((((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑋 ∧ 0 ∈ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ∧ (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑆) |
79 | 33, 43, 77, 78 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑆) |
80 | 21, 79 | eqsstrrid 3926 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆) |
81 | | ovex 7205 |
. . . . . . . 8
⊢ (𝑦(-g‘𝐺)𝑧) ∈ V |
82 | 81, 38 | fnmpti 6480 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) Fn 𝑆 |
83 | | df-f 6343 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆 ↔ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) Fn 𝑆 ∧ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆)) |
84 | 82, 83 | mpbiran 709 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆 ↔ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆) |
85 | 80, 84 | sylibr 237 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆) |
86 | 38 | fmpt 6886 |
. . . . 5
⊢
(∀𝑧 ∈
𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆 ↔ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆) |
87 | 85, 86 | sylibr 237 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆) |
88 | 87 | ralrimiva 3096 |
. . 3
⊢ (𝐺 ∈ TopGrp →
∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆) |
89 | 8, 28 | issubg4 18418 |
. . . 4
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆))) |
90 | 10, 89 | syl 17 |
. . 3
⊢ (𝐺 ∈ TopGrp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆))) |
91 | 6, 16, 88, 90 | mpbir3and 1343 |
. 2
⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (SubGrp‘𝐺)) |
92 | 10 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝐺 ∈ Grp) |
93 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(oppg‘𝐺) = (oppg‘𝐺) |
94 | 93, 46 | oppginv 18607 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
(invg‘𝐺) =
(invg‘(oppg‘𝐺))) |
95 | 92, 94 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (invg‘𝐺) =
(invg‘(oppg‘𝐺))) |
96 | 95 | fveq1d 6678 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) =
((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))) |
97 | | simprll 779 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝑦 ∈ 𝑋) |
98 | 8, 46 | grpinvinv 18286 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) = 𝑦) |
99 | 92, 97, 98 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) = 𝑦) |
100 | 96, 99 | eqtr3d 2775 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦)) = 𝑦) |
101 | 100 | oveq1d 7187 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) = (𝑦(+g‘(oppg‘𝐺))𝑧)) |
102 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘(oppg‘𝐺)) =
(+g‘(oppg‘𝐺)) |
103 | 45, 93, 102 | oppgplus 18597 |
. . . . . 6
⊢ (𝑦(+g‘(oppg‘𝐺))𝑧) = (𝑧(+g‘𝐺)𝑦) |
104 | 101, 103 | eqtrdi 2789 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) = (𝑧(+g‘𝐺)𝑦)) |
105 | 8, 46 | grpinvcl 18271 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
106 | 92, 97, 105 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
107 | | simprlr 780 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝑧 ∈ 𝑋) |
108 | 99 | oveq1d 7187 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = (𝑦(+g‘𝐺)𝑧)) |
109 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝑆) |
110 | 108, 109 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆) |
111 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝐺 ~QG 𝑆) = (𝐺 ~QG 𝑆) |
112 | 8, 46, 45, 111 | eqgval 18449 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆))) |
113 | 92, 5, 112 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆))) |
114 | 106, 107,
110, 113 | mpbir3and 1343 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧) |
115 | 8, 11, 7, 1, 111 | tgpconncompeqg 22865 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧
((invg‘𝐺)‘𝑦) ∈ 𝑋) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = ∪ {𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
116 | 106, 115 | syldan 594 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = ∪ {𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
117 | 93 | oppgtgp 22851 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp →
(oppg‘𝐺) ∈ TopGrp) |
118 | 117 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(oppg‘𝐺) ∈ TopGrp) |
119 | 93, 8 | oppgbas 18599 |
. . . . . . . . . . . . 13
⊢ 𝑋 =
(Base‘(oppg‘𝐺)) |
120 | 93, 11 | oppgid 18604 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘(oppg‘𝐺)) |
121 | 93, 7 | oppgtopn 18601 |
. . . . . . . . . . . . 13
⊢ 𝐽 =
(TopOpen‘(oppg‘𝐺)) |
122 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
((oppg‘𝐺) ~QG 𝑆) = ((oppg‘𝐺) ~QG 𝑆) |
123 | 119, 120,
121, 1, 122 | tgpconncompeqg 22865 |
. . . . . . . . . . . 12
⊢
(((oppg‘𝐺) ∈ TopGrp ∧
((invg‘𝐺)‘𝑦) ∈ 𝑋) → [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) = ∪
{𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
124 | 118, 106,
123 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) = ∪
{𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
125 | 116, 124 | eqtr4d 2776 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆)) |
126 | 125 | eleq2d 2818 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑧 ∈ [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ 𝑧 ∈ [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆))) |
127 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
128 | | fvex 6689 |
. . . . . . . . . 10
⊢
((invg‘𝐺)‘𝑦) ∈ V |
129 | 127, 128 | elec 8366 |
. . . . . . . . 9
⊢ (𝑧 ∈
[((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ ((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧) |
130 | 127, 128 | elec 8366 |
. . . . . . . . 9
⊢ (𝑧 ∈
[((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) ↔
((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧) |
131 | 126, 129,
130 | 3bitr3g 316 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ ((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧)) |
132 | 114, 131 | mpbid 235 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧) |
133 | | eqid 2738 |
. . . . . . . . 9
⊢
(invg‘(oppg‘𝐺)) =
(invg‘(oppg‘𝐺)) |
134 | 119, 133,
102, 122 | eqgval 18449 |
. . . . . . . 8
⊢
(((oppg‘𝐺) ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆))) |
135 | 118, 5, 134 | sylancl 589 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆))) |
136 | 132, 135 | mpbid 235 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆)) |
137 | 136 | simp3d 1145 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆) |
138 | 104, 137 | eqeltrrd 2834 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆) |
139 | 138 | expr 460 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆)) |
140 | 139 | ralrimivva 3103 |
. 2
⊢ (𝐺 ∈ TopGrp →
∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆)) |
141 | 8, 45 | isnsg2 18428 |
. 2
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆))) |
142 | 91, 140, 141 | sylanbrc 586 |
1
⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺)) |