Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  symggen Structured version   Unicode version

Theorem symggen 15967
 Description: The span of the transpositions is the subgroup that moves finitely many points. (Contributed by Stefan O'Rear, 28-Aug-2015.)
Hypotheses
Ref Expression
symgtrf.t pmTrsp
symgtrf.g
symgtrf.b
symggen.k mrClsSubMnd
Assertion
Ref Expression
symggen
Distinct variable groups:   ,   ,   ,   ,   ,   ,

Proof of Theorem symggen
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2976 . . . 4
2 symgtrf.g . . . . . . 7
32symggrp 15896 . . . . . 6
4 grpmnd 15541 . . . . . 6
53, 4syl 16 . . . . 5
6 symgtrf.b . . . . . 6
76submacs 15484 . . . . 5 SubMnd ACS
8 acsmre 14582 . . . . 5 SubMnd ACS SubMnd Moore
95, 7, 83syl 20 . . . 4 SubMnd Moore
101, 9syl 16 . . 3 SubMnd Moore
11 symgtrf.t . . . . . 6 pmTrsp
1211, 2, 6symgtrf 15966 . . . . 5
1312a1i 11 . . . 4
14 2onn 7071 . . . . . 6
15 nnfi 7495 . . . . . 6
1614, 15ax-mp 5 . . . . 5
17 eqid 2438 . . . . . . . . 9 pmTrsp pmTrsp
1817, 11pmtrfb 15962 . . . . . . . 8
1918simp3bi 1005 . . . . . . 7
20 enfi 7521 . . . . . . 7
2119, 20syl 16 . . . . . 6
2221adantl 466 . . . . 5
2316, 22mpbiri 233 . . . 4
2413, 23ssrabdv 3426 . . 3
252, 6symgfisg 15965 . . . 4 SubGrp
26 subgsubm 15694 . . . 4 SubGrp SubMnd
2725, 26syl 16 . . 3 SubMnd
28 symggen.k . . . 4 mrClsSubMnd
2928mrcsscl 14550 . . 3 SubMnd Moore SubMnd
3010, 24, 27, 29syl3anc 1218 . 2
31 vex 2970 . . . . . . 7
3231a1i 11 . . . . . 6
33 finnum 8110 . . . . . 6
34 domfi 7526 . . . . . . . 8
352, 6elsymgbas2 15877 . . . . . . . . . . . . . . . 16
3635ibi 241 . . . . . . . . . . . . . . 15
3736adantl 466 . . . . . . . . . . . . . 14
38 f1ofn 5637 . . . . . . . . . . . . . 14
39 fnnfpeq0 5904 . . . . . . . . . . . . . 14
4037, 38, 393syl 20 . . . . . . . . . . . . 13
412, 6elbasfv 14213 . . . . . . . . . . . . . . . . 17
4241adantl 466 . . . . . . . . . . . . . . . 16
432symgid 15897 . . . . . . . . . . . . . . . 16
4442, 43syl 16 . . . . . . . . . . . . . . 15
4542, 9syl 16 . . . . . . . . . . . . . . . . 17 SubMnd Moore
4628mrccl 14541 . . . . . . . . . . . . . . . . 17 SubMnd Moore SubMnd
4745, 12, 46sylancl 662 . . . . . . . . . . . . . . . 16 SubMnd
48 eqid 2438 . . . . . . . . . . . . . . . . 17
4948subm0cl 15471 . . . . . . . . . . . . . . . 16 SubMnd
5047, 49syl 16 . . . . . . . . . . . . . . 15
5144, 50eqeltrd 2512 . . . . . . . . . . . . . 14
52 eleq1a 2507 . . . . . . . . . . . . . 14
5351, 52syl 16 . . . . . . . . . . . . 13
5440, 53sylbid 215 . . . . . . . . . . . 12
5554adantr 465 . . . . . . . . . . 11
56 n0 3641 . . . . . . . . . . . 12
5742adantr 465 . . . . . . . . . . . . . . . . . . . . 21
58 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23
59 f1omvdmvd 15940 . . . . . . . . . . . . . . . . . . . . . . . . 25
6037, 59sylan 471 . . . . . . . . . . . . . . . . . . . . . . . 24
6160eldifad 3335 . . . . . . . . . . . . . . . . . . . . . . 23
62 prssi 4024 . . . . . . . . . . . . . . . . . . . . . . 23
6358, 61, 62syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
64 difss 3478 . . . . . . . . . . . . . . . . . . . . . . . . 25
65 dmss 5034 . . . . . . . . . . . . . . . . . . . . . . . . 25
6664, 65ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24
67 f1odm 5640 . . . . . . . . . . . . . . . . . . . . . . . . 25
6837, 67syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
6966, 68syl5sseq 3399 . . . . . . . . . . . . . . . . . . . . . . 23
7069adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
7163, 70sstrd 3361 . . . . . . . . . . . . . . . . . . . . 21
7237adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7372, 38syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
7469sselda 3351 . . . . . . . . . . . . . . . . . . . . . . . . 25
75 fnelnfp 5903 . . . . . . . . . . . . . . . . . . . . . . . . 25
7673, 74, 75syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
7758, 76mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23
7877necomd 2690 . . . . . . . . . . . . . . . . . . . . . 22
79 vex 2970 . . . . . . . . . . . . . . . . . . . . . . 23
80 fvex 5696 . . . . . . . . . . . . . . . . . . . . . . 23
81 pr2nelem 8163 . . . . . . . . . . . . . . . . . . . . . . 23
8279, 80, 81mp3an12 1304 . . . . . . . . . . . . . . . . . . . . . 22
8378, 82syl 16 . . . . . . . . . . . . . . . . . . . . 21
8417, 11pmtrrn 15954 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp
8557, 71, 83, 84syl3anc 1218 . . . . . . . . . . . . . . . . . . . 20 pmTrsp
8612, 85sseldi 3349 . . . . . . . . . . . . . . . . . . 19 pmTrsp
87 simplr 754 . . . . . . . . . . . . . . . . . . 19
88 eqid 2438 . . . . . . . . . . . . . . . . . . . 20
892, 6, 88symgov 15886 . . . . . . . . . . . . . . . . . . 19 pmTrsp pmTrsp pmTrsp
9086, 87, 89syl2anc 661 . . . . . . . . . . . . . . . . . 18 pmTrsp pmTrsp
9190oveq2d 6102 . . . . . . . . . . . . . . . . 17 pmTrsp pmTrsp pmTrsp pmTrsp
9242, 3syl 16 . . . . . . . . . . . . . . . . . . . . 21
9392adantr 465 . . . . . . . . . . . . . . . . . . . 20
946, 88grpcl 15542 . . . . . . . . . . . . . . . . . . . 20 pmTrsp pmTrsp
9593, 86, 87, 94syl3anc 1218 . . . . . . . . . . . . . . . . . . 19 pmTrsp
9690, 95eqeltrrd 2513 . . . . . . . . . . . . . . . . . 18 pmTrsp
972, 6, 88symgov 15886 . . . . . . . . . . . . . . . . . 18 pmTrsp pmTrsp pmTrsp pmTrsp pmTrsp pmTrsp
9886, 96, 97syl2anc 661 . . . . . . . . . . . . . . . . 17 pmTrsp pmTrsp pmTrsp pmTrsp
99 coass 5351 . . . . . . . . . . . . . . . . . 18 pmTrsp pmTrsp pmTrsp pmTrsp
10017, 11pmtrfinv 15958 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp pmTrsp pmTrsp
10185, 100syl 16 . . . . . . . . . . . . . . . . . . . 20 pmTrsp pmTrsp
102101coeq1d 4996 . . . . . . . . . . . . . . . . . . 19 pmTrsp pmTrsp
103 f1of 5636 . . . . . . . . . . . . . . . . . . . 20
104 fcoi2 5581 . . . . . . . . . . . . . . . . . . . 20
10572, 103, 1043syl 20 . . . . . . . . . . . . . . . . . . 19
106102, 105eqtrd 2470 . . . . . . . . . . . . . . . . . 18 pmTrsp pmTrsp
10799, 106syl5eqr 2484 . . . . . . . . . . . . . . . . 17 pmTrsp pmTrsp
10891, 98, 1073eqtrd 2474 . . . . . . . . . . . . . . . 16 pmTrsp pmTrsp
109108adantlr 714 . . . . . . . . . . . . . . 15 pmTrsp pmTrsp
11047ad2antrr 725 . . . . . . . . . . . . . . . 16 SubMnd
11128mrcssid 14547 . . . . . . . . . . . . . . . . . . . 20 SubMnd Moore
11245, 12, 111sylancl 662 . . . . . . . . . . . . . . . . . . 19
113112adantr 465 . . . . . . . . . . . . . . . . . 18
114113, 85sseldd 3352 . . . . . . . . . . . . . . . . 17 pmTrsp
115114adantlr 714 . . . . . . . . . . . . . . . 16 pmTrsp
11690difeq1d 3468 . . . . . . . . . . . . . . . . . . . 20 pmTrsp pmTrsp
117116dmeqd 5037 . . . . . . . . . . . . . . . . . . 19 pmTrsp pmTrsp
118 simpll 753 . . . . . . . . . . . . . . . . . . . 20
119 mvdco 15942 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp pmTrsp
12017pmtrmvd 15953 . . . . . . . . . . . . . . . . . . . . . . . . 25 pmTrsp
12157, 71, 83, 120syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp
122121, 63eqsstrd 3385 . . . . . . . . . . . . . . . . . . . . . . 23 pmTrsp
123 ssid 3370 . . . . . . . . . . . . . . . . . . . . . . . 24
124123a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
125122, 124unssd 3527 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp
126119, 125syl5ss 3362 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp
127 fvco2 5761 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp pmTrsp
12873, 74, 127syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23 pmTrsp pmTrsp
129 prcom 3948 . . . . . . . . . . . . . . . . . . . . . . . . . 26
130129fveq2i 5689 . . . . . . . . . . . . . . . . . . . . . . . . 25 pmTrsp pmTrsp
131130fveq1i 5687 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp pmTrsp
13270, 61sseldd 3352 . . . . . . . . . . . . . . . . . . . . . . . . 25
13317pmtrprfv 15950 . . . . . . . . . . . . . . . . . . . . . . . . 25 pmTrsp
13457, 132, 74, 77, 133syl13anc 1220 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp
135131, 134syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . 23 pmTrsp
136128, 135eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp
1372, 6elsymgbas2 15877 . . . . . . . . . . . . . . . . . . . . . . . . 25 pmTrsp pmTrsp pmTrsp
138137ibi 241 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp pmTrsp
139 f1ofn 5637 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp pmTrsp
14096, 138, 1393syl 20 . . . . . . . . . . . . . . . . . . . . . . 23 pmTrsp
141 fnelnfp 5903 . . . . . . . . . . . . . . . . . . . . . . . 24 pmTrsp pmTrsp pmTrsp
142141necon2bbid 2664 . . . . . . . . . . . . . . . . . . . . . . 23 pmTrsp pmTrsp pmTrsp
143140, 74, 142syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp pmTrsp
144136, 143mpbid 210 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp
145126, 58, 144ssnelpssd 3738 . . . . . . . . . . . . . . . . . . . 20 pmTrsp
146 php3 7489 . . . . . . . . . . . . . . . . . . . 20 pmTrsp pmTrsp
147118, 145, 146syl2anc 661 . . . . . . . . . . . . . . . . . . 19 pmTrsp
148117, 147eqbrtrd 4307 . . . . . . . . . . . . . . . . . 18 pmTrsp
149148adantlr 714 . . . . . . . . . . . . . . . . 17 pmTrsp
15095adantlr 714 . . . . . . . . . . . . . . . . 17 pmTrsp
151 ovex 6111 . . . . . . . . . . . . . . . . . . 19 pmTrsp
152 difeq1 3462 . . . . . . . . . . . . . . . . . . . . . 22 pmTrsp pmTrsp
153152dmeqd 5037 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp pmTrsp
154153breq1d 4297 . . . . . . . . . . . . . . . . . . . 20 pmTrsp pmTrsp
155 eleq1 2498 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp pmTrsp
156 eleq1 2498 . . . . . . . . . . . . . . . . . . . . 21 pmTrsp pmTrsp
157155, 156imbi12d 320 . . . . . . . . . . . . . . . . . . . 20 pmTrsp pmTrsp pmTrsp
158154, 157imbi12d 320 . . . . . . . . . . . . . . . . . . 19 pmTrsp pmTrsp pmTrsp pmTrsp
159151, 158spcv 3058 . . . . . . . . . . . . . . . . . 18 pmTrsp pmTrsp pmTrsp
160159ad2antlr 726 . . . . . . . . . . . . . . . . 17 pmTrsp pmTrsp pmTrsp
161149, 150, 160mp2d 45 . . . . . . . . . . . . . . . 16 pmTrsp
16288submcl 15472 . . . . . . . . . . . . . . . 16 SubMnd pmTrsp pmTrsp pmTrsp pmTrsp
163110, 115, 161, 162syl3anc 1218 . . . . . . . . . . . . . . 15 pmTrsp pmTrsp
164109, 163eqeltrrd 2513 . . . . . . . . . . . . . 14
165164ex 434 . . . . . . . . . . . . 13
166165exlimdv 1690 . . . . . . . . . . . 12
16756, 166syl5bi 217 . . . . . . . . . . 11
16855, 167pm2.61dne 2683 . . . . . . . . . 10
169168exp31 604 . . . . . . . . 9
170169com23 78 . . . . . . . 8
17134, 170syl 16 . . . . . . 7
1721713impia 1184 . . . . . 6
173 eleq1 2498 . . . . . . 7
174 eleq1 2498 . . . . . . 7
175173, 174imbi12d 320 . . . . . 6
176 eleq1 2498 . . . . . . 7
177 eleq1 2498 . . . . . . 7
178176, 177imbi12d 320 . . . . . 6
179 difeq1 3462 . . . . . . 7
180179dmeqd 5037 . . . . . 6
181 difeq1 3462 . . . . . . 7
182181dmeqd 5037 . . . . . 6
18332, 33, 172, 175, 178, 180, 182indcardi 8203 . . . . 5
184183impcom 430 . . . 4