Step | Hyp | Ref
| Expression |
1 | | tgpconncomp.s |
. . . . 5
β’ π = βͺ
{π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} |
2 | | ssrab2 4041 |
. . . . . 6
β’ {π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} β π« π |
3 | | sspwuni 5064 |
. . . . . 6
β’ ({π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} β π« π β βͺ {π₯
β π« π β£
( 0
β π₯ β§ (π½ βΎt π₯) β Conn)} β π) |
4 | 2, 3 | mpbi 229 |
. . . . 5
β’ βͺ {π₯
β π« π β£
( 0
β π₯ β§ (π½ βΎt π₯) β Conn)} β π |
5 | 1, 4 | eqsstri 3982 |
. . . 4
β’ π β π |
6 | 5 | a1i 11 |
. . 3
β’ (πΊ β TopGrp β π β π) |
7 | | tgpconncomp.j |
. . . . . 6
β’ π½ = (TopOpenβπΊ) |
8 | | tgpconncomp.x |
. . . . . 6
β’ π = (BaseβπΊ) |
9 | 7, 8 | tgptopon 23456 |
. . . . 5
β’ (πΊ β TopGrp β π½ β (TopOnβπ)) |
10 | | tgpgrp 23452 |
. . . . . 6
β’ (πΊ β TopGrp β πΊ β Grp) |
11 | | tgpconncomp.z |
. . . . . . 7
β’ 0 =
(0gβπΊ) |
12 | 8, 11 | grpidcl 18786 |
. . . . . 6
β’ (πΊ β Grp β 0 β π) |
13 | 10, 12 | syl 17 |
. . . . 5
β’ (πΊ β TopGrp β 0 β π) |
14 | 1 | conncompid 22805 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ 0 β π) β 0 β π) |
15 | 9, 13, 14 | syl2anc 585 |
. . . 4
β’ (πΊ β TopGrp β 0 β π) |
16 | 15 | ne0d 4299 |
. . 3
β’ (πΊ β TopGrp β π β β
) |
17 | | df-ima 5650 |
. . . . . . . 8
β’ ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π) = ran ((π§ β π β¦ (π¦(-gβπΊ)π§)) βΎ π) |
18 | | resmpt 5995 |
. . . . . . . . . 10
β’ (π β π β ((π§ β π β¦ (π¦(-gβπΊ)π§)) βΎ π) = (π§ β π β¦ (π¦(-gβπΊ)π§))) |
19 | 5, 18 | ax-mp 5 |
. . . . . . . . 9
β’ ((π§ β π β¦ (π¦(-gβπΊ)π§)) βΎ π) = (π§ β π β¦ (π¦(-gβπΊ)π§)) |
20 | 19 | rneqi 5896 |
. . . . . . . 8
β’ ran
((π§ β π β¦ (π¦(-gβπΊ)π§)) βΎ π) = ran (π§ β π β¦ (π¦(-gβπΊ)π§)) |
21 | 17, 20 | eqtri 2761 |
. . . . . . 7
β’ ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π) = ran (π§ β π β¦ (π¦(-gβπΊ)π§)) |
22 | | imassrn 6028 |
. . . . . . . . 9
β’ ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π) β ran (π§ β π β¦ (π¦(-gβπΊ)π§)) |
23 | 10 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π¦ β π) β πΊ β Grp) |
24 | 23 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π¦ β π) β§ π§ β π) β πΊ β Grp) |
25 | 6 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π¦ β π) β π¦ β π) |
26 | 25 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π¦ β π) β§ π§ β π) β π¦ β π) |
27 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π¦ β π) β§ π§ β π) β π§ β π) |
28 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(-gβπΊ) = (-gβπΊ) |
29 | 8, 28 | grpsubcl 18835 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ π¦ β π β§ π§ β π) β (π¦(-gβπΊ)π§) β π) |
30 | 24, 26, 27, 29 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π¦ β π) β§ π§ β π) β (π¦(-gβπΊ)π§) β π) |
31 | 30 | fmpttd 7067 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π¦ β π) β (π§ β π β¦ (π¦(-gβπΊ)π§)):πβΆπ) |
32 | 31 | frnd 6680 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π¦ β π) β ran (π§ β π β¦ (π¦(-gβπΊ)π§)) β π) |
33 | 22, 32 | sstrid 3959 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ π¦ β π) β ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π) β π) |
34 | 8, 11, 28 | grpsubid 18839 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π¦ β π) β (π¦(-gβπΊ)π¦) = 0 ) |
35 | 23, 25, 34 | syl2anc 585 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π¦ β π) β (π¦(-gβπΊ)π¦) = 0 ) |
36 | | simpr 486 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π¦ β π) β π¦ β π) |
37 | | ovex 7394 |
. . . . . . . . . . 11
β’ (π¦(-gβπΊ)π¦) β V |
38 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π§ β π β¦ (π¦(-gβπΊ)π§)) = (π§ β π β¦ (π¦(-gβπΊ)π§)) |
39 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π§ = π¦ β (π¦(-gβπΊ)π§) = (π¦(-gβπΊ)π¦)) |
40 | 38, 39 | elrnmpt1s 5916 |
. . . . . . . . . . 11
β’ ((π¦ β π β§ (π¦(-gβπΊ)π¦) β V) β (π¦(-gβπΊ)π¦) β ran (π§ β π β¦ (π¦(-gβπΊ)π§))) |
41 | 36, 37, 40 | sylancl 587 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π¦ β π) β (π¦(-gβπΊ)π¦) β ran (π§ β π β¦ (π¦(-gβπΊ)π§))) |
42 | 35, 41 | eqeltrrd 2835 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π¦ β π) β 0 β ran (π§ β π β¦ (π¦(-gβπΊ)π§))) |
43 | 42, 21 | eleqtrrdi 2845 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ π¦ β π) β 0 β ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π)) |
44 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
45 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(+gβπΊ) = (+gβπΊ) |
46 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(invgβπΊ) = (invgβπΊ) |
47 | 8, 45, 46, 28 | grpsubval 18804 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π β§ π§ β π) β (π¦(-gβπΊ)π§) = (π¦(+gβπΊ)((invgβπΊ)βπ§))) |
48 | 25, 47 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((πΊ β TopGrp β§ π¦ β π) β§ π§ β π) β (π¦(-gβπΊ)π§) = (π¦(+gβπΊ)((invgβπΊ)βπ§))) |
49 | 48 | mpteq2dva 5209 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π¦ β π) β (π§ β π β¦ (π¦(-gβπΊ)π§)) = (π§ β π β¦ (π¦(+gβπΊ)((invgβπΊ)βπ§)))) |
50 | 8, 46 | grpinvcl 18806 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ π§ β π) β ((invgβπΊ)βπ§) β π) |
51 | 23, 50 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((πΊ β TopGrp β§ π¦ β π) β§ π§ β π) β ((invgβπΊ)βπ§) β π) |
52 | 8, 46 | grpinvf 18805 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β Grp β
(invgβπΊ):πβΆπ) |
53 | 10, 52 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (πΊ β TopGrp β
(invgβπΊ):πβΆπ) |
54 | 53 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((πΊ β TopGrp β§ π¦ β π) β (invgβπΊ):πβΆπ) |
55 | 54 | feqmptd 6914 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π¦ β π) β (invgβπΊ) = (π§ β π β¦ ((invgβπΊ)βπ§))) |
56 | | eqidd 2734 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π¦ β π) β (π€ β π β¦ (π¦(+gβπΊ)π€)) = (π€ β π β¦ (π¦(+gβπΊ)π€))) |
57 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π€ = ((invgβπΊ)βπ§) β (π¦(+gβπΊ)π€) = (π¦(+gβπΊ)((invgβπΊ)βπ§))) |
58 | 51, 55, 56, 57 | fmptco 7079 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π¦ β π) β ((π€ β π β¦ (π¦(+gβπΊ)π€)) β (invgβπΊ)) = (π§ β π β¦ (π¦(+gβπΊ)((invgβπΊ)βπ§)))) |
59 | 49, 58 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π¦ β π) β (π§ β π β¦ (π¦(-gβπΊ)π§)) = ((π€ β π β¦ (π¦(+gβπΊ)π€)) β (invgβπΊ))) |
60 | 7, 46 | grpinvhmeo 23460 |
. . . . . . . . . . . . 13
β’ (πΊ β TopGrp β
(invgβπΊ)
β (π½Homeoπ½)) |
61 | 60 | adantr 482 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π¦ β π) β (invgβπΊ) β (π½Homeoπ½)) |
62 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π€ β π β¦ (π¦(+gβπΊ)π€)) = (π€ β π β¦ (π¦(+gβπΊ)π€)) |
63 | 62, 8, 45, 7 | tgplacthmeo 23477 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π¦ β π) β (π€ β π β¦ (π¦(+gβπΊ)π€)) β (π½Homeoπ½)) |
64 | 25, 63 | syldan 592 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π¦ β π) β (π€ β π β¦ (π¦(+gβπΊ)π€)) β (π½Homeoπ½)) |
65 | | hmeoco 23146 |
. . . . . . . . . . . 12
β’
(((invgβπΊ) β (π½Homeoπ½) β§ (π€ β π β¦ (π¦(+gβπΊ)π€)) β (π½Homeoπ½)) β ((π€ β π β¦ (π¦(+gβπΊ)π€)) β (invgβπΊ)) β (π½Homeoπ½)) |
66 | 61, 64, 65 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π¦ β π) β ((π€ β π β¦ (π¦(+gβπΊ)π€)) β (invgβπΊ)) β (π½Homeoπ½)) |
67 | 59, 66 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π¦ β π) β (π§ β π β¦ (π¦(-gβπΊ)π§)) β (π½Homeoπ½)) |
68 | | hmeocn 23134 |
. . . . . . . . . 10
β’ ((π§ β π β¦ (π¦(-gβπΊ)π§)) β (π½Homeoπ½) β (π§ β π β¦ (π¦(-gβπΊ)π§)) β (π½ Cn π½)) |
69 | 67, 68 | syl 17 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π¦ β π) β (π§ β π β¦ (π¦(-gβπΊ)π§)) β (π½ Cn π½)) |
70 | | toponuni 22286 |
. . . . . . . . . . . 12
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
71 | 9, 70 | syl 17 |
. . . . . . . . . . 11
β’ (πΊ β TopGrp β π = βͺ
π½) |
72 | 71 | adantr 482 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π¦ β π) β π = βͺ π½) |
73 | 5, 72 | sseqtrid 4000 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π¦ β π) β π β βͺ π½) |
74 | 1 | conncompconn 22806 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ 0 β π) β (π½ βΎt π) β Conn) |
75 | 9, 13, 74 | syl2anc 585 |
. . . . . . . . . 10
β’ (πΊ β TopGrp β (π½ βΎt π) β Conn) |
76 | 75 | adantr 482 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π¦ β π) β (π½ βΎt π) β Conn) |
77 | 44, 69, 73, 76 | connima 22799 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ π¦ β π) β (π½ βΎt ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π)) β Conn) |
78 | 1 | conncompss 22807 |
. . . . . . . 8
β’ ((((π§ β π β¦ (π¦(-gβπΊ)π§)) β π) β π β§ 0 β ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π) β§ (π½ βΎt ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π)) β Conn) β ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π) β π) |
79 | 33, 43, 77, 78 | syl3anc 1372 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π¦ β π) β ((π§ β π β¦ (π¦(-gβπΊ)π§)) β π) β π) |
80 | 21, 79 | eqsstrrid 3997 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π¦ β π) β ran (π§ β π β¦ (π¦(-gβπΊ)π§)) β π) |
81 | | ovex 7394 |
. . . . . . . 8
β’ (π¦(-gβπΊ)π§) β V |
82 | 81, 38 | fnmpti 6648 |
. . . . . . 7
β’ (π§ β π β¦ (π¦(-gβπΊ)π§)) Fn π |
83 | | df-f 6504 |
. . . . . . 7
β’ ((π§ β π β¦ (π¦(-gβπΊ)π§)):πβΆπ β ((π§ β π β¦ (π¦(-gβπΊ)π§)) Fn π β§ ran (π§ β π β¦ (π¦(-gβπΊ)π§)) β π)) |
84 | 82, 83 | mpbiran 708 |
. . . . . 6
β’ ((π§ β π β¦ (π¦(-gβπΊ)π§)):πβΆπ β ran (π§ β π β¦ (π¦(-gβπΊ)π§)) β π) |
85 | 80, 84 | sylibr 233 |
. . . . 5
β’ ((πΊ β TopGrp β§ π¦ β π) β (π§ β π β¦ (π¦(-gβπΊ)π§)):πβΆπ) |
86 | 38 | fmpt 7062 |
. . . . 5
β’
(βπ§ β
π (π¦(-gβπΊ)π§) β π β (π§ β π β¦ (π¦(-gβπΊ)π§)):πβΆπ) |
87 | 85, 86 | sylibr 233 |
. . . 4
β’ ((πΊ β TopGrp β§ π¦ β π) β βπ§ β π (π¦(-gβπΊ)π§) β π) |
88 | 87 | ralrimiva 3140 |
. . 3
β’ (πΊ β TopGrp β
βπ¦ β π βπ§ β π (π¦(-gβπΊ)π§) β π) |
89 | 8, 28 | issubg4 18955 |
. . . 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 482 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β πΊ β Grp) |
93 | | eqid 2733 |
. . . . . . . . . . 11
β’
(oppgβπΊ) = (oppgβπΊ) |
94 | 93, 46 | oppginv 19148 |
. . . . . . . . . 10
β’ (πΊ β Grp β
(invgβπΊ) =
(invgβ(oppgβπΊ))) |
95 | 92, 94 | syl 17 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β (invgβπΊ) =
(invgβ(oppgβπΊ))) |
96 | 95 | fveq1d 6848 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β ((invgβπΊ)β((invgβπΊ)βπ¦)) =
((invgβ(oppgβπΊ))β((invgβπΊ)βπ¦))) |
97 | | simprll 778 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β π¦ β π) |
98 | 8, 46 | grpinvinv 18822 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π¦ β π) β ((invgβπΊ)β((invgβπΊ)βπ¦)) = π¦) |
99 | 92, 97, 98 | syl2anc 585 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β ((invgβπΊ)β((invgβπΊ)βπ¦)) = π¦) |
100 | 96, 99 | eqtr3d 2775 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β
((invgβ(oppgβπΊ))β((invgβπΊ)βπ¦)) = π¦) |
101 | 100 | oveq1d 7376 |
. . . . . 6
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β
(((invgβ(oppgβπΊ))β((invgβπΊ)βπ¦))(+gβ(oppgβπΊ))π§) = (π¦(+gβ(oppgβπΊ))π§)) |
102 | | eqid 2733 |
. . . . . . 7
β’
(+gβ(oppgβπΊ)) =
(+gβ(oppgβπΊ)) |
103 | 45, 93, 102 | oppgplus 19135 |
. . . . . 6
β’ (π¦(+gβ(oppgβπΊ))π§) = (π§(+gβπΊ)π¦) |
104 | 101, 103 | eqtrdi 2789 |
. . . . 5
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β
(((invgβ(oppgβπΊ))β((invgβπΊ)βπ¦))(+gβ(oppgβπΊ))π§) = (π§(+gβπΊ)π¦)) |
105 | 8, 46 | grpinvcl 18806 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ π¦ β π) β ((invgβπΊ)βπ¦) β π) |
106 | 92, 97, 105 | syl2anc 585 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β ((invgβπΊ)βπ¦) β π) |
107 | | simprlr 779 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β π§ β π) |
108 | 99 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β (((invgβπΊ)β((invgβπΊ)βπ¦))(+gβπΊ)π§) = (π¦(+gβπΊ)π§)) |
109 | | simprr 772 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β (π¦(+gβπΊ)π§) β π) |
110 | 108, 109 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β (((invgβπΊ)β((invgβπΊ)βπ¦))(+gβπΊ)π§) β π) |
111 | | eqid 2733 |
. . . . . . . . . . 11
β’ (πΊ ~QG π) = (πΊ ~QG π) |
112 | 8, 46, 45, 111 | eqgval 18987 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ π β π) β (((invgβπΊ)βπ¦)(πΊ ~QG π)π§ β (((invgβπΊ)βπ¦) β π β§ π§ β π β§ (((invgβπΊ)β((invgβπΊ)βπ¦))(+gβπΊ)π§) β π))) |
113 | 92, 5, 112 | sylancl 587 |
. . . . . . . . 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 23486 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§
((invgβπΊ)βπ¦) β π) β [((invgβπΊ)βπ¦)](πΊ ~QG π) = βͺ {π₯ β π« π β£
(((invgβπΊ)βπ¦) β π₯ β§ (π½ βΎt π₯) β Conn)}) |
116 | 106, 115 | syldan 592 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β [((invgβπΊ)βπ¦)](πΊ ~QG π) = βͺ {π₯ β π« π β£
(((invgβπΊ)βπ¦) β π₯ β§ (π½ βΎt π₯) β Conn)}) |
117 | 93 | oppgtgp 23472 |
. . . . . . . . . . . . 13
β’ (πΊ β TopGrp β
(oppgβπΊ) β TopGrp) |
118 | 117 | adantr 482 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β
(oppgβπΊ) β TopGrp) |
119 | 93, 8 | oppgbas 19138 |
. . . . . . . . . . . . 13
β’ π =
(Baseβ(oppgβπΊ)) |
120 | 93, 11 | oppgid 19145 |
. . . . . . . . . . . . 13
β’ 0 =
(0gβ(oppgβπΊ)) |
121 | 93, 7 | oppgtopn 19142 |
. . . . . . . . . . . . 13
β’ π½ =
(TopOpenβ(oppgβπΊ)) |
122 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
((oppgβπΊ) ~QG π) = ((oppgβπΊ) ~QG π) |
123 | 119, 120,
121, 1, 122 | tgpconncompeqg 23486 |
. . . . . . . . . . . 12
β’
(((oppgβπΊ) β TopGrp β§
((invgβπΊ)βπ¦) β π) β [((invgβπΊ)βπ¦)]((oppgβπΊ) ~QG π) = βͺ
{π₯ β π« π β£
(((invgβπΊ)βπ¦) β π₯ β§ (π½ βΎt π₯) β Conn)}) |
124 | 118, 106,
123 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β [((invgβπΊ)βπ¦)]((oppgβπΊ) ~QG π) = βͺ
{π₯ β π« π β£
(((invgβπΊ)βπ¦) β π₯ β§ (π½ βΎt π₯) β Conn)}) |
125 | 116, 124 | eqtr4d 2776 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β [((invgβπΊ)βπ¦)](πΊ ~QG π) = [((invgβπΊ)βπ¦)]((oppgβπΊ) ~QG π)) |
126 | 125 | eleq2d 2820 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β (π§ β [((invgβπΊ)βπ¦)](πΊ ~QG π) β π§ β [((invgβπΊ)βπ¦)]((oppgβπΊ) ~QG π))) |
127 | | vex 3451 |
. . . . . . . . . 10
β’ π§ β V |
128 | | fvex 6859 |
. . . . . . . . . 10
β’
((invgβπΊ)βπ¦) β V |
129 | 127, 128 | elec 8698 |
. . . . . . . . 9
β’ (π§ β
[((invgβπΊ)βπ¦)](πΊ ~QG π) β ((invgβπΊ)βπ¦)(πΊ ~QG π)π§) |
130 | 127, 128 | elec 8698 |
. . . . . . . . 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 2733 |
. . . . . . . . 9
β’
(invgβ(oppgβπΊ)) =
(invgβ(oppgβπΊ)) |
134 | 119, 133,
102, 122 | eqgval 18987 |
. . . . . . . 8
β’
(((oppgβπΊ) β TopGrp β§ π β π) β (((invgβπΊ)βπ¦)((oppgβπΊ) ~QG π)π§ β (((invgβπΊ)βπ¦) β π β§ π§ β π β§
(((invgβ(oppgβπΊ))β((invgβπΊ)βπ¦))(+gβ(oppgβπΊ))π§) β π))) |
135 | 118, 5, 134 | sylancl 587 |
. . . . . . 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 1145 |
. . . . 5
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β
(((invgβ(oppgβπΊ))β((invgβπΊ)βπ¦))(+gβ(oppgβπΊ))π§) β π) |
138 | 104, 137 | eqeltrrd 2835 |
. . . 4
β’ ((πΊ β TopGrp β§ ((π¦ β π β§ π§ β π) β§ (π¦(+gβπΊ)π§) β π)) β (π§(+gβπΊ)π¦) β π) |
139 | 138 | expr 458 |
. . 3
β’ ((πΊ β TopGrp β§ (π¦ β π β§ π§ β π)) β ((π¦(+gβπΊ)π§) β π β (π§(+gβπΊ)π¦) β π)) |
140 | 139 | ralrimivva 3194 |
. 2
β’ (πΊ β TopGrp β
βπ¦ β π βπ§ β π ((π¦(+gβπΊ)π§) β π β (π§(+gβπΊ)π¦) β π)) |
141 | 8, 45 | isnsg2 18966 |
. 2
β’ (π β (NrmSGrpβπΊ) β (π β (SubGrpβπΊ) β§ βπ¦ β π βπ§ β π ((π¦(+gβπΊ)π§) β π β (π§(+gβπΊ)π¦) β π))) |
142 | 91, 140, 141 | sylanbrc 584 |
1
β’ (πΊ β TopGrp β π β (NrmSGrpβπΊ)) |