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=BaseG
Assertion symgsssg ⊢D∈V→x∈B|dom⁡x∖I⊆X∈SubGrp⁡G

Proof

Step Hyp Ref Expression
1 symgsssg.g ⊢G=SymGrp⁡D
2 symgsssg.b ⊢B=BaseG
3 eqidd ⊢D∈V→G↾𝑠x∈B|dom⁡x∖I⊆X=G↾𝑠x∈B|dom⁡x∖I⊆X
4 eqidd ⊢D∈V→0G=0G
5 eqidd ⊢D∈V→+G=+G
6 ssrab2 ⊢x∈B|dom⁡x∖I⊆X⊆B
7 6 2 sseqtri ⊢x∈B|dom⁡x∖I⊆X⊆BaseG
8 7 a1i ⊢D∈V→x∈B|dom⁡x∖I⊆X⊆BaseG
9 difeq1 ⊢x=0G→x∖I=0G∖I
10 9 dmeqd ⊢x=0G→dom⁡x∖I=dom⁡0G∖I
11 10 sseq1d ⊢x=0G→dom⁡x∖I⊆X↔dom⁡0G∖I⊆X
12 1 symggrp ⊢D∈V→G∈Grp
13 eqid ⊢0G=0G
14 2 13 grpidcl ⊢G∈Grp→0G∈B
15 12 14 syl ⊢D∈V→0G∈B
16 1 symgid ⊢D∈V→I↾D=0G
17 16 difeq1d ⊢D∈V→I↾D∖I=0G∖I
18 17 dmeqd ⊢D∈V→dom⁡I↾D∖I=dom⁡0G∖I
19 resss ⊢I↾D⊆I
20 ssdif0 ⊢I↾D⊆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 ⊢∅⊆X
26 24 25 eqsstri ⊢dom⁡I↾D∖I⊆X
27 18 26 eqsstrrdi ⊢D∈V→dom⁡0G∖I⊆X
28 11 15 27 elrabd ⊢D∈V→0G∈x∈B|dom⁡x∖I⊆X
29 biid ⊢D∈V↔D∈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⊆X↔dom⁡y∖I⊆X
33 32 elrab ⊢y∈x∈B|dom⁡x∖I⊆X↔y∈B∧dom⁡y∖I⊆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⊆X↔dom⁡z∖I⊆X
37 36 elrab ⊢z∈x∈B|dom⁡x∖I⊆X↔z∈B∧dom⁡z∖I⊆X
38 difeq1 ⊢x=y+Gz→x∖I=y+Gz∖I
39 38 dmeqd ⊢x=y+Gz→dom⁡x∖I=dom⁡y+Gz∖I
40 39 sseq1d ⊢x=y+Gz→dom⁡x∖I⊆X↔dom⁡y+Gz∖I⊆X
41 12 3ad2ant1 ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→G∈Grp
42 simp2l ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→y∈B
43 simp3l ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→z∈B
44 eqid ⊢+G=+G
45 2 44 grpcl ⊢G∈Grp∧y∈B∧z∈B→y+Gz∈B
46 41 42 43 45 syl3anc ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→y+Gz∈B
47 1 2 44 symgov ⊢y∈B∧z∈B→y+Gz=y∘z
48 42 43 47 syl2anc ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→y+Gz=y∘z
49 48 difeq1d ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→y+Gz∖I=y∘z∖I
50 49 dmeqd ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→dom⁡y+Gz∖I=dom⁡y∘z∖I
51 mvdco ⊢dom⁡y∘z∖I⊆dom⁡y∖I∪dom⁡z∖I
52 simp2r ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→dom⁡y∖I⊆X
53 simp3r ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→dom⁡z∖I⊆X
54 52 53 unssd ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→dom⁡y∖I∪dom⁡z∖I⊆X
55 51 54 sstrid ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→dom⁡y∘z∖I⊆X
56 50 55 eqsstrd ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→dom⁡y+Gz∖I⊆X
57 40 46 56 elrabd ⊢D∈V∧y∈B∧dom⁡y∖I⊆X∧z∈B∧dom⁡z∖I⊆X→y+Gz∈x∈B|dom⁡x∖I⊆X
58 29 33 37 57 syl3anb ⊢D∈V∧y∈x∈B|dom⁡x∖I⊆X∧z∈x∈B|dom⁡x∖I⊆X→y+Gz∈x∈B|dom⁡x∖I⊆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⊆X↔dom⁡invg⁡G⁡y∖I⊆X
62 simprl ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→y∈B
63 eqid ⊢invg⁡G=invg⁡G
64 2 63 grpinvcl ⊢G∈Grp∧y∈B→invg⁡G⁡y∈B
65 12 62 64 syl2an2r ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→invg⁡G⁡y∈B
66 1 2 63 symginv ⊢y∈B→invg⁡G⁡y=y-1
67 66 ad2antrl ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→invg⁡G⁡y=y-1
68 67 difeq1d ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→invg⁡G⁡y∖I=y-1∖I
69 68 dmeqd ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→dom⁡invg⁡G⁡y∖I=dom⁡y-1∖I
70 1 2 symgbasf1o ⊢y∈B→y:D⟶1-1 ontoD
71 70 ad2antrl ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→y:D⟶1-1 ontoD
72 f1omvdcnv ⊢y:D⟶1-1 ontoD→dom⁡y-1∖I=dom⁡y∖I
73 71 72 syl ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→dom⁡y-1∖I=dom⁡y∖I
74 69 73 eqtrd ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→dom⁡invg⁡G⁡y∖I=dom⁡y∖I
75 simprr ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→dom⁡y∖I⊆X
76 74 75 eqsstrd ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→dom⁡invg⁡G⁡y∖I⊆X
77 61 65 76 elrabd ⊢D∈V∧y∈B∧dom⁡y∖I⊆X→invg⁡G⁡y∈x∈B|dom⁡x∖I⊆X
78 33 77 sylan2b ⊢D∈V∧y∈x∈B|dom⁡x∖I⊆X→invg⁡G⁡y∈x∈B|dom⁡x∖I⊆X
79 3 4 5 8 28 58 78 12 issubgrpd2 ⊢D∈V→x∈B|dom⁡x∖I⊆X∈SubGrp⁡G