MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgpconncomp Structured version   Visualization version   GIF version

Theorem tgpconncomp 22286
Description: The identity component, the connected component containing the identity element, is a closed (conncompcld 21608) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.)
Hypotheses
Ref Expression
tgpconncomp.x 𝑋 = (Base‘𝐺)
tgpconncomp.z 0 = (0g𝐺)
tgpconncomp.j 𝐽 = (TopOpen‘𝐺)
tgpconncomp.s 𝑆 = {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)}
Assertion
Ref Expression
tgpconncomp (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺))
Distinct variable groups:   𝑥, 0   𝑥,𝐽   𝑥,𝐺   𝑥,𝑋
Allowed substitution hint:   𝑆(𝑥)

Proof of Theorem tgpconncomp
Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tgpconncomp.s . . . . 5 𝑆 = {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)}
2 ssrab2 3912 . . . . . 6 {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋
3 sspwuni 4832 . . . . . 6 ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ 𝑋)
42, 3mpbi 222 . . . . 5 {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ 𝑋
51, 4eqsstri 3860 . . . 4 𝑆𝑋
65a1i 11 . . 3 (𝐺 ∈ TopGrp → 𝑆𝑋)
7 tgpconncomp.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
8 tgpconncomp.x . . . . . 6 𝑋 = (Base‘𝐺)
97, 8tgptopon 22256 . . . . 5 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
10 tgpgrp 22252 . . . . . 6 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
11 tgpconncomp.z . . . . . . 7 0 = (0g𝐺)
128, 11grpidcl 17804 . . . . . 6 (𝐺 ∈ Grp → 0𝑋)
1310, 12syl 17 . . . . 5 (𝐺 ∈ TopGrp → 0𝑋)
141conncompid 21605 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 0𝑋) → 0𝑆)
159, 13, 14syl2anc 579 . . . 4 (𝐺 ∈ TopGrp → 0𝑆)
1615ne0d 4151 . . 3 (𝐺 ∈ TopGrp → 𝑆 ≠ ∅)
17 df-ima 5355 . . . . . . . 8 ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆) = ran ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ↾ 𝑆)
18 resmpt 5686 . . . . . . . . . 10 (𝑆𝑋 → ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ↾ 𝑆) = (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)))
195, 18ax-mp 5 . . . . . . . . 9 ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ↾ 𝑆) = (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧))
2019rneqi 5584 . . . . . . . 8 ran ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ↾ 𝑆) = ran (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧))
2117, 20eqtri 2849 . . . . . . 7 ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆) = ran (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧))
22 imassrn 5718 . . . . . . . . 9 ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆) ⊆ ran (𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧))
2310adantr 474 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → 𝐺 ∈ Grp)
2423adantr 474 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑦𝑆) ∧ 𝑧𝑋) → 𝐺 ∈ Grp)
256sselda 3827 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → 𝑦𝑋)
2625adantr 474 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑦𝑆) ∧ 𝑧𝑋) → 𝑦𝑋)
27 simpr 479 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝑦𝑆) ∧ 𝑧𝑋) → 𝑧𝑋)
28 eqid 2825 . . . . . . . . . . . . 13 (-g𝐺) = (-g𝐺)
298, 28grpsubcl 17849 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑦𝑋𝑧𝑋) → (𝑦(-g𝐺)𝑧) ∈ 𝑋)
3024, 26, 27, 29syl3anc 1494 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝑦𝑆) ∧ 𝑧𝑋) → (𝑦(-g𝐺)𝑧) ∈ 𝑋)
3130fmpttd 6634 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)):𝑋𝑋)
3231frnd 6285 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → ran (𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ⊆ 𝑋)
3322, 32syl5ss 3838 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆) ⊆ 𝑋)
348, 11, 28grpsubid 17853 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑦𝑋) → (𝑦(-g𝐺)𝑦) = 0 )
3523, 25, 34syl2anc 579 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑦(-g𝐺)𝑦) = 0 )
36 simpr 479 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → 𝑦𝑆)
37 ovex 6937 . . . . . . . . . . 11 (𝑦(-g𝐺)𝑦) ∈ V
38 eqid 2825 . . . . . . . . . . . 12 (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)) = (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧))
39 oveq2 6913 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑦(-g𝐺)𝑧) = (𝑦(-g𝐺)𝑦))
4038, 39elrnmpt1s 5606 . . . . . . . . . . 11 ((𝑦𝑆 ∧ (𝑦(-g𝐺)𝑦) ∈ V) → (𝑦(-g𝐺)𝑦) ∈ ran (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)))
4136, 37, 40sylancl 580 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑦(-g𝐺)𝑦) ∈ ran (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)))
4235, 41eqeltrrd 2907 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → 0 ∈ ran (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)))
4342, 21syl6eleqr 2917 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → 0 ∈ ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆))
44 eqid 2825 . . . . . . . . 9 𝐽 = 𝐽
45 eqid 2825 . . . . . . . . . . . . . . 15 (+g𝐺) = (+g𝐺)
46 eqid 2825 . . . . . . . . . . . . . . 15 (invg𝐺) = (invg𝐺)
478, 45, 46, 28grpsubval 17819 . . . . . . . . . . . . . 14 ((𝑦𝑋𝑧𝑋) → (𝑦(-g𝐺)𝑧) = (𝑦(+g𝐺)((invg𝐺)‘𝑧)))
4825, 47sylan 575 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑦𝑆) ∧ 𝑧𝑋) → (𝑦(-g𝐺)𝑧) = (𝑦(+g𝐺)((invg𝐺)‘𝑧)))
4948mpteq2dva 4967 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) = (𝑧𝑋 ↦ (𝑦(+g𝐺)((invg𝐺)‘𝑧))))
508, 46grpinvcl 17821 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → ((invg𝐺)‘𝑧) ∈ 𝑋)
5123, 50sylan 575 . . . . . . . . . . . . 13 (((𝐺 ∈ TopGrp ∧ 𝑦𝑆) ∧ 𝑧𝑋) → ((invg𝐺)‘𝑧) ∈ 𝑋)
528, 46grpinvf 17820 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Grp → (invg𝐺):𝑋𝑋)
5310, 52syl 17 . . . . . . . . . . . . . . 15 (𝐺 ∈ TopGrp → (invg𝐺):𝑋𝑋)
5453adantr 474 . . . . . . . . . . . . . 14 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (invg𝐺):𝑋𝑋)
5554feqmptd 6496 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (invg𝐺) = (𝑧𝑋 ↦ ((invg𝐺)‘𝑧)))
56 eqidd 2826 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) = (𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)))
57 oveq2 6913 . . . . . . . . . . . . 13 (𝑤 = ((invg𝐺)‘𝑧) → (𝑦(+g𝐺)𝑤) = (𝑦(+g𝐺)((invg𝐺)‘𝑧)))
5851, 55, 56, 57fmptco 6646 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → ((𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) ∘ (invg𝐺)) = (𝑧𝑋 ↦ (𝑦(+g𝐺)((invg𝐺)‘𝑧))))
5949, 58eqtr4d 2864 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) = ((𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) ∘ (invg𝐺)))
607, 46grpinvhmeo 22260 . . . . . . . . . . . . 13 (𝐺 ∈ TopGrp → (invg𝐺) ∈ (𝐽Homeo𝐽))
6160adantr 474 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (invg𝐺) ∈ (𝐽Homeo𝐽))
62 eqid 2825 . . . . . . . . . . . . . 14 (𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) = (𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤))
6362, 8, 45, 7tgplacthmeo 22277 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝑦𝑋) → (𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) ∈ (𝐽Homeo𝐽))
6425, 63syldan 585 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) ∈ (𝐽Homeo𝐽))
65 hmeoco 21946 . . . . . . . . . . . 12 (((invg𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) ∈ (𝐽Homeo𝐽)) → ((𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) ∘ (invg𝐺)) ∈ (𝐽Homeo𝐽))
6661, 64, 65syl2anc 579 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → ((𝑤𝑋 ↦ (𝑦(+g𝐺)𝑤)) ∘ (invg𝐺)) ∈ (𝐽Homeo𝐽))
6759, 66eqeltrd 2906 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ∈ (𝐽Homeo𝐽))
68 hmeocn 21934 . . . . . . . . . 10 ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
6967, 68syl 17 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
70 toponuni 21089 . . . . . . . . . . . 12 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
719, 70syl 17 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → 𝑋 = 𝐽)
7271adantr 474 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → 𝑋 = 𝐽)
735, 72syl5sseq 3878 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → 𝑆 𝐽)
741conncompconn 21606 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 0𝑋) → (𝐽t 𝑆) ∈ Conn)
759, 13, 74syl2anc 579 . . . . . . . . . 10 (𝐺 ∈ TopGrp → (𝐽t 𝑆) ∈ Conn)
7675adantr 474 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝐽t 𝑆) ∈ Conn)
7744, 69, 73, 76connima 21599 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝐽t ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆)) ∈ Conn)
781conncompss 21607 . . . . . . . 8 ((((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆) ⊆ 𝑋0 ∈ ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆) ∧ (𝐽t ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆)) ∈ Conn) → ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆) ⊆ 𝑆)
7933, 43, 77, 78syl3anc 1494 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → ((𝑧𝑋 ↦ (𝑦(-g𝐺)𝑧)) “ 𝑆) ⊆ 𝑆)
8021, 79syl5eqssr 3875 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → ran (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)) ⊆ 𝑆)
81 ovex 6937 . . . . . . . 8 (𝑦(-g𝐺)𝑧) ∈ V
8281, 38fnmpti 6255 . . . . . . 7 (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)) Fn 𝑆
83 df-f 6127 . . . . . . 7 ((𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)):𝑆𝑆 ↔ ((𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)) Fn 𝑆 ∧ ran (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)) ⊆ 𝑆))
8482, 83mpbiran 700 . . . . . 6 ((𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)):𝑆𝑆 ↔ ran (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)) ⊆ 𝑆)
8580, 84sylibr 226 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)):𝑆𝑆)
8638fmpt 6629 . . . . 5 (∀𝑧𝑆 (𝑦(-g𝐺)𝑧) ∈ 𝑆 ↔ (𝑧𝑆 ↦ (𝑦(-g𝐺)𝑧)):𝑆𝑆)
8785, 86sylibr 226 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑦𝑆) → ∀𝑧𝑆 (𝑦(-g𝐺)𝑧) ∈ 𝑆)
8887ralrimiva 3175 . . 3 (𝐺 ∈ TopGrp → ∀𝑦𝑆𝑧𝑆 (𝑦(-g𝐺)𝑧) ∈ 𝑆)
898, 28issubg4 17964 . . . 4 (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆𝑋𝑆 ≠ ∅ ∧ ∀𝑦𝑆𝑧𝑆 (𝑦(-g𝐺)𝑧) ∈ 𝑆)))
9010, 89syl 17 . . 3 (𝐺 ∈ TopGrp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆𝑋𝑆 ≠ ∅ ∧ ∀𝑦𝑆𝑧𝑆 (𝑦(-g𝐺)𝑧) ∈ 𝑆)))
916, 16, 88, 90mpbir3and 1446 . 2 (𝐺 ∈ TopGrp → 𝑆 ∈ (SubGrp‘𝐺))
9210adantr 474 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → 𝐺 ∈ Grp)
93 eqid 2825 . . . . . . . . . . 11 (oppg𝐺) = (oppg𝐺)
9493, 46oppginv 18139 . . . . . . . . . 10 (𝐺 ∈ Grp → (invg𝐺) = (invg‘(oppg𝐺)))
9592, 94syl 17 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (invg𝐺) = (invg‘(oppg𝐺)))
9695fveq1d 6435 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → ((invg𝐺)‘((invg𝐺)‘𝑦)) = ((invg‘(oppg𝐺))‘((invg𝐺)‘𝑦)))
97 simprll 797 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → 𝑦𝑋)
988, 46grpinvinv 17836 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ 𝑦𝑋) → ((invg𝐺)‘((invg𝐺)‘𝑦)) = 𝑦)
9992, 97, 98syl2anc 579 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → ((invg𝐺)‘((invg𝐺)‘𝑦)) = 𝑦)
10096, 99eqtr3d 2863 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → ((invg‘(oppg𝐺))‘((invg𝐺)‘𝑦)) = 𝑦)
101100oveq1d 6920 . . . . . 6 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg‘(oppg𝐺))‘((invg𝐺)‘𝑦))(+g‘(oppg𝐺))𝑧) = (𝑦(+g‘(oppg𝐺))𝑧))
102 eqid 2825 . . . . . . 7 (+g‘(oppg𝐺)) = (+g‘(oppg𝐺))
10345, 93, 102oppgplus 18129 . . . . . 6 (𝑦(+g‘(oppg𝐺))𝑧) = (𝑧(+g𝐺)𝑦)
104101, 103syl6eq 2877 . . . . 5 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg‘(oppg𝐺))‘((invg𝐺)‘𝑦))(+g‘(oppg𝐺))𝑧) = (𝑧(+g𝐺)𝑦))
1058, 46grpinvcl 17821 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ 𝑦𝑋) → ((invg𝐺)‘𝑦) ∈ 𝑋)
10692, 97, 105syl2anc 579 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → ((invg𝐺)‘𝑦) ∈ 𝑋)
107 simprlr 798 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → 𝑧𝑋)
10899oveq1d 6920 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg𝐺)‘((invg𝐺)‘𝑦))(+g𝐺)𝑧) = (𝑦(+g𝐺)𝑧))
109 simprr 789 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (𝑦(+g𝐺)𝑧) ∈ 𝑆)
110108, 109eqeltrd 2906 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg𝐺)‘((invg𝐺)‘𝑦))(+g𝐺)𝑧) ∈ 𝑆)
111 eqid 2825 . . . . . . . . . . 11 (𝐺 ~QG 𝑆) = (𝐺 ~QG 𝑆)
1128, 46, 45, 111eqgval 17994 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ 𝑆𝑋) → (((invg𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ (((invg𝐺)‘𝑦) ∈ 𝑋𝑧𝑋 ∧ (((invg𝐺)‘((invg𝐺)‘𝑦))(+g𝐺)𝑧) ∈ 𝑆)))
11392, 5, 112sylancl 580 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ (((invg𝐺)‘𝑦) ∈ 𝑋𝑧𝑋 ∧ (((invg𝐺)‘((invg𝐺)‘𝑦))(+g𝐺)𝑧) ∈ 𝑆)))
114106, 107, 110, 113mpbir3and 1446 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → ((invg𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧)
1158, 11, 7, 1, 111tgpconncompeqg 22285 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ ((invg𝐺)‘𝑦) ∈ 𝑋) → [((invg𝐺)‘𝑦)](𝐺 ~QG 𝑆) = {𝑥 ∈ 𝒫 𝑋 ∣ (((invg𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽t 𝑥) ∈ Conn)})
116106, 115syldan 585 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → [((invg𝐺)‘𝑦)](𝐺 ~QG 𝑆) = {𝑥 ∈ 𝒫 𝑋 ∣ (((invg𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽t 𝑥) ∈ Conn)})
11793oppgtgp 22272 . . . . . . . . . . . . 13 (𝐺 ∈ TopGrp → (oppg𝐺) ∈ TopGrp)
118117adantr 474 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (oppg𝐺) ∈ TopGrp)
11993, 8oppgbas 18131 . . . . . . . . . . . . 13 𝑋 = (Base‘(oppg𝐺))
12093, 11oppgid 18136 . . . . . . . . . . . . 13 0 = (0g‘(oppg𝐺))
12193, 7oppgtopn 18133 . . . . . . . . . . . . 13 𝐽 = (TopOpen‘(oppg𝐺))
122 eqid 2825 . . . . . . . . . . . . 13 ((oppg𝐺) ~QG 𝑆) = ((oppg𝐺) ~QG 𝑆)
123119, 120, 121, 1, 122tgpconncompeqg 22285 . . . . . . . . . . . 12 (((oppg𝐺) ∈ TopGrp ∧ ((invg𝐺)‘𝑦) ∈ 𝑋) → [((invg𝐺)‘𝑦)]((oppg𝐺) ~QG 𝑆) = {𝑥 ∈ 𝒫 𝑋 ∣ (((invg𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽t 𝑥) ∈ Conn)})
124118, 106, 123syl2anc 579 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → [((invg𝐺)‘𝑦)]((oppg𝐺) ~QG 𝑆) = {𝑥 ∈ 𝒫 𝑋 ∣ (((invg𝐺)‘𝑦) ∈ 𝑥 ∧ (𝐽t 𝑥) ∈ Conn)})
125116, 124eqtr4d 2864 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → [((invg𝐺)‘𝑦)](𝐺 ~QG 𝑆) = [((invg𝐺)‘𝑦)]((oppg𝐺) ~QG 𝑆))
126125eleq2d 2892 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (𝑧 ∈ [((invg𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ 𝑧 ∈ [((invg𝐺)‘𝑦)]((oppg𝐺) ~QG 𝑆)))
127 vex 3417 . . . . . . . . . 10 𝑧 ∈ V
128 fvex 6446 . . . . . . . . . 10 ((invg𝐺)‘𝑦) ∈ V
129127, 128elec 8051 . . . . . . . . 9 (𝑧 ∈ [((invg𝐺)‘𝑦)](𝐺 ~QG 𝑆) ↔ ((invg𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧)
130127, 128elec 8051 . . . . . . . . 9 (𝑧 ∈ [((invg𝐺)‘𝑦)]((oppg𝐺) ~QG 𝑆) ↔ ((invg𝐺)‘𝑦)((oppg𝐺) ~QG 𝑆)𝑧)
131126, 129, 1303bitr3g 305 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg𝐺)‘𝑦)(𝐺 ~QG 𝑆)𝑧 ↔ ((invg𝐺)‘𝑦)((oppg𝐺) ~QG 𝑆)𝑧))
132114, 131mpbid 224 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → ((invg𝐺)‘𝑦)((oppg𝐺) ~QG 𝑆)𝑧)
133 eqid 2825 . . . . . . . . 9 (invg‘(oppg𝐺)) = (invg‘(oppg𝐺))
134119, 133, 102, 122eqgval 17994 . . . . . . . 8 (((oppg𝐺) ∈ TopGrp ∧ 𝑆𝑋) → (((invg𝐺)‘𝑦)((oppg𝐺) ~QG 𝑆)𝑧 ↔ (((invg𝐺)‘𝑦) ∈ 𝑋𝑧𝑋 ∧ (((invg‘(oppg𝐺))‘((invg𝐺)‘𝑦))(+g‘(oppg𝐺))𝑧) ∈ 𝑆)))
135118, 5, 134sylancl 580 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg𝐺)‘𝑦)((oppg𝐺) ~QG 𝑆)𝑧 ↔ (((invg𝐺)‘𝑦) ∈ 𝑋𝑧𝑋 ∧ (((invg‘(oppg𝐺))‘((invg𝐺)‘𝑦))(+g‘(oppg𝐺))𝑧) ∈ 𝑆)))
136132, 135mpbid 224 . . . . . 6 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg𝐺)‘𝑦) ∈ 𝑋𝑧𝑋 ∧ (((invg‘(oppg𝐺))‘((invg𝐺)‘𝑦))(+g‘(oppg𝐺))𝑧) ∈ 𝑆))
137136simp3d 1178 . . . . 5 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (((invg‘(oppg𝐺))‘((invg𝐺)‘𝑦))(+g‘(oppg𝐺))𝑧) ∈ 𝑆)
138104, 137eqeltrrd 2907 . . . 4 ((𝐺 ∈ TopGrp ∧ ((𝑦𝑋𝑧𝑋) ∧ (𝑦(+g𝐺)𝑧) ∈ 𝑆)) → (𝑧(+g𝐺)𝑦) ∈ 𝑆)
139138expr 450 . . 3 ((𝐺 ∈ TopGrp ∧ (𝑦𝑋𝑧𝑋)) → ((𝑦(+g𝐺)𝑧) ∈ 𝑆 → (𝑧(+g𝐺)𝑦) ∈ 𝑆))
140139ralrimivva 3180 . 2 (𝐺 ∈ TopGrp → ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧) ∈ 𝑆 → (𝑧(+g𝐺)𝑦) ∈ 𝑆))
1418, 45isnsg2 17975 . 2 (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧) ∈ 𝑆 → (𝑧(+g𝐺)𝑦) ∈ 𝑆)))
14291, 140, 141sylanbrc 578 1 (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1111   = wceq 1656  wcel 2164  wne 2999  wral 3117  {crab 3121  Vcvv 3414  wss 3798  c0 4144  𝒫 cpw 4378   cuni 4658   class class class wbr 4873  cmpt 4952  ran crn 5343  cres 5344  cima 5345  ccom 5346   Fn wfn 6118  wf 6119  cfv 6123  (class class class)co 6905  [cec 8007  Basecbs 16222  +gcplusg 16305  t crest 16434  TopOpenctopn 16435  0gc0g 16453  Grpcgrp 17776  invgcminusg 17777  -gcsg 17778  SubGrpcsubg 17939  NrmSGrpcnsg 17940   ~QG cqg 17941  oppgcoppg 18125  TopOnctopon 21085   Cn ccn 21399  Conncconn 21585  Homeochmeo 21927  TopGrpctgp 22245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-tpos 7617  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-oadd 7830  df-er 8009  df-ec 8011  df-map 8124  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-fi 8586  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420  df-9 11421  df-ndx 16225  df-slot 16226  df-base 16228  df-sets 16229  df-ress 16230  df-plusg 16318  df-tset 16324  df-rest 16436  df-topn 16437  df-0g 16455  df-topgen 16457  df-plusf 17594  df-mgm 17595  df-sgrp 17637  df-mnd 17648  df-grp 17779  df-minusg 17780  df-sbg 17781  df-subg 17942  df-nsg 17943  df-eqg 17944  df-oppg 18126  df-top 21069  df-topon 21086  df-topsp 21108  df-bases 21121  df-cld 21194  df-cn 21402  df-cnp 21403  df-conn 21586  df-tx 21736  df-hmeo 21929  df-tmd 22246  df-tgp 22247
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator