Step | Hyp | Ref
| Expression |
1 | | tgpconncomp.s |
. . . . 5
⊢ 𝑆 = ∪
{𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} |
2 | | ssrab2 4013 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 |
3 | | sspwuni 5029 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋) |
4 | 2, 3 | mpbi 229 |
. . . . 5
⊢ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋 |
5 | 1, 4 | eqsstri 3955 |
. . . 4
⊢ 𝑆 ⊆ 𝑋 |
6 | 5 | a1i 11 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝑆 ⊆ 𝑋) |
7 | | tgpconncomp.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
8 | | tgpconncomp.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
9 | 7, 8 | tgptopon 23233 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
10 | | tgpgrp 23229 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
11 | | tgpconncomp.z |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
12 | 8, 11 | grpidcl 18607 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
13 | 10, 12 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 0 ∈ 𝑋) |
14 | 1 | conncompid 22582 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆) |
15 | 9, 13, 14 | syl2anc 584 |
. . . 4
⊢ (𝐺 ∈ TopGrp → 0 ∈ 𝑆) |
16 | 15 | ne0d 4269 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝑆 ≠ ∅) |
17 | | df-ima 5602 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) = ran ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) |
18 | | resmpt 5945 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
19 | 5, 18 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
20 | 19 | rneqi 5846 |
. . . . . . . 8
⊢ ran
((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
21 | 17, 20 | eqtri 2766 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) = ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
22 | | imassrn 5980 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) |
23 | 10 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝐺 ∈ Grp) |
24 | 23 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝐺 ∈ Grp) |
25 | 6 | sselda 3921 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑋) |
26 | 25 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
27 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
28 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(-g‘𝐺) = (-g‘𝐺) |
29 | 8, 28 | grpsubcl 18655 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) ∈ 𝑋) |
30 | 24, 26, 27, 29 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) ∈ 𝑋) |
31 | 30 | fmpttd 6989 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)):𝑋⟶𝑋) |
32 | 31 | frnd 6608 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑋) |
33 | 22, 32 | sstrid 3932 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑋) |
34 | 8, 11, 28 | grpsubid 18659 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑦) = 0 ) |
35 | 23, 25, 34 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑦(-g‘𝐺)𝑦) = 0 ) |
36 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
37 | | ovex 7308 |
. . . . . . . . . . 11
⊢ (𝑦(-g‘𝐺)𝑦) ∈ V |
38 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
39 | | oveq2 7283 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑦(-g‘𝐺)𝑧) = (𝑦(-g‘𝐺)𝑦)) |
40 | 38, 39 | elrnmpt1s 5866 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑆 ∧ (𝑦(-g‘𝐺)𝑦) ∈ V) → (𝑦(-g‘𝐺)𝑦) ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
41 | 36, 37, 40 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑦(-g‘𝐺)𝑦) ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
42 | 35, 41 | eqeltrrd 2840 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 0 ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
43 | 42, 21 | eleqtrrdi 2850 |
. . . . . . . 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 18625 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
48 | 25, 47 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
49 | 48 | mpteq2dva 5174 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧)))) |
50 | 8, 46 | grpinvcl 18627 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
51 | 23, 50 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
52 | 8, 46 | grpinvf 18626 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):𝑋⟶𝑋) |
53 | 10, 52 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺):𝑋⟶𝑋) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺):𝑋⟶𝑋) |
55 | 54 | feqmptd 6837 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺) = (𝑧 ∈ 𝑋 ↦ ((invg‘𝐺)‘𝑧))) |
56 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤))) |
57 | | oveq2 7283 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((invg‘𝐺)‘𝑧) → (𝑦(+g‘𝐺)𝑤) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
58 | 51, 55, 56, 57 | fmptco 7001 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧)))) |
59 | 49, 58 | eqtr4d 2781 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺))) |
60 | 7, 46 | grpinvhmeo 23237 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ (𝐽Homeo𝐽)) |
61 | 60 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺) ∈ (𝐽Homeo𝐽)) |
62 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) |
63 | 62, 8, 45, 7 | tgplacthmeo 23254 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑋) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) |
64 | 25, 63 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) |
65 | | hmeoco 22923 |
. . . . . . . . . . . 12
⊢
(((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
66 | 61, 64, 65 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
67 | 59, 66 | eqeltrd 2839 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽)) |
68 | | hmeocn 22911 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
69 | 67, 68 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
70 | | toponuni 22063 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
71 | 9, 70 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝑋 = ∪
𝐽) |
72 | 71 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑋 = ∪ 𝐽) |
73 | 5, 72 | sseqtrid 3973 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝐽) |
74 | 1 | conncompconn 22583 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn) |
75 | 9, 13, 74 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝐺 ∈ TopGrp → (𝐽 ↾t 𝑆) ∈ Conn) |
76 | 75 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝐽 ↾t 𝑆) ∈ Conn) |
77 | 44, 69, 73, 76 | connima 22576 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn) |
78 | 1 | conncompss 22584 |
. . . . . . . 8
⊢ ((((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑋 ∧ 0 ∈ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ∧ (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑆) |
79 | 33, 43, 77, 78 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑆) |
80 | 21, 79 | eqsstrrid 3970 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆) |
81 | | ovex 7308 |
. . . . . . . 8
⊢ (𝑦(-g‘𝐺)𝑧) ∈ V |
82 | 81, 38 | fnmpti 6576 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) Fn 𝑆 |
83 | | df-f 6437 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆 ↔ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) Fn 𝑆 ∧ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆)) |
84 | 82, 83 | mpbiran 706 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆 ↔ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆) |
85 | 80, 84 | sylibr 233 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆) |
86 | 38 | fmpt 6984 |
. . . . 5
⊢
(∀𝑧 ∈
𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆 ↔ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆) |
87 | 85, 86 | sylibr 233 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆) |
88 | 87 | ralrimiva 3103 |
. . 3
⊢ (𝐺 ∈ TopGrp →
∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆) |
89 | 8, 28 | issubg4 18774 |
. . . 4
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆))) |
90 | 10, 89 | syl 17 |
. . 3
⊢ (𝐺 ∈ TopGrp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆))) |
91 | 6, 16, 88, 90 | mpbir3and 1341 |
. 2
⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (SubGrp‘𝐺)) |
92 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝐺 ∈ Grp) |
93 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(oppg‘𝐺) = (oppg‘𝐺) |
94 | 93, 46 | oppginv 18966 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
(invg‘𝐺) =
(invg‘(oppg‘𝐺))) |
95 | 92, 94 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (invg‘𝐺) =
(invg‘(oppg‘𝐺))) |
96 | 95 | fveq1d 6776 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) =
((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))) |
97 | | simprll 776 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝑦 ∈ 𝑋) |
98 | 8, 46 | grpinvinv 18642 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) = 𝑦) |
99 | 92, 97, 98 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) = 𝑦) |
100 | 96, 99 | eqtr3d 2780 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦)) = 𝑦) |
101 | 100 | oveq1d 7290 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) = (𝑦(+g‘(oppg‘𝐺))𝑧)) |
102 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘(oppg‘𝐺)) =
(+g‘(oppg‘𝐺)) |
103 | 45, 93, 102 | oppgplus 18953 |
. . . . . 6
⊢ (𝑦(+g‘(oppg‘𝐺))𝑧) = (𝑧(+g‘𝐺)𝑦) |
104 | 101, 103 | eqtrdi 2794 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) = (𝑧(+g‘𝐺)𝑦)) |
105 | 8, 46 | grpinvcl 18627 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
106 | 92, 97, 105 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
107 | | simprlr 777 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝑧 ∈ 𝑋) |
108 | 99 | oveq1d 7290 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = (𝑦(+g‘𝐺)𝑧)) |
109 | | simprr 770 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝑆) |
110 | 108, 109 | eqeltrd 2839 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆) |
111 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝐺 ~QG 𝑆) = (𝐺 ~QG 𝑆) |
112 | 8, 46, 45, 111 | eqgval 18805 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆))) |
113 | 92, 5, 112 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆))) |
114 | 106, 107,
110, 113 | mpbir3and 1341 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧) |
115 | 8, 11, 7, 1, 111 | tgpconncompeqg 23263 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧
((invg‘𝐺)‘𝑦) ∈ 𝑋) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = ∪ {𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
116 | 106, 115 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = ∪ {𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
117 | 93 | oppgtgp 23249 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp →
(oppg‘𝐺) ∈ TopGrp) |
118 | 117 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(oppg‘𝐺) ∈ TopGrp) |
119 | 93, 8 | oppgbas 18956 |
. . . . . . . . . . . . 13
⊢ 𝑋 =
(Base‘(oppg‘𝐺)) |
120 | 93, 11 | oppgid 18963 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘(oppg‘𝐺)) |
121 | 93, 7 | oppgtopn 18960 |
. . . . . . . . . . . . 13
⊢ 𝐽 =
(TopOpen‘(oppg‘𝐺)) |
122 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
((oppg‘𝐺) ~QG 𝑆) = ((oppg‘𝐺) ~QG 𝑆) |
123 | 119, 120,
121, 1, 122 | tgpconncompeqg 23263 |
. . . . . . . . . . . 12
⊢
(((oppg‘𝐺) ∈ TopGrp ∧
((invg‘𝐺)‘𝑦) ∈ 𝑋) → [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) = ∪
{𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
124 | 118, 106,
123 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) = ∪
{𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
125 | 116, 124 | eqtr4d 2781 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆)) |
126 | 125 | eleq2d 2824 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑧 ∈ [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ 𝑧 ∈ [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆))) |
127 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
128 | | fvex 6787 |
. . . . . . . . . 10
⊢
((invg‘𝐺)‘𝑦) ∈ V |
129 | 127, 128 | elec 8542 |
. . . . . . . . 9
⊢ (𝑧 ∈
[((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ ((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧) |
130 | 127, 128 | elec 8542 |
. . . . . . . . 9
⊢ (𝑧 ∈
[((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) ↔
((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧) |
131 | 126, 129,
130 | 3bitr3g 313 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ ((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧)) |
132 | 114, 131 | mpbid 231 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧) |
133 | | eqid 2738 |
. . . . . . . . 9
⊢
(invg‘(oppg‘𝐺)) =
(invg‘(oppg‘𝐺)) |
134 | 119, 133,
102, 122 | eqgval 18805 |
. . . . . . . 8
⊢
(((oppg‘𝐺) ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆))) |
135 | 118, 5, 134 | sylancl 586 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆))) |
136 | 132, 135 | mpbid 231 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆)) |
137 | 136 | simp3d 1143 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆) |
138 | 104, 137 | eqeltrrd 2840 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆) |
139 | 138 | expr 457 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆)) |
140 | 139 | ralrimivva 3123 |
. 2
⊢ (𝐺 ∈ TopGrp →
∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆)) |
141 | 8, 45 | isnsg2 18784 |
. 2
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆))) |
142 | 91, 140, 141 | sylanbrc 583 |
1
⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺)) |