Step | Hyp | Ref
| Expression |
1 | | tgpconncomp.s |
. . . . 5
↾t Conn |
2 | | ssrab2 3687 |
. . . . . 6
↾t Conn |
3 | | sspwuni 4611 |
. . . . . 6
↾t Conn
↾t Conn |
4 | 2, 3 | mpbi 220 |
. . . . 5
↾t Conn |
5 | 1, 4 | eqsstri 3635 |
. . . 4
|
6 | 5 | a1i 11 |
. . 3
|
7 | | tgpconncomp.j |
. . . . . 6
|
8 | | tgpconncomp.x |
. . . . . 6
|
9 | 7, 8 | tgptopon 21886 |
. . . . 5
TopOn |
10 | | tgpgrp 21882 |
. . . . . 6
|
11 | | tgpconncomp.z |
. . . . . . 7
|
12 | 8, 11 | grpidcl 17450 |
. . . . . 6
|
13 | 10, 12 | syl 17 |
. . . . 5
|
14 | 1 | conncompid 21234 |
. . . . 5
TopOn |
15 | 9, 13, 14 | syl2anc 693 |
. . . 4
|
16 | | ne0i 3921 |
. . . 4
|
17 | 15, 16 | syl 17 |
. . 3
|
18 | | df-ima 5127 |
. . . . . . . 8
|
19 | | resmpt 5449 |
. . . . . . . . . 10
|
20 | 5, 19 | ax-mp 5 |
. . . . . . . . 9
|
21 | 20 | rneqi 5352 |
. . . . . . . 8
|
22 | 18, 21 | eqtri 2644 |
. . . . . . 7
|
23 | | imassrn 5477 |
. . . . . . . . 9
|
24 | 10 | adantr 481 |
. . . . . . . . . . . . 13
|
25 | 24 | adantr 481 |
. . . . . . . . . . . 12
|
26 | 6 | sselda 3603 |
. . . . . . . . . . . . 13
|
27 | 26 | adantr 481 |
. . . . . . . . . . . 12
|
28 | | simpr 477 |
. . . . . . . . . . . 12
|
29 | | eqid 2622 |
. . . . . . . . . . . . 13
|
30 | 8, 29 | grpsubcl 17495 |
. . . . . . . . . . . 12
|
31 | 25, 27, 28, 30 | syl3anc 1326 |
. . . . . . . . . . 11
|
32 | | eqid 2622 |
. . . . . . . . . . 11
|
33 | 31, 32 | fmptd 6385 |
. . . . . . . . . 10
|
34 | | frn 6053 |
. . . . . . . . . 10
|
35 | 33, 34 | syl 17 |
. . . . . . . . 9
|
36 | 23, 35 | syl5ss 3614 |
. . . . . . . 8
|
37 | 8, 11, 29 | grpsubid 17499 |
. . . . . . . . . . 11
|
38 | 24, 26, 37 | syl2anc 693 |
. . . . . . . . . 10
|
39 | | simpr 477 |
. . . . . . . . . . 11
|
40 | | ovex 6678 |
. . . . . . . . . . 11
|
41 | | eqid 2622 |
. . . . . . . . . . . 12
|
42 | | oveq2 6658 |
. . . . . . . . . . . 12
|
43 | 41, 42 | elrnmpt1s 5373 |
. . . . . . . . . . 11
|
44 | 39, 40, 43 | sylancl 694 |
. . . . . . . . . 10
|
45 | 38, 44 | eqeltrrd 2702 |
. . . . . . . . 9
|
46 | 45, 22 | syl6eleqr 2712 |
. . . . . . . 8
|
47 | | eqid 2622 |
. . . . . . . . 9
|
48 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
49 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
50 | 8, 48, 49, 29 | grpsubval 17465 |
. . . . . . . . . . . . . 14
|
51 | 26, 50 | sylan 488 |
. . . . . . . . . . . . 13
|
52 | 51 | mpteq2dva 4744 |
. . . . . . . . . . . 12
|
53 | 8, 49 | grpinvcl 17467 |
. . . . . . . . . . . . . 14
|
54 | 24, 53 | sylan 488 |
. . . . . . . . . . . . 13
|
55 | 8, 49 | grpinvf 17466 |
. . . . . . . . . . . . . . . 16
|
56 | 10, 55 | syl 17 |
. . . . . . . . . . . . . . 15
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . 14
|
58 | 57 | feqmptd 6249 |
. . . . . . . . . . . . 13
|
59 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
60 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
61 | 54, 58, 59, 60 | fmptco 6396 |
. . . . . . . . . . . 12
|
62 | 52, 61 | eqtr4d 2659 |
. . . . . . . . . . 11
|
63 | 7, 49 | grpinvhmeo 21890 |
. . . . . . . . . . . . 13
|
64 | 63 | adantr 481 |
. . . . . . . . . . . 12
|
65 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
66 | 65, 8, 48, 7 | tgplacthmeo 21907 |
. . . . . . . . . . . . 13
|
67 | 26, 66 | syldan 487 |
. . . . . . . . . . . 12
|
68 | | hmeoco 21575 |
. . . . . . . . . . . 12
|
69 | 64, 67, 68 | syl2anc 693 |
. . . . . . . . . . 11
|
70 | 62, 69 | eqeltrd 2701 |
. . . . . . . . . 10
|
71 | | hmeocn 21563 |
. . . . . . . . . 10
|
72 | 70, 71 | syl 17 |
. . . . . . . . 9
|
73 | | toponuni 20719 |
. . . . . . . . . . . 12
TopOn
|
74 | 9, 73 | syl 17 |
. . . . . . . . . . 11
|
75 | 74 | adantr 481 |
. . . . . . . . . 10
|
76 | 5, 75 | syl5sseq 3653 |
. . . . . . . . 9
|
77 | 1 | conncompconn 21235 |
. . . . . . . . . . 11
TopOn ↾t Conn |
78 | 9, 13, 77 | syl2anc 693 |
. . . . . . . . . 10
↾t Conn |
79 | 78 | adantr 481 |
. . . . . . . . 9
↾t Conn |
80 | 47, 72, 76, 79 | connima 21228 |
. . . . . . . 8
↾t Conn |
81 | 1 | conncompss 21236 |
. . . . . . . 8
↾t Conn |
82 | 36, 46, 80, 81 | syl3anc 1326 |
. . . . . . 7
|
83 | 22, 82 | syl5eqssr 3650 |
. . . . . 6
|
84 | | ovex 6678 |
. . . . . . . 8
|
85 | 84, 41 | fnmpti 6022 |
. . . . . . 7
|
86 | | df-f 5892 |
. . . . . . 7
|
87 | 85, 86 | mpbiran 953 |
. . . . . 6
|
88 | 83, 87 | sylibr 224 |
. . . . 5
|
89 | 41 | fmpt 6381 |
. . . . 5
|
90 | 88, 89 | sylibr 224 |
. . . 4
|
91 | 90 | ralrimiva 2966 |
. . 3
|
92 | 8, 29 | issubg4 17613 |
. . . 4
SubGrp
|
93 | 10, 92 | syl 17 |
. . 3
SubGrp
|
94 | 6, 17, 91, 93 | mpbir3and 1245 |
. 2
SubGrp |
95 | 10 | adantr 481 |
. . . . . . . . . 10
|
96 | | eqid 2622 |
. . . . . . . . . . 11
oppg oppg |
97 | 96, 49 | oppginv 17789 |
. . . . . . . . . 10
oppg |
98 | 95, 97 | syl 17 |
. . . . . . . . 9
oppg |
99 | 98 | fveq1d 6193 |
. . . . . . . 8
oppg |
100 | | simprll 802 |
. . . . . . . . 9
|
101 | 8, 49 | grpinvinv 17482 |
. . . . . . . . 9
|
102 | 95, 100, 101 | syl2anc 693 |
. . . . . . . 8
|
103 | 99, 102 | eqtr3d 2658 |
. . . . . . 7
oppg |
104 | 103 | oveq1d 6665 |
. . . . . 6
oppg oppg oppg |
105 | | eqid 2622 |
. . . . . . 7
oppg oppg |
106 | 48, 96, 105 | oppgplus 17779 |
. . . . . 6
oppg |
107 | 104, 106 | syl6eq 2672 |
. . . . 5
oppg oppg |
108 | 8, 49 | grpinvcl 17467 |
. . . . . . . . . 10
|
109 | 95, 100, 108 | syl2anc 693 |
. . . . . . . . 9
|
110 | | simprlr 803 |
. . . . . . . . 9
|
111 | 102 | oveq1d 6665 |
. . . . . . . . . 10
|
112 | | simprr 796 |
. . . . . . . . . 10
|
113 | 111, 112 | eqeltrd 2701 |
. . . . . . . . 9
|
114 | | eqid 2622 |
. . . . . . . . . . 11
~QG ~QG |
115 | 8, 49, 48, 114 | eqgval 17643 |
. . . . . . . . . 10
~QG
|
116 | 95, 5, 115 | sylancl 694 |
. . . . . . . . 9
~QG
|
117 | 109, 110,
113, 116 | mpbir3and 1245 |
. . . . . . . 8
~QG |
118 | 8, 11, 7, 1, 114 | tgpconncompeqg 21915 |
. . . . . . . . . . . 12
~QG
↾t Conn |
119 | 109, 118 | syldan 487 |
. . . . . . . . . . 11
~QG
↾t Conn |
120 | 96 | oppgtgp 21902 |
. . . . . . . . . . . . 13
oppg |
121 | 120 | adantr 481 |
. . . . . . . . . . . 12
oppg |
122 | 96, 8 | oppgbas 17781 |
. . . . . . . . . . . . 13
oppg |
123 | 96, 11 | oppgid 17786 |
. . . . . . . . . . . . 13
oppg |
124 | 96, 7 | oppgtopn 17783 |
. . . . . . . . . . . . 13
oppg |
125 | | eqid 2622 |
. . . . . . . . . . . . 13
oppg
~QG oppg ~QG |
126 | 122, 123,
124, 1, 125 | tgpconncompeqg 21915 |
. . . . . . . . . . . 12
oppg oppg
~QG
↾t Conn |
127 | 121, 109,
126 | syl2anc 693 |
. . . . . . . . . . 11
oppg
~QG
↾t Conn |
128 | 119, 127 | eqtr4d 2659 |
. . . . . . . . . 10
~QG oppg
~QG |
129 | 128 | eleq2d 2687 |
. . . . . . . . 9
~QG oppg
~QG |
130 | | vex 3203 |
. . . . . . . . . 10
|
131 | | fvex 6201 |
. . . . . . . . . 10
|
132 | 130, 131 | elec 7786 |
. . . . . . . . 9
~QG ~QG |
133 | 130, 131 | elec 7786 |
. . . . . . . . 9
oppg ~QG
oppg ~QG |
134 | 129, 132,
133 | 3bitr3g 302 |
. . . . . . . 8
~QG oppg ~QG |
135 | 117, 134 | mpbid 222 |
. . . . . . 7
oppg ~QG |
136 | | eqid 2622 |
. . . . . . . . 9
oppg oppg |
137 | 122, 136,
105, 125 | eqgval 17643 |
. . . . . . . 8
oppg
oppg ~QG
oppg oppg |
138 | 121, 5, 137 | sylancl 694 |
. . . . . . 7
oppg ~QG
oppg oppg |
139 | 135, 138 | mpbid 222 |
. . . . . 6
oppg oppg |
140 | 139 | simp3d 1075 |
. . . . 5
oppg oppg |
141 | 107, 140 | eqeltrrd 2702 |
. . . 4
|
142 | 141 | expr 643 |
. . 3
|
143 | 142 | ralrimivva 2971 |
. 2
|
144 | 8, 48 | isnsg2 17624 |
. 2
NrmSGrp SubGrp
|
145 | 94, 143, 144 | sylanbrc 698 |
1
NrmSGrp |