Metamath Proof Explorer

Theorem symgsssg

Description: The symmetric group has subgroups restricting the set of non-fixed points. (Contributed by Stefan O'Rear, 24-Aug-2015)

Ref Expression
Hypotheses symgsssg.g 
|- G = ( SymGrp ` D )
symgsssg.b 
|- B = ( Base ` G )
Assertion symgsssg 
|- ( D e. V -> { x e. B | dom ( x \ _I ) C_ X } 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 ) C_ X } ) = ( G |`s { x e. B | dom ( x \ _I ) C_ X } ) )
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 ) C_ X } C_ B
7 6 2 sseqtri 
 |-  { x e. B | dom ( x \ _I ) C_ X } C_ ( Base ` G )
8 7 a1i 
 |-  ( D e. V -> { x e. B | dom ( x \ _I ) C_ X } 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 sseq1d 
 |-  ( x = ( 0g ` G ) -> ( dom ( x \ _I ) C_ X <-> dom ( ( 0g ` G ) \ _I ) C_ X ) )
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 0ss 
 |-  (/) C_ X
26 24 25 eqsstri 
 |-  dom ( ( _I |` D ) \ _I ) C_ X
27 18 26 eqsstrrdi 
 |-  ( D e. V -> dom ( ( 0g ` G ) \ _I ) C_ X )
28 11 15 27 elrabd 
 |-  ( D e. V -> ( 0g ` G ) e. { x e. B | dom ( x \ _I ) C_ X } )
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 sseq1d 
 |-  ( x = y -> ( dom ( x \ _I ) C_ X <-> dom ( y \ _I ) C_ X ) )
33 32 elrab 
 |-  ( y e. { x e. B | dom ( x \ _I ) C_ X } <-> ( y e. B /\ dom ( y \ _I ) C_ X ) )
34 difeq1 
 |-  ( x = z -> ( x \ _I ) = ( z \ _I ) )
35 34 dmeqd 
 |-  ( x = z -> dom ( x \ _I ) = dom ( z \ _I ) )
36 35 sseq1d 
 |-  ( x = z -> ( dom ( x \ _I ) C_ X <-> dom ( z \ _I ) C_ X ) )
37 36 elrab 
 |-  ( z e. { x e. B | dom ( x \ _I ) C_ X } <-> ( z e. B /\ dom ( z \ _I ) C_ X ) )
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 sseq1d 
 |-  ( x = ( y ( +g ` G ) z ) -> ( dom ( x \ _I ) C_ X <-> dom ( ( y ( +g ` G ) z ) \ _I ) C_ X ) )
41 12 3ad2ant1 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> G e. Grp )
42 simp2l 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> y e. B )
43 simp3l 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> 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 ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> ( 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 ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> ( y ( +g ` G ) z ) = ( y o. z ) )
49 48 difeq1d 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> ( ( y ( +g ` G ) z ) \ _I ) = ( ( y o. z ) \ _I ) )
50 49 dmeqd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> dom ( ( y ( +g ` G ) z ) \ _I ) = dom ( ( y o. z ) \ _I ) )
51 mvdco 
 |-  dom ( ( y o. z ) \ _I ) C_ ( dom ( y \ _I ) u. dom ( z \ _I ) )
52 simp2r 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> dom ( y \ _I ) C_ X )
53 simp3r 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> dom ( z \ _I ) C_ X )
54 52 53 unssd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> ( dom ( y \ _I ) u. dom ( z \ _I ) ) C_ X )
55 51 54 sstrid 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> dom ( ( y o. z ) \ _I ) C_ X )
56 50 55 eqsstrd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> dom ( ( y ( +g ` G ) z ) \ _I ) C_ X )
57 40 46 56 elrabd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) /\ ( z e. B /\ dom ( z \ _I ) C_ X ) ) -> ( y ( +g ` G ) z ) e. { x e. B | dom ( x \ _I ) C_ X } )
58 29 33 37 57 syl3anb 
 |-  ( ( D e. V /\ y e. { x e. B | dom ( x \ _I ) C_ X } /\ z e. { x e. B | dom ( x \ _I ) C_ X } ) -> ( y ( +g ` G ) z ) e. { x e. B | dom ( x \ _I ) C_ X } )
59 difeq1 
 |-  ( x = ( ( invg ` G ) ` y ) -> ( x \ _I ) = ( ( ( invg ` G ) ` y ) \ _I ) )
60 59 dmeqd 
 |-  ( x = ( ( invg ` G ) ` y ) -> dom ( x \ _I ) = dom ( ( ( invg ` G ) ` y ) \ _I ) )
61 60 sseq1d 
 |-  ( x = ( ( invg ` G ) ` y ) -> ( dom ( x \ _I ) C_ X <-> dom ( ( ( invg ` G ) ` y ) \ _I ) C_ X ) )
62 simprl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> y e. B )
63 eqid 
 |-  ( invg ` G ) = ( invg ` G )
64 2 63 grpinvcl 
 |-  ( ( G e. Grp /\ y e. B ) -> ( ( invg ` G ) ` y ) e. B )
65 12 62 64 syl2an2r 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> ( ( invg ` G ) ` y ) e. B )
66 1 2 63 symginv 
 |-  ( y e. B -> ( ( invg ` G ) ` y ) = `' y )
67 66 ad2antrl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> ( ( invg ` G ) ` y ) = `' y )
68 67 difeq1d 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> ( ( ( invg ` G ) ` y ) \ _I ) = ( `' y \ _I ) )
69 68 dmeqd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> dom ( ( ( invg ` G ) ` y ) \ _I ) = dom ( `' y \ _I ) )
70 1 2 symgbasf1o 
 |-  ( y e. B -> y : D -1-1-onto-> D )
71 70 ad2antrl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> y : D -1-1-onto-> D )
72 f1omvdcnv 
 |-  ( y : D -1-1-onto-> D -> dom ( `' y \ _I ) = dom ( y \ _I ) )
73 71 72 syl 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> dom ( `' y \ _I ) = dom ( y \ _I ) )
74 69 73 eqtrd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> dom ( ( ( invg ` G ) ` y ) \ _I ) = dom ( y \ _I ) )
75 simprr 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> dom ( y \ _I ) C_ X )
76 74 75 eqsstrd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> dom ( ( ( invg ` G ) ` y ) \ _I ) C_ X )
77 61 65 76 elrabd 
 |-  ( ( D e. V /\ ( y e. B /\ dom ( y \ _I ) C_ X ) ) -> ( ( invg ` G ) ` y ) e. { x e. B | dom ( x \ _I ) C_ X } )
78 33 77 sylan2b 
 |-  ( ( D e. V /\ y e. { x e. B | dom ( x \ _I ) C_ X } ) -> ( ( invg ` G ) ` y ) e. { x e. B | dom ( x \ _I ) C_ X } )
79 3 4 5 8 28 58 78 12 issubgrpd2 
 |-  ( D e. V -> { x e. B | dom ( x \ _I ) C_ X } e. ( SubGrp ` G ) )