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 𝐺 = ( SymGrp ‘ 𝐷 )
symgsssg.b 𝐵 = ( Base ‘ 𝐺 )
Assertion symgsssg ( 𝐷𝑉 → { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 symgsssg.g 𝐺 = ( SymGrp ‘ 𝐷 )
2 symgsssg.b 𝐵 = ( Base ‘ 𝐺 )
3 eqidd ( 𝐷𝑉 → ( 𝐺s { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ) = ( 𝐺s { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ) )
4 eqidd ( 𝐷𝑉 → ( 0g𝐺 ) = ( 0g𝐺 ) )
5 eqidd ( 𝐷𝑉 → ( +g𝐺 ) = ( +g𝐺 ) )
6 ssrab2 { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ⊆ 𝐵
7 6 2 sseqtri { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ⊆ ( Base ‘ 𝐺 )
8 7 a1i ( 𝐷𝑉 → { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ⊆ ( Base ‘ 𝐺 ) )
9 difeq1 ( 𝑥 = ( 0g𝐺 ) → ( 𝑥 ∖ I ) = ( ( 0g𝐺 ) ∖ I ) )
10 9 dmeqd ( 𝑥 = ( 0g𝐺 ) → dom ( 𝑥 ∖ I ) = dom ( ( 0g𝐺 ) ∖ I ) )
11 10 sseq1d ( 𝑥 = ( 0g𝐺 ) → ( dom ( 𝑥 ∖ I ) ⊆ 𝑋 ↔ dom ( ( 0g𝐺 ) ∖ I ) ⊆ 𝑋 ) )
12 1 symggrp ( 𝐷𝑉𝐺 ∈ Grp )
13 eqid ( 0g𝐺 ) = ( 0g𝐺 )
14 2 13 grpidcl ( 𝐺 ∈ Grp → ( 0g𝐺 ) ∈ 𝐵 )
15 12 14 syl ( 𝐷𝑉 → ( 0g𝐺 ) ∈ 𝐵 )
16 1 symgid ( 𝐷𝑉 → ( I ↾ 𝐷 ) = ( 0g𝐺 ) )
17 16 difeq1d ( 𝐷𝑉 → ( ( I ↾ 𝐷 ) ∖ I ) = ( ( 0g𝐺 ) ∖ I ) )
18 17 dmeqd ( 𝐷𝑉 → dom ( ( I ↾ 𝐷 ) ∖ I ) = dom ( ( 0g𝐺 ) ∖ I ) )
19 resss ( I ↾ 𝐷 ) ⊆ I
20 ssdif0 ( ( I ↾ 𝐷 ) ⊆ I ↔ ( ( I ↾ 𝐷 ) ∖ I ) = ∅ )
21 19 20 mpbi ( ( I ↾ 𝐷 ) ∖ I ) = ∅
22 21 dmeqi dom ( ( I ↾ 𝐷 ) ∖ I ) = dom ∅
23 dm0 dom ∅ = ∅
24 22 23 eqtri dom ( ( I ↾ 𝐷 ) ∖ I ) = ∅
25 0ss ∅ ⊆ 𝑋
26 24 25 eqsstri dom ( ( I ↾ 𝐷 ) ∖ I ) ⊆ 𝑋
27 18 26 eqsstrrdi ( 𝐷𝑉 → dom ( ( 0g𝐺 ) ∖ I ) ⊆ 𝑋 )
28 11 15 27 elrabd ( 𝐷𝑉 → ( 0g𝐺 ) ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } )
29 biid ( 𝐷𝑉𝐷𝑉 )
30 difeq1 ( 𝑥 = 𝑦 → ( 𝑥 ∖ I ) = ( 𝑦 ∖ I ) )
31 30 dmeqd ( 𝑥 = 𝑦 → dom ( 𝑥 ∖ I ) = dom ( 𝑦 ∖ I ) )
32 31 sseq1d ( 𝑥 = 𝑦 → ( dom ( 𝑥 ∖ I ) ⊆ 𝑋 ↔ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) )
33 32 elrab ( 𝑦 ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ↔ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) )
34 difeq1 ( 𝑥 = 𝑧 → ( 𝑥 ∖ I ) = ( 𝑧 ∖ I ) )
35 34 dmeqd ( 𝑥 = 𝑧 → dom ( 𝑥 ∖ I ) = dom ( 𝑧 ∖ I ) )
36 35 sseq1d ( 𝑥 = 𝑧 → ( dom ( 𝑥 ∖ I ) ⊆ 𝑋 ↔ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) )
37 36 elrab ( 𝑧 ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ↔ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) )
38 difeq1 ( 𝑥 = ( 𝑦 ( +g𝐺 ) 𝑧 ) → ( 𝑥 ∖ I ) = ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ∖ I ) )
39 38 dmeqd ( 𝑥 = ( 𝑦 ( +g𝐺 ) 𝑧 ) → dom ( 𝑥 ∖ I ) = dom ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ∖ I ) )
40 39 sseq1d ( 𝑥 = ( 𝑦 ( +g𝐺 ) 𝑧 ) → ( dom ( 𝑥 ∖ I ) ⊆ 𝑋 ↔ dom ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ∖ I ) ⊆ 𝑋 ) )
41 12 3ad2ant1 ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → 𝐺 ∈ Grp )
42 simp2l ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → 𝑦𝐵 )
43 simp3l ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → 𝑧𝐵 )
44 eqid ( +g𝐺 ) = ( +g𝐺 )
45 2 44 grpcl ( ( 𝐺 ∈ Grp ∧ 𝑦𝐵𝑧𝐵 ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) ∈ 𝐵 )
46 41 42 43 45 syl3anc ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) ∈ 𝐵 )
47 1 2 44 symgov ( ( 𝑦𝐵𝑧𝐵 ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) = ( 𝑦𝑧 ) )
48 42 43 47 syl2anc ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) = ( 𝑦𝑧 ) )
49 48 difeq1d ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ∖ I ) = ( ( 𝑦𝑧 ) ∖ I ) )
50 49 dmeqd ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → dom ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ∖ I ) = dom ( ( 𝑦𝑧 ) ∖ I ) )
51 mvdco dom ( ( 𝑦𝑧 ) ∖ I ) ⊆ ( dom ( 𝑦 ∖ I ) ∪ dom ( 𝑧 ∖ I ) )
52 simp2r ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → dom ( 𝑦 ∖ I ) ⊆ 𝑋 )
53 simp3r ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → dom ( 𝑧 ∖ I ) ⊆ 𝑋 )
54 52 53 unssd ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → ( dom ( 𝑦 ∖ I ) ∪ dom ( 𝑧 ∖ I ) ) ⊆ 𝑋 )
55 51 54 sstrid ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → dom ( ( 𝑦𝑧 ) ∖ I ) ⊆ 𝑋 )
56 50 55 eqsstrd ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → dom ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ∖ I ) ⊆ 𝑋 )
57 40 46 56 elrabd ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ∧ ( 𝑧𝐵 ∧ dom ( 𝑧 ∖ I ) ⊆ 𝑋 ) ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } )
58 29 33 37 57 syl3anb ( ( 𝐷𝑉𝑦 ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ∧ 𝑧 ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } )
59 difeq1 ( 𝑥 = ( ( invg𝐺 ) ‘ 𝑦 ) → ( 𝑥 ∖ I ) = ( ( ( invg𝐺 ) ‘ 𝑦 ) ∖ I ) )
60 59 dmeqd ( 𝑥 = ( ( invg𝐺 ) ‘ 𝑦 ) → dom ( 𝑥 ∖ I ) = dom ( ( ( invg𝐺 ) ‘ 𝑦 ) ∖ I ) )
61 60 sseq1d ( 𝑥 = ( ( invg𝐺 ) ‘ 𝑦 ) → ( dom ( 𝑥 ∖ I ) ⊆ 𝑋 ↔ dom ( ( ( invg𝐺 ) ‘ 𝑦 ) ∖ I ) ⊆ 𝑋 ) )
62 simprl ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → 𝑦𝐵 )
63 eqid ( invg𝐺 ) = ( invg𝐺 )
64 2 63 grpinvcl ( ( 𝐺 ∈ Grp ∧ 𝑦𝐵 ) → ( ( invg𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
65 12 62 64 syl2an2r ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → ( ( invg𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
66 1 2 63 symginv ( 𝑦𝐵 → ( ( invg𝐺 ) ‘ 𝑦 ) = 𝑦 )
67 66 ad2antrl ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → ( ( invg𝐺 ) ‘ 𝑦 ) = 𝑦 )
68 67 difeq1d ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → ( ( ( invg𝐺 ) ‘ 𝑦 ) ∖ I ) = ( 𝑦 ∖ I ) )
69 68 dmeqd ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → dom ( ( ( invg𝐺 ) ‘ 𝑦 ) ∖ I ) = dom ( 𝑦 ∖ I ) )
70 1 2 symgbasf1o ( 𝑦𝐵𝑦 : 𝐷1-1-onto𝐷 )
71 70 ad2antrl ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → 𝑦 : 𝐷1-1-onto𝐷 )
72 f1omvdcnv ( 𝑦 : 𝐷1-1-onto𝐷 → dom ( 𝑦 ∖ I ) = dom ( 𝑦 ∖ I ) )
73 71 72 syl ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → dom ( 𝑦 ∖ I ) = dom ( 𝑦 ∖ I ) )
74 69 73 eqtrd ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → dom ( ( ( invg𝐺 ) ‘ 𝑦 ) ∖ I ) = dom ( 𝑦 ∖ I ) )
75 simprr ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → dom ( 𝑦 ∖ I ) ⊆ 𝑋 )
76 74 75 eqsstrd ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → dom ( ( ( invg𝐺 ) ‘ 𝑦 ) ∖ I ) ⊆ 𝑋 )
77 61 65 76 elrabd ( ( 𝐷𝑉 ∧ ( 𝑦𝐵 ∧ dom ( 𝑦 ∖ I ) ⊆ 𝑋 ) ) → ( ( invg𝐺 ) ‘ 𝑦 ) ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } )
78 33 77 sylan2b ( ( 𝐷𝑉𝑦 ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ) → ( ( invg𝐺 ) ‘ 𝑦 ) ∈ { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } )
79 3 4 5 8 28 58 78 12 issubgrpd2 ( 𝐷𝑉 → { 𝑥𝐵 ∣ dom ( 𝑥 ∖ I ) ⊆ 𝑋 } ∈ ( SubGrp ‘ 𝐺 ) )