Metamath Proof Explorer

Theorem tgpconncomp

Description: The identity component, the connected component containing the identity element, is a closed ( conncompcld ) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypotheses tgpconncomp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
tgpconncomp.z ⊢ 0 = ( 0g ‘ 𝐺 )
tgpconncomp.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tgpconncomp.s ⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
Assertion tgpconncomp ( 𝐺 ∈ TopGrp → 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 tgpconncomp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 tgpconncomp.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 tgpconncomp.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
4 tgpconncomp.s ⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
5 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝒫 𝑋
6 sspwuni ⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝒫 𝑋 ↔ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝑋 )
7 5 6 mpbi ⊢ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝑋
8 4 7 eqsstri ⊢ 𝑆 ⊆ 𝑋
9 8 a1i ⊢ ( 𝐺 ∈ TopGrp → 𝑆 ⊆ 𝑋 )
10 3 1 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
12 1 2 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝑋 )
13 11 12 syl ⊢ ( 𝐺 ∈ TopGrp → 0 ∈ 𝑋 )
14 4 conncompid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 0 ∈ 𝑋 ) → 0 ∈ 𝑆 )
15 10 13 14 syl2anc ⊢ ( 𝐺 ∈ TopGrp → 0 ∈ 𝑆 )
16 15 ne0d ⊢ ( 𝐺 ∈ TopGrp → 𝑆 ≠ ∅ )
17 df-ima ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) = ran ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ↾ 𝑆 )
18 resmpt ⊢ ( 𝑆 ⊆ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ↾ 𝑆 ) = ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) )
19 8 18 ax-mp ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ↾ 𝑆 ) = ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) )
20 19 rneqi ⊢ ran ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ↾ 𝑆 ) = ran ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) )
21 17 20 eqtri ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) = ran ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) )
22 imassrn ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ⊆ ran ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) )
23 11 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → 𝐺 ∈ Grp )
24 23 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝐺 ∈ Grp )
25 9 sselda ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑋 )
26 25 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
27 simpr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
28 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
29 1 28 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
30 24 26 27 29 syl3anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
31 30 fmpttd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 ⟶ 𝑋 )
32 31 frnd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ran ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ⊆ 𝑋 )
33 22 32 sstrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ⊆ 𝑋 )
34 1 2 28 grpsubid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) = 0 )
35 23 25 34 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) = 0 )
36 simpr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
37 ovex ⊢ ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ∈ V
38 eqid ⊢ ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) )
39 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) )
40 38 39 elrnmpt1s ⊢ ( ( 𝑦 ∈ 𝑆 ∧ ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ∈ V ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ran ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) )
41 36 37 40 sylancl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ran ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) )
42 35 41 eqeltrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → 0 ∈ ran ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) )
43 42 21 eleqtrrdi ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → 0 ∈ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) )
44 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
45 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
46 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
47 1 45 46 28 grpsubval ⊢ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
48 25 47 sylan ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
49 48 mpteq2dva ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) )
50 1 46 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
51 23 50 sylan ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
52 1 46 grpinvf ⊢ ( 𝐺 ∈ Grp → ( invg ‘ 𝐺 ) : 𝑋 ⟶ 𝑋 )
53 11 52 syl ⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) : 𝑋 ⟶ 𝑋 )
54 53 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( invg ‘ 𝐺 ) : 𝑋 ⟶ 𝑋 )
55 54 feqmptd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( invg ‘ 𝐺 ) = ( 𝑧 ∈ 𝑋 ↦ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
56 eqidd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) )
57 oveq2 ⊢ ( 𝑤 = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) = ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
58 51 55 56 57 fmptco ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) ∘ ( invg ‘ 𝐺 ) ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ) )
59 49 58 eqtr4d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) ∘ ( invg ‘ 𝐺 ) ) )
60 3 46 grpinvhmeo ⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) ∈ ( 𝐽 Homeo 𝐽 ) )
61 60 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( invg ‘ 𝐺 ) ∈ ( 𝐽 Homeo 𝐽 ) )
62 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) )
63 62 1 45 3 tgplacthmeo ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑋 ) → ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
64 25 63 syldan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
65 hmeoco ⊢ ( ( ( invg ‘ 𝐺 ) ∈ ( 𝐽 Homeo 𝐽 ) ∧ ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) ∈ ( 𝐽 Homeo 𝐽 ) ) → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) ∘ ( invg ‘ 𝐺 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
66 61 64 65 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑤 ) ) ∘ ( invg ‘ 𝐺 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
67 59 66 eqeltrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
68 hmeocn ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Homeo 𝐽 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
69 67 68 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
70 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
71 10 70 syl ⊢ ( 𝐺 ∈ TopGrp → 𝑋 = ∪ 𝐽 )
72 71 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → 𝑋 = ∪ 𝐽 )
73 8 72 sseqtrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → 𝑆 ⊆ ∪ 𝐽 )
74 4 conncompconn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 0 ∈ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn )
75 10 13 74 syl2anc ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ↾t 𝑆 ) ∈ Conn )
76 75 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn )
77 44 69 73 76 connima ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝐽 ↾t ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ) ∈ Conn )
78 4 conncompss ⊢ ( ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ⊆ 𝑋 ∧ 0 ∈ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ∧ ( 𝐽 ↾t ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ) ∈ Conn ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ⊆ 𝑆 )
79 33 43 77 78 syl3anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ⊆ 𝑆 )
80 21 79 eqsstrrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ran ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ⊆ 𝑆 )
81 ovex ⊢ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ∈ V
82 81 38 fnmpti ⊢ ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) Fn 𝑆
83 df-f ⊢ ( ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) : 𝑆 ⟶ 𝑆 ↔ ( ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) Fn 𝑆 ∧ ran ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ⊆ 𝑆 ) )
84 82 83 mpbiran ⊢ ( ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) : 𝑆 ⟶ 𝑆 ↔ ran ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) ⊆ 𝑆 )
85 80 84 sylibr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) : 𝑆 ⟶ 𝑆 )
86 38 fmpt ⊢ ( ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 ∈ 𝑆 ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ) : 𝑆 ⟶ 𝑆 )
87 85 86 sylibr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
88 87 ralrimiva ⊢ ( 𝐺 ∈ TopGrp → ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
89 1 28 issubg4 ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) )
90 11 89 syl ⊢ ( 𝐺 ∈ TopGrp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) )
91 9 16 88 90 mpbir3and ⊢ ( 𝐺 ∈ TopGrp → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
92 11 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → 𝐺 ∈ Grp )
93 eqid ⊢ ( oppg ‘ 𝐺 ) = ( oppg ‘ 𝐺 )
94 93 46 oppginv ⊢ ( 𝐺 ∈ Grp → ( invg ‘ 𝐺 ) = ( invg ‘ ( oppg ‘ 𝐺 ) ) )
95 92 94 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( invg ‘ 𝐺 ) = ( invg ‘ ( oppg ‘ 𝐺 ) ) )
96 95 fveq1d ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( invg ‘ ( oppg ‘ 𝐺 ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
97 simprll ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → 𝑦 ∈ 𝑋 )
98 1 46 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = 𝑦 )
99 92 97 98 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = 𝑦 )
100 96 99 eqtr3d ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( invg ‘ ( oppg ‘ 𝐺 ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = 𝑦 )
101 100 oveq1d ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ ( oppg ‘ 𝐺 ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑧 ) = ( 𝑦 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑧 ) )
102 eqid ⊢ ( +g ‘ ( oppg ‘ 𝐺 ) ) = ( +g ‘ ( oppg ‘ 𝐺 ) )
103 45 93 102 oppgplus ⊢ ( 𝑦 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 )
104 101 103 eqtrdi ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ ( oppg ‘ 𝐺 ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) )
105 1 46 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 )
106 92 97 105 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 )
107 simprlr ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → 𝑧 ∈ 𝑋 )
108 99 oveq1d ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
109 simprr ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
110 108 109 eqeltrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
111 eqid ⊢ ( 𝐺 ~QG 𝑆 ) = ( 𝐺 ~QG 𝑆 )
112 1 46 45 111 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( 𝐺 ~QG 𝑆 ) 𝑧 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) )
113 92 8 112 sylancl ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( 𝐺 ~QG 𝑆 ) 𝑧 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) )
114 106 107 110 113 mpbir3and ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( 𝐺 ~QG 𝑆 ) 𝑧 )
115 1 2 3 4 111 tgpconncompeqg ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ) → [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( 𝐺 ~QG 𝑆 ) = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
116 106 115 syldan ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( 𝐺 ~QG 𝑆 ) = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
117 93 oppgtgp ⊢ ( 𝐺 ∈ TopGrp → ( oppg ‘ 𝐺 ) ∈ TopGrp )
118 117 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( oppg ‘ 𝐺 ) ∈ TopGrp )
119 93 1 oppgbas ⊢ 𝑋 = ( Base ‘ ( oppg ‘ 𝐺 ) )
120 93 2 oppgid ⊢ 0 = ( 0g ‘ ( oppg ‘ 𝐺 ) )
121 93 3 oppgtopn ⊢ 𝐽 = ( TopOpen ‘ ( oppg ‘ 𝐺 ) )
122 eqid ⊢ ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) = ( ( oppg ‘ 𝐺 ) ~QG 𝑆 )
123 119 120 121 4 122 tgpconncompeqg ⊢ ( ( ( oppg ‘ 𝐺 ) ∈ TopGrp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ) → [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
124 118 106 123 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
125 116 124 eqtr4d ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( 𝐺 ~QG 𝑆 ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) )
126 125 eleq2d ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( 𝑧 ∈ [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( 𝐺 ~QG 𝑆 ) ↔ 𝑧 ∈ [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) ) )
127 vex ⊢ 𝑧 ∈ V
128 fvex ⊢ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ V
129 127 128 elec ⊢ ( 𝑧 ∈ [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( 𝐺 ~QG 𝑆 ) ↔ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( 𝐺 ~QG 𝑆 ) 𝑧 )
130 127 128 elec ⊢ ( 𝑧 ∈ [ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ] ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) ↔ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) 𝑧 )
131 126 129 130 3bitr3g ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( 𝐺 ~QG 𝑆 ) 𝑧 ↔ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) 𝑧 ) )
132 114 131 mpbid ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) 𝑧 )
133 eqid ⊢ ( invg ‘ ( oppg ‘ 𝐺 ) ) = ( invg ‘ ( oppg ‘ 𝐺 ) )
134 119 133 102 122 eqgval ⊢ ( ( ( oppg ‘ 𝐺 ) ∈ TopGrp ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) 𝑧 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ ( oppg ‘ 𝐺 ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑧 ) ∈ 𝑆 ) ) )
135 118 8 134 sylancl ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ( ( oppg ‘ 𝐺 ) ~QG 𝑆 ) 𝑧 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ ( oppg ‘ 𝐺 ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑧 ) ∈ 𝑆 ) ) )
136 132 135 mpbid ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ ( oppg ‘ 𝐺 ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑧 ) ∈ 𝑆 ) )
137 136 simp3d ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ ( oppg ‘ 𝐺 ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑧 ) ∈ 𝑆 )
138 104 137 eqeltrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) → ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
139 138 expr ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 → ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) )
140 139 ralrimivva ⊢ ( 𝐺 ∈ TopGrp → ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 → ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) )
141 1 45 isnsg2 ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 → ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ) )
142 91 140 141 sylanbrc ⊢ ( 𝐺 ∈ TopGrp → 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) )