Metamath Proof Explorer

Theorem symgfisg

Description: The symmetric group has a subgroup of permutations that move finitely many points. (Contributed by Stefan O'Rear, 24-Aug-2015)

Ref Expression
Hypotheses symgsssg.g 
|- G = ( SymGrp ` D )
symgsssg.b 
|- B = ( Base ` G )
Assertion symgfisg 
|- ( D e. V -> { x e. B | dom ( x \ _I ) e. Fin } e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 symgsssg.g 
 |-  G = ( SymGrp ` D )
2 symgsssg.b 
 |-  B = ( Base ` G )
3 eqidd 
 |-  ( D e. V -> ( G |`s { x e. B | dom ( x \ _I ) e. Fin } ) = ( G |`s { x e. B | dom ( x \ _I ) e. Fin } ) )
4 eqidd 
 |-  ( D e. V -> ( 0g ` G ) = ( 0g ` G ) )
5 eqidd 
 |-  ( D e. V -> ( +g ` G ) = ( +g ` G ) )
6 ssrab2 
 |-  { x e. B | dom ( x \ _I ) e. Fin } C_ B
7 6 2 sseqtri 
 |-  { x e. B | dom ( x \ _I ) e. Fin } C_ ( Base ` G )
8 7 a1i 
 |-  ( D e. V -> { x e. B | dom ( x \ _I ) e. Fin } C_ ( Base ` G ) )
9 difeq1 
 |-  ( x = ( 0g ` G ) -> ( x \ _I ) = ( ( 0g ` G ) \ _I ) )
10 9 dmeqd 
 |-  ( x = ( 0g ` G ) -> dom ( x \ _I ) = dom ( ( 0g ` G ) \ _I ) )
11 10 eleq1d 
 |-  ( x = ( 0g ` G ) -> ( dom ( x \ _I ) e. Fin <-> dom ( ( 0g ` G ) \ _I ) e. Fin ) )
12 1 symggrp 
 |-  ( D e. V -> G e. Grp )
13 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
14 2 13 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
15 12 14 syl 
 |-  ( D e. V -> ( 0g ` G ) e. B )
16 1 symgid 
 |-  ( D e. V -> ( _I |` D ) = ( 0g ` G ) )
17 16 difeq1d 
 |-  ( D e. V -> ( ( _I |` D ) \ _I ) = ( ( 0g ` G ) \ _I ) )
18 17 dmeqd 
 |-  ( D e. V -> dom ( ( _I |` D ) \ _I ) = dom ( ( 0g ` G ) \ _I ) )
19 resss 
 |-  ( _I |` D ) C_ _I
20 ssdif0 
 |-  ( ( _I |` D ) C_ _I <-> ( ( _I |` D ) \ _I ) = (/) )
21 19 20 mpbi 
 |-  ( ( _I |` D ) \ _I ) = (/)
22 21 dmeqi 
 |-  dom ( ( _I |` D ) \ _I ) = dom (/)
23 dm0 
 |-  dom (/) = (/)
24 22 23 eqtri 
 |-  dom ( ( _I |` D ) \ _I ) = (/)
25 0fi 
 |-  (/) e. Fin
26 24 25 eqeltri 
 |-  dom ( ( _I |` D ) \ _I ) e. Fin
27 18 26 eqeltrrdi 
 |-  ( D e. V -> dom ( ( 0g ` G ) \ _I ) e. Fin )
28 11 15 27 elrabd 
 |-  ( D e. V -> ( 0g ` G ) e. { x e. B | dom ( x \ _I ) e. Fin } )
29 biid 
 |-  ( D e. V <-> D e. V )
30 difeq1 
 |-  ( x = y -> ( x \ _I ) = ( y \ _I ) )
31 30 dmeqd 
 |-  ( x = y -> dom ( x \ _I ) = dom ( y \ _I ) )
32 31 eleq1d 
 |-  ( x = y -> ( dom ( x \ _I ) e. Fin <-> dom ( y \ _I ) e. Fin ) )
33 32 elrab 
 |-  ( y e. { x e. B | dom ( x \ _I ) e. Fin } <-> ( y e. B /\ dom ( y \ _I ) e. Fin ) )
34 difeq1 
 |-  ( x = z -> ( x \ _I ) = ( z \ _I ) )
35 34 dmeqd 
 |-  ( x = z -> dom ( x \ _I ) = dom ( z \ _I ) )
36 35 eleq1d 
 |-  ( x = z -> ( dom ( x \ _I ) e. Fin <-> dom ( z \ _I ) e. Fin ) )
37 36 elrab 
 |-  ( z e. { x e. B | dom ( x \ _I ) e. Fin } <-> ( z e. B /\ dom ( z \ _I ) e. Fin ) )
38 difeq1 
 |-  ( x = ( y ( +g ` G ) z ) -> ( x \ _I ) = ( ( y ( +g ` G ) z ) \ _I ) )
39 38 dmeqd 
 |-  ( x = ( y ( +g ` G ) z ) -> dom ( x \ _I ) = dom ( ( y ( +g ` G ) z ) \ _I ) )
40 39 eleq1d 
 |-  ( x = ( y ( +g ` G ) z ) -> ( dom ( x \ _I ) e. Fin <-> dom ( ( y ( +g ` G ) z ) \ _I ) e. Fin ) )
41 12 3ad2ant1 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> G e. Grp )
42 simp2l 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> y e. B )
43 simp3l 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> z e. B )
44 eqid 
 |-  ( +g ` G ) = ( +g ` G )
45 2 44 grpcl 
 |-  ( ( G e. Grp /\ y e. B /\ z e. B ) -> ( y ( +g ` G ) z ) e. B )
46 41 42 43 45 syl3anc 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> ( y ( +g ` G ) z ) e. B )
47 1 2 44 symgov 
 |-  ( ( y e. B /\ z e. B ) -> ( y ( +g ` G ) z ) = ( y o. z ) )
48 42 43 47 syl2anc 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> ( y ( +g ` G ) z ) = ( y o. z ) )
49 48 difeq1d 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> ( ( y ( +g ` G ) z ) \ _I ) = ( ( y o. z ) \ _I ) )
50 49 dmeqd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> dom ( ( y ( +g ` G ) z ) \ _I ) = dom ( ( y o. z ) \ _I ) )
51 simp2r 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> dom ( y \ _I ) e. Fin )
52 simp3r 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> dom ( z \ _I ) e. Fin )
53 unfi 
 |-  ( ( dom ( y \ _I ) e. Fin /\ dom ( z \ _I ) e. Fin ) -> ( dom ( y \ _I ) u. dom ( z \ _I ) ) e. Fin )
54 51 52 53 syl2anc 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> ( dom ( y \ _I ) u. dom ( z \ _I ) ) e. Fin )
55 mvdco 
 |-  dom ( ( y o. z ) \ _I ) C_ ( dom ( y \ _I ) u. dom ( z \ _I ) )
56 ssfi 
 |-  ( ( ( dom ( y \ _I ) u. dom ( z \ _I ) ) e. Fin /\ dom ( ( y o. z ) \ _I ) C_ ( dom ( y \ _I ) u. dom ( z \ _I ) ) ) -> dom ( ( y o. z ) \ _I ) e. Fin )
57 54 55 56 sylancl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> dom ( ( y o. z ) \ _I ) e. Fin )
58 50 57 eqeltrd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> dom ( ( y ( +g ` G ) z ) \ _I ) e. Fin )
59 40 46 58 elrabd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) /\ ( z e. B /\ dom ( z \ _I ) e. Fin ) ) -> ( y ( +g ` G ) z ) e. { x e. B | dom ( x \ _I ) e. Fin } )
60 29 33 37 59 syl3anb 
 |-  ( ( D e. V /\ y e. { x e. B | dom ( x \ _I ) e. Fin } /\ z e. { x e. B | dom ( x \ _I ) e. Fin } ) -> ( y ( +g ` G ) z ) e. { x e. B | dom ( x \ _I ) e. Fin } )
61 difeq1 
 |-  ( x = ( ( invg ` G ) ` y ) -> ( x \ _I ) = ( ( ( invg ` G ) ` y ) \ _I ) )
62 61 dmeqd 
 |-  ( x = ( ( invg ` G ) ` y ) -> dom ( x \ _I ) = dom ( ( ( invg ` G ) ` y ) \ _I ) )
63 62 eleq1d 
 |-  ( x = ( ( invg ` G ) ` y ) -> ( dom ( x \ _I ) e. Fin <-> dom ( ( ( invg ` G ) ` y ) \ _I ) e. Fin ) )
64 simprl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> y e. B )
65 eqid 
 |-  ( invg ` G ) = ( invg ` G )
66 2 65 grpinvcl 
 |-  ( ( G e. Grp /\ y e. B ) -> ( ( invg ` G ) ` y ) e. B )
67 12 64 66 syl2an2r 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> ( ( invg ` G ) ` y ) e. B )
68 1 2 65 symginv 
 |-  ( y e. B -> ( ( invg ` G ) ` y ) = `' y )
69 68 ad2antrl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> ( ( invg ` G ) ` y ) = `' y )
70 69 difeq1d 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> ( ( ( invg ` G ) ` y ) \ _I ) = ( `' y \ _I ) )
71 70 dmeqd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> dom ( ( ( invg ` G ) ` y ) \ _I ) = dom ( `' y \ _I ) )
72 1 2 symgbasf1o 
 |-  ( y e. B -> y : D -1-1-onto-> D )
73 72 ad2antrl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> y : D -1-1-onto-> D )
74 f1omvdcnv 
 |-  ( y : D -1-1-onto-> D -> dom ( `' y \ _I ) = dom ( y \ _I ) )
75 73 74 syl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> dom ( `' y \ _I ) = dom ( y \ _I ) )
76 71 75 eqtrd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> dom ( ( ( invg ` G ) ` y ) \ _I ) = dom ( y \ _I ) )
77 simprr 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> dom ( y \ _I ) e. Fin )
78 76 77 eqeltrd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> dom ( ( ( invg ` G ) ` y ) \ _I ) e. Fin )
79 63 67 78 elrabd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) e. Fin ) ) -> ( ( invg ` G ) ` y ) e. { x e. B | dom ( x \ _I ) e. Fin } )
80 33 79 sylan2b 
 |-  ( ( D e. V /\ y e. { x e. B | dom ( x \ _I ) e. Fin } ) -> ( ( invg ` G ) ` y ) e. { x e. B | dom ( x \ _I ) e. Fin } )
81 3 4 5 8 28 60 80 12 issubgrpd2 
 |-  ( D e. V -> { x e. B | dom ( x \ _I ) e. Fin } e. ( SubGrp ` G ) )