Step | Hyp | Ref
| Expression |
1 | | tgpconcomp.s |
. . . . 5
⊢ 𝑆 = ∪
{𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} |
2 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ 𝒫 𝑋 |
3 | | sspwuni 4547 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ 𝑋) |
4 | 2, 3 | mpbi 219 |
. . . . 5
⊢ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ 𝑋 |
5 | 1, 4 | eqsstri 3598 |
. . . 4
⊢ 𝑆 ⊆ 𝑋 |
6 | 5 | a1i 11 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝑆 ⊆ 𝑋) |
7 | | tgpconcomp.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
8 | | tgpconcomp.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
9 | 7, 8 | tgptopon 21696 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
10 | | tgpgrp 21692 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
11 | | tgpconcomp.z |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
12 | 8, 11 | grpidcl 17273 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
13 | 10, 12 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 0 ∈ 𝑋) |
14 | 1 | concompid 21044 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆) |
15 | 9, 13, 14 | syl2anc 691 |
. . . 4
⊢ (𝐺 ∈ TopGrp → 0 ∈ 𝑆) |
16 | | ne0i 3880 |
. . . 4
⊢ ( 0 ∈ 𝑆 → 𝑆 ≠ ∅) |
17 | 15, 16 | syl 17 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝑆 ≠ ∅) |
18 | | df-ima 5051 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) = ran ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) |
19 | | resmpt 5369 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
20 | 5, 19 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
21 | 20 | rneqi 5273 |
. . . . . . . 8
⊢ ran
((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
22 | 18, 21 | eqtri 2632 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) = ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
23 | | imassrn 5396 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) |
24 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝐺 ∈ Grp) |
25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝐺 ∈ Grp) |
26 | 6 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑋) |
27 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
28 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
29 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(-g‘𝐺) = (-g‘𝐺) |
30 | 8, 29 | grpsubcl 17318 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) ∈ 𝑋) |
31 | 25, 27, 28, 30 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) ∈ 𝑋) |
32 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) |
33 | 31, 32 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)):𝑋⟶𝑋) |
34 | | frn 5966 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)):𝑋⟶𝑋 → ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑋) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑋) |
36 | 23, 35 | syl5ss 3579 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑋) |
37 | 8, 11, 29 | grpsubid 17322 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑦) = 0 ) |
38 | 24, 26, 37 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑦(-g‘𝐺)𝑦) = 0 ) |
39 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
40 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑦(-g‘𝐺)𝑦) ∈ V |
41 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
42 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑦(-g‘𝐺)𝑧) = (𝑦(-g‘𝐺)𝑦)) |
43 | 41, 42 | elrnmpt1s 5294 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑆 ∧ (𝑦(-g‘𝐺)𝑦) ∈ V) → (𝑦(-g‘𝐺)𝑦) ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
44 | 39, 40, 43 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑦(-g‘𝐺)𝑦) ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
45 | 38, 44 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 0 ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
46 | 45, 22 | syl6eleqr 2699 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 0 ∈ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) |
47 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
48 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝐺) = (+g‘𝐺) |
49 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(invg‘𝐺) = (invg‘𝐺) |
50 | 8, 48, 49, 29 | grpsubval 17288 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
51 | 26, 50 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
52 | 51 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧)))) |
53 | 8, 49 | grpinvcl 17290 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
54 | 24, 53 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
55 | 8, 49 | grpinvf 17289 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):𝑋⟶𝑋) |
56 | 10, 55 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺):𝑋⟶𝑋) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺):𝑋⟶𝑋) |
58 | 57 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺) = (𝑧 ∈ 𝑋 ↦ ((invg‘𝐺)‘𝑧))) |
59 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤))) |
60 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((invg‘𝐺)‘𝑧) → (𝑦(+g‘𝐺)𝑤) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
61 | 54, 58, 59, 60 | fmptco 6303 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧)))) |
62 | 52, 61 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺))) |
63 | 7, 49 | grpinvhmeo 21700 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ (𝐽Homeo𝐽)) |
64 | 63 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺) ∈ (𝐽Homeo𝐽)) |
65 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) |
66 | 65, 8, 48, 7 | tgplacthmeo 21717 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑋) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) |
67 | 26, 66 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) |
68 | | hmeoco 21385 |
. . . . . . . . . . . 12
⊢
(((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
69 | 64, 67, 68 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
70 | 62, 69 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽)) |
71 | | hmeocn 21373 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
73 | | toponuni 20542 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
74 | 9, 73 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝑋 = ∪
𝐽) |
75 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑋 = ∪ 𝐽) |
76 | 5, 75 | syl5sseq 3616 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝐽) |
77 | 1 | concompcon 21045 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Con) |
78 | 9, 13, 77 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝐺 ∈ TopGrp → (𝐽 ↾t 𝑆) ∈ Con) |
79 | 78 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝐽 ↾t 𝑆) ∈ Con) |
80 | 47, 72, 76, 79 | conima 21038 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) ∈ Con) |
81 | 1 | concompss 21046 |
. . . . . . . 8
⊢ ((((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑋 ∧ 0 ∈ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ∧ (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) ∈ Con) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑆) |
82 | 36, 46, 80, 81 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑆) |
83 | 22, 82 | syl5eqssr 3613 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆) |
84 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑦(-g‘𝐺)𝑧) ∈ V |
85 | 84, 41 | fnmpti 5935 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) Fn 𝑆 |
86 | | df-f 5808 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆 ↔ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) Fn 𝑆 ∧ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆)) |
87 | 85, 86 | mpbiran 955 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆 ↔ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆) |
88 | 83, 87 | sylibr 223 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆) |
89 | 41 | fmpt 6289 |
. . . . 5
⊢
(∀𝑧 ∈
𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆 ↔ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆) |
90 | 88, 89 | sylibr 223 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆) |
91 | 90 | ralrimiva 2949 |
. . 3
⊢ (𝐺 ∈ TopGrp →
∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆) |
92 | 8, 29 | issubg4 17436 |
. . . 4
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆))) |
93 | 10, 92 | syl 17 |
. . 3
⊢ (𝐺 ∈ TopGrp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆))) |
94 | 6, 17, 91, 93 | mpbir3and 1238 |
. 2
⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (SubGrp‘𝐺)) |
95 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝐺 ∈ Grp) |
96 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(oppg‘𝐺) = (oppg‘𝐺) |
97 | 96, 49 | oppginv 17612 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
(invg‘𝐺) =
(invg‘(oppg‘𝐺))) |
98 | 95, 97 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (invg‘𝐺) =
(invg‘(oppg‘𝐺))) |
99 | 98 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) =
((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))) |
100 | | simprll 798 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝑦 ∈ 𝑋) |
101 | 8, 49 | grpinvinv 17305 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) = 𝑦) |
102 | 95, 100, 101 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) = 𝑦) |
103 | 99, 102 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦)) = 𝑦) |
104 | 103 | oveq1d 6564 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) = (𝑦(+g‘(oppg‘𝐺))𝑧)) |
105 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘(oppg‘𝐺)) =
(+g‘(oppg‘𝐺)) |
106 | 48, 96, 105 | oppgplus 17602 |
. . . . . 6
⊢ (𝑦(+g‘(oppg‘𝐺))𝑧) = (𝑧(+g‘𝐺)𝑦) |
107 | 104, 106 | syl6eq 2660 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) = (𝑧(+g‘𝐺)𝑦)) |
108 | 8, 49 | grpinvcl 17290 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
109 | 95, 100, 108 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
110 | | simprlr 799 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝑧 ∈ 𝑋) |
111 | 102 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = (𝑦(+g‘𝐺)𝑧)) |
112 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝑆) |
113 | 111, 112 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆) |
114 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐺 ~QG 𝑆) = (𝐺 ~QG 𝑆) |
115 | 8, 49, 48, 114 | eqgval 17466 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆))) |
116 | 95, 5, 115 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆))) |
117 | 109, 110,
113, 116 | mpbir3and 1238 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧) |
118 | 8, 11, 7, 1, 114 | tgpconcompeqg 21725 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧
((invg‘𝐺)‘𝑦) ∈ 𝑋) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = ∪ {𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}) |
119 | 109, 118 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = ∪ {𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}) |
120 | 96 | oppgtgp 21712 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp →
(oppg‘𝐺) ∈ TopGrp) |
121 | 120 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(oppg‘𝐺) ∈ TopGrp) |
122 | 96, 8 | oppgbas 17604 |
. . . . . . . . . . . . 13
⊢ 𝑋 =
(Base‘(oppg‘𝐺)) |
123 | 96, 11 | oppgid 17609 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘(oppg‘𝐺)) |
124 | 96, 7 | oppgtopn 17606 |
. . . . . . . . . . . . 13
⊢ 𝐽 =
(TopOpen‘(oppg‘𝐺)) |
125 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
((oppg‘𝐺) ~QG 𝑆) = ((oppg‘𝐺) ~QG 𝑆) |
126 | 122, 123,
124, 1, 125 | tgpconcompeqg 21725 |
. . . . . . . . . . . 12
⊢
(((oppg‘𝐺) ∈ TopGrp ∧
((invg‘𝐺)‘𝑦) ∈ 𝑋) → [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) = ∪
{𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}) |
127 | 121, 109,
126 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) = ∪
{𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}) |
128 | 119, 127 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆)) |
129 | 128 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑧 ∈ [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ 𝑧 ∈ [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆))) |
130 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
131 | | fvex 6113 |
. . . . . . . . . 10
⊢
((invg‘𝐺)‘𝑦) ∈ V |
132 | 130, 131 | elec 7673 |
. . . . . . . . 9
⊢ (𝑧 ∈
[((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ ((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧) |
133 | 130, 131 | elec 7673 |
. . . . . . . . 9
⊢ (𝑧 ∈
[((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆) ↔
((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧) |
134 | 129, 132,
133 | 3bitr3g 301 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ ((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧)) |
135 | 117, 134 | mpbid 221 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧) |
136 | | eqid 2610 |
. . . . . . . . 9
⊢
(invg‘(oppg‘𝐺)) =
(invg‘(oppg‘𝐺)) |
137 | 122, 136,
105, 125 | eqgval 17466 |
. . . . . . . 8
⊢
(((oppg‘𝐺) ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆))) |
138 | 121, 5, 137 | sylancl 693 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧 ↔ (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆))) |
139 | 135, 138 | mpbid 221 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆)) |
140 | 139 | simp3d 1068 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) ∈ 𝑆) |
141 | 107, 140 | eqeltrrd 2689 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆) |
142 | 141 | expr 641 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆)) |
143 | 142 | ralrimivva 2954 |
. 2
⊢ (𝐺 ∈ TopGrp →
∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆)) |
144 | 8, 48 | isnsg2 17447 |
. 2
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆))) |
145 | 94, 143, 144 | sylanbrc 695 |
1
⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺)) |