| Step | Hyp | Ref
| Expression |
| 1 | | tgpconncomp.s |
. . . . 5
⊢ 𝑆 = ∪
{𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} |
| 2 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 |
| 3 | | sspwuni 5100 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋) |
| 4 | 2, 3 | mpbi 230 |
. . . . 5
⊢ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋 |
| 5 | 1, 4 | eqsstri 4030 |
. . . 4
⊢ 𝑆 ⊆ 𝑋 |
| 6 | 5 | a1i 11 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝑆 ⊆ 𝑋) |
| 7 | | tgpconncomp.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
| 8 | | tgpconncomp.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
| 9 | 7, 8 | tgptopon 24090 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
| 10 | | tgpgrp 24086 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
| 11 | | tgpconncomp.z |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
| 12 | 8, 11 | grpidcl 18983 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
| 13 | 10, 12 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 0 ∈ 𝑋) |
| 14 | 1 | conncompid 23439 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆) |
| 15 | 9, 13, 14 | syl2anc 584 |
. . . 4
⊢ (𝐺 ∈ TopGrp → 0 ∈ 𝑆) |
| 16 | 15 | ne0d 4342 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝑆 ≠ ∅) |
| 17 | | df-ima 5698 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) = ran ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) |
| 18 | | resmpt 6055 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
| 19 | 5, 18 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
| 20 | 19 | rneqi 5948 |
. . . . . . . 8
⊢ ran
((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ↾ 𝑆) = ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
| 21 | 17, 20 | eqtri 2765 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) = ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
| 22 | | imassrn 6089 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) |
| 23 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝐺 ∈ Grp) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝐺 ∈ Grp) |
| 25 | 6 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑋) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
| 27 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(-g‘𝐺) = (-g‘𝐺) |
| 29 | 8, 28 | grpsubcl 19038 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) ∈ 𝑋) |
| 30 | 24, 26, 27, 29 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) ∈ 𝑋) |
| 31 | 30 | fmpttd 7135 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)):𝑋⟶𝑋) |
| 32 | 31 | frnd 6744 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ran (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑋) |
| 33 | 22, 32 | sstrid 3995 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑋) |
| 34 | 8, 11, 28 | grpsubid 19042 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑦) = 0 ) |
| 35 | 23, 25, 34 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑦(-g‘𝐺)𝑦) = 0 ) |
| 36 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
| 37 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑦(-g‘𝐺)𝑦) ∈ V |
| 38 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) |
| 39 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑦(-g‘𝐺)𝑧) = (𝑦(-g‘𝐺)𝑦)) |
| 40 | 38, 39 | elrnmpt1s 5970 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑆 ∧ (𝑦(-g‘𝐺)𝑦) ∈ V) → (𝑦(-g‘𝐺)𝑦) ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
| 41 | 36, 37, 40 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑦(-g‘𝐺)𝑦) ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
| 42 | 35, 41 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 0 ∈ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧))) |
| 43 | 42, 21 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 0 ∈ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) |
| 44 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 45 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 46 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 47 | 8, 45, 46, 28 | grpsubval 19003 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
| 48 | 25, 47 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦(-g‘𝐺)𝑧) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
| 49 | 48 | mpteq2dva 5242 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧)))) |
| 50 | 8, 46 | grpinvcl 19005 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
| 51 | 23, 50 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
| 52 | 8, 46 | grpinvf 19004 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):𝑋⟶𝑋) |
| 53 | 10, 52 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺):𝑋⟶𝑋) |
| 54 | 53 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺):𝑋⟶𝑋) |
| 55 | 54 | feqmptd 6977 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺) = (𝑧 ∈ 𝑋 ↦ ((invg‘𝐺)‘𝑧))) |
| 56 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤))) |
| 57 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((invg‘𝐺)‘𝑧) → (𝑦(+g‘𝐺)𝑤) = (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧))) |
| 58 | 51, 55, 56, 57 | fmptco 7149 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑧)))) |
| 59 | 49, 58 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) = ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺))) |
| 60 | 7, 46 | grpinvhmeo 24094 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ (𝐽Homeo𝐽)) |
| 61 | 60 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (invg‘𝐺) ∈ (𝐽Homeo𝐽)) |
| 62 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) |
| 63 | 62, 8, 45, 7 | tgplacthmeo 24111 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑋) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) |
| 64 | 25, 63 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) |
| 65 | | hmeoco 23780 |
. . . . . . . . . . . 12
⊢
(((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
| 66 | 61, 64, 65 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑤 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑤)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
| 67 | 59, 66 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽)) |
| 68 | | hmeocn 23768 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
| 69 | 67, 68 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
| 70 | | toponuni 22920 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 71 | 9, 70 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → 𝑋 = ∪
𝐽) |
| 72 | 71 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑋 = ∪ 𝐽) |
| 73 | 5, 72 | sseqtrid 4026 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝐽) |
| 74 | 1 | conncompconn 23440 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn) |
| 75 | 9, 13, 74 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝐺 ∈ TopGrp → (𝐽 ↾t 𝑆) ∈ Conn) |
| 76 | 75 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝐽 ↾t 𝑆) ∈ Conn) |
| 77 | 44, 69, 73, 76 | connima 23433 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn) |
| 78 | 1 | conncompss 23441 |
. . . . . . . 8
⊢ ((((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑋 ∧ 0 ∈ ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ∧ (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑆) |
| 79 | 33, 43, 77, 78 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ((𝑧 ∈ 𝑋 ↦ (𝑦(-g‘𝐺)𝑧)) “ 𝑆) ⊆ 𝑆) |
| 80 | 21, 79 | eqsstrrid 4023 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆) |
| 81 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑦(-g‘𝐺)𝑧) ∈ V |
| 82 | 81, 38 | fnmpti 6711 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) Fn 𝑆 |
| 83 | | df-f 6565 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆 ↔ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) Fn 𝑆 ∧ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆)) |
| 84 | 82, 83 | mpbiran 709 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆 ↔ ran (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)) ⊆ 𝑆) |
| 85 | 80, 84 | sylibr 234 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆) |
| 86 | 38 | fmpt 7130 |
. . . . 5
⊢
(∀𝑧 ∈
𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆 ↔ (𝑧 ∈ 𝑆 ↦ (𝑦(-g‘𝐺)𝑧)):𝑆⟶𝑆) |
| 87 | 85, 86 | sylibr 234 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆) → ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆) |
| 88 | 87 | ralrimiva 3146 |
. . 3
⊢ (𝐺 ∈ TopGrp →
∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 (𝑦(-g‘𝐺)𝑧) ∈ 𝑆) |
| 89 | 8, 28 | issubg4 19163 |
. . . 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 480 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝐺 ∈ Grp) |
| 93 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(oppg‘𝐺) = (oppg‘𝐺) |
| 94 | 93, 46 | oppginv 19378 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
(invg‘𝐺) =
(invg‘(oppg‘𝐺))) |
| 95 | 92, 94 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (invg‘𝐺) =
(invg‘(oppg‘𝐺))) |
| 96 | 95 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) =
((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))) |
| 97 | | simprll 779 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝑦 ∈ 𝑋) |
| 98 | 8, 46 | grpinvinv 19023 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) = 𝑦) |
| 99 | 92, 97, 98 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑦)) = 𝑦) |
| 100 | 96, 99 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦)) = 𝑦) |
| 101 | 100 | oveq1d 7446 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) = (𝑦(+g‘(oppg‘𝐺))𝑧)) |
| 102 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘(oppg‘𝐺)) =
(+g‘(oppg‘𝐺)) |
| 103 | 45, 93, 102 | oppgplus 19367 |
. . . . . 6
⊢ (𝑦(+g‘(oppg‘𝐺))𝑧) = (𝑧(+g‘𝐺)𝑦) |
| 104 | 101, 103 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(((invg‘(oppg‘𝐺))‘((invg‘𝐺)‘𝑦))(+g‘(oppg‘𝐺))𝑧) = (𝑧(+g‘𝐺)𝑦)) |
| 105 | 8, 46 | grpinvcl 19005 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
| 106 | 92, 97, 105 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
| 107 | | simprlr 780 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → 𝑧 ∈ 𝑋) |
| 108 | 99 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = (𝑦(+g‘𝐺)𝑧)) |
| 109 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝑆) |
| 110 | 108, 109 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (((invg‘𝐺)‘((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) ∈ 𝑆) |
| 111 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐺 ~QG 𝑆) = (𝐺 ~QG 𝑆) |
| 112 | 8, 46, 45, 111 | eqgval 19195 |
. . . . . . . . . 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 1343 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧) |
| 115 | 8, 11, 7, 1, 111 | tgpconncompeqg 24120 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧
((invg‘𝐺)‘𝑦) ∈ 𝑋) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = ∪ {𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
| 116 | 106, 115 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = ∪ {𝑥 ∈ 𝒫 𝑋 ∣
(((invg‘𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) |
| 117 | 93 | oppgtgp 24106 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp →
(oppg‘𝐺) ∈ TopGrp) |
| 118 | 117 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) →
(oppg‘𝐺) ∈ TopGrp) |
| 119 | 93, 8 | oppgbas 19370 |
. . . . . . . . . . . . 13
⊢ 𝑋 =
(Base‘(oppg‘𝐺)) |
| 120 | 93, 11 | oppgid 19375 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘(oppg‘𝐺)) |
| 121 | 93, 7 | oppgtopn 19372 |
. . . . . . . . . . . . 13
⊢ 𝐽 =
(TopOpen‘(oppg‘𝐺)) |
| 122 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
((oppg‘𝐺) ~QG 𝑆) = ((oppg‘𝐺) ~QG 𝑆) |
| 123 | 119, 120,
121, 1, 122 | tgpconncompeqg 24120 |
. . . . . . . . . . . 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 2780 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) = [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆)) |
| 126 | 125 | eleq2d 2827 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑧 ∈ [((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ 𝑧 ∈ [((invg‘𝐺)‘𝑦)]((oppg‘𝐺) ~QG 𝑆))) |
| 127 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
| 128 | | fvex 6919 |
. . . . . . . . . 10
⊢
((invg‘𝐺)‘𝑦) ∈ V |
| 129 | 127, 128 | elec 8791 |
. . . . . . . . 9
⊢ (𝑧 ∈
[((invg‘𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ ((invg‘𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧) |
| 130 | 127, 128 | elec 8791 |
. . . . . . . . 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 232 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → ((invg‘𝐺)‘𝑦)((oppg‘𝐺) ~QG 𝑆)𝑧) |
| 133 | | eqid 2737 |
. . . . . . . . 9
⊢
(invg‘(oppg‘𝐺)) =
(invg‘(oppg‘𝐺)) |
| 134 | 119, 133,
102, 122 | eqgval 19195 |
. . . . . . . 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 232 |
. . . . . 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 2842 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ ((𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑦(+g‘𝐺)𝑧) ∈ 𝑆)) → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆) |
| 139 | 138 | expr 456 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆)) |
| 140 | 139 | ralrimivva 3202 |
. 2
⊢ (𝐺 ∈ TopGrp →
∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆)) |
| 141 | 8, 45 | isnsg2 19174 |
. 2
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 → (𝑧(+g‘𝐺)𝑦) ∈ 𝑆))) |
| 142 | 91, 140, 141 | sylanbrc 583 |
1
⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺)) |