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

Proof

Step Hyp Ref Expression
1 symgsssg.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 symgsssg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 eqidd ⊢ ( 𝐷 ∈ 𝑉 → ( 𝐺 ↾s { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ) = ( 𝐺 ↾s { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ) )
4 eqidd ⊢ ( 𝐷 ∈ 𝑉 → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) )
5 eqidd ⊢ ( 𝐷 ∈ 𝑉 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) )
6 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ⊆ 𝐵
7 6 2 sseqtri ⊢ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ⊆ ( Base ‘ 𝐺 )
8 7 a1i ⊢ ( 𝐷 ∈ 𝑉 → { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ⊆ ( Base ‘ 𝐺 ) )
9 difeq1 ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( 𝑥 ∖ I ) = ( ( 0g ‘ 𝐺 ) ∖ I ) )
10 9 dmeqd ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → dom ( 𝑥 ∖ I ) = dom ( ( 0g ‘ 𝐺 ) ∖ I ) )
11 10 eleq1d ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( dom ( 𝑥 ∖ I ) ∈ Fin ↔ dom ( ( 0g ‘ 𝐺 ) ∖ I ) ∈ Fin ) )
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 0fi ⊢ ∅ ∈ Fin
26 24 25 eqeltri ⊢ dom ( ( I ↾ 𝐷 ) ∖ I ) ∈ Fin
27 18 26 eqeltrrdi ⊢ ( 𝐷 ∈ 𝑉 → dom ( ( 0g ‘ 𝐺 ) ∖ I ) ∈ Fin )
28 11 15 27 elrabd ⊢ ( 𝐷 ∈ 𝑉 → ( 0g ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
29 biid ⊢ ( 𝐷 ∈ 𝑉 ↔ 𝐷 ∈ 𝑉 )
30 difeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∖ I ) = ( 𝑦 ∖ I ) )
31 30 dmeqd ⊢ ( 𝑥 = 𝑦 → dom ( 𝑥 ∖ I ) = dom ( 𝑦 ∖ I ) )
32 31 eleq1d ⊢ ( 𝑥 = 𝑦 → ( dom ( 𝑥 ∖ I ) ∈ Fin ↔ dom ( 𝑦 ∖ I ) ∈ Fin ) )
33 32 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ↔ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) )
34 difeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∖ I ) = ( 𝑧 ∖ I ) )
35 34 dmeqd ⊢ ( 𝑥 = 𝑧 → dom ( 𝑥 ∖ I ) = dom ( 𝑧 ∖ I ) )
36 35 eleq1d ⊢ ( 𝑥 = 𝑧 → ( dom ( 𝑥 ∖ I ) ∈ Fin ↔ dom ( 𝑧 ∖ I ) ∈ Fin ) )
37 36 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ↔ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) )
38 difeq1 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( 𝑥 ∖ I ) = ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∖ I ) )
39 38 dmeqd ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → dom ( 𝑥 ∖ I ) = dom ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∖ I ) )
40 39 eleq1d ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( dom ( 𝑥 ∖ I ) ∈ Fin ↔ dom ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∖ I ) ∈ Fin ) )
41 12 3ad2ant1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → 𝐺 ∈ Grp )
42 simp2l ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → 𝑦 ∈ 𝐵 )
43 simp3l ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → 𝑧 ∈ 𝐵 )
44 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
45 2 44 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝐵 )
46 41 42 43 45 syl3anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝐵 )
47 1 2 44 symgov ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ∘ 𝑧 ) )
48 42 43 47 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ∘ 𝑧 ) )
49 48 difeq1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∖ I ) = ( ( 𝑦 ∘ 𝑧 ) ∖ I ) )
50 49 dmeqd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → dom ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∖ I ) = dom ( ( 𝑦 ∘ 𝑧 ) ∖ I ) )
51 simp2r ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → dom ( 𝑦 ∖ I ) ∈ Fin )
52 simp3r ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → dom ( 𝑧 ∖ I ) ∈ Fin )
53 unfi ⊢ ( ( dom ( 𝑦 ∖ I ) ∈ Fin ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) → ( dom ( 𝑦 ∖ I ) ∪ dom ( 𝑧 ∖ I ) ) ∈ Fin )
54 51 52 53 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → ( dom ( 𝑦 ∖ I ) ∪ dom ( 𝑧 ∖ I ) ) ∈ Fin )
55 mvdco ⊢ dom ( ( 𝑦 ∘ 𝑧 ) ∖ I ) ⊆ ( dom ( 𝑦 ∖ I ) ∪ dom ( 𝑧 ∖ I ) )
56 ssfi ⊢ ( ( ( dom ( 𝑦 ∖ I ) ∪ dom ( 𝑧 ∖ I ) ) ∈ Fin ∧ dom ( ( 𝑦 ∘ 𝑧 ) ∖ I ) ⊆ ( dom ( 𝑦 ∖ I ) ∪ dom ( 𝑧 ∖ I ) ) ) → dom ( ( 𝑦 ∘ 𝑧 ) ∖ I ) ∈ Fin )
57 54 55 56 sylancl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → dom ( ( 𝑦 ∘ 𝑧 ) ∖ I ) ∈ Fin )
58 50 57 eqeltrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → dom ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∖ I ) ∈ Fin )
59 40 46 58 elrabd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ∧ ( 𝑧 ∈ 𝐵 ∧ dom ( 𝑧 ∖ I ) ∈ Fin ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
60 29 33 37 59 syl3anb ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ∧ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
61 difeq1 ⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( 𝑥 ∖ I ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∖ I ) )
62 61 dmeqd ⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → dom ( 𝑥 ∖ I ) = dom ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∖ I ) )
63 62 eleq1d ⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( dom ( 𝑥 ∖ I ) ∈ Fin ↔ dom ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∖ I ) ∈ Fin ) )
64 simprl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → 𝑦 ∈ 𝐵 )
65 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
66 2 65 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
67 12 64 66 syl2an2r ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
68 1 2 65 symginv ⊢ ( 𝑦 ∈ 𝐵 → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) = ◡ 𝑦 )
69 68 ad2antrl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) = ◡ 𝑦 )
70 69 difeq1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∖ I ) = ( ◡ 𝑦 ∖ I ) )
71 70 dmeqd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → dom ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∖ I ) = dom ( ◡ 𝑦 ∖ I ) )
72 1 2 symgbasf1o ⊢ ( 𝑦 ∈ 𝐵 → 𝑦 : 𝐷 –1-1-onto→ 𝐷 )
73 72 ad2antrl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → 𝑦 : 𝐷 –1-1-onto→ 𝐷 )
74 f1omvdcnv ⊢ ( 𝑦 : 𝐷 –1-1-onto→ 𝐷 → dom ( ◡ 𝑦 ∖ I ) = dom ( 𝑦 ∖ I ) )
75 73 74 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → dom ( ◡ 𝑦 ∖ I ) = dom ( 𝑦 ∖ I ) )
76 71 75 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → dom ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∖ I ) = dom ( 𝑦 ∖ I ) )
77 simprr ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → dom ( 𝑦 ∖ I ) ∈ Fin )
78 76 77 eqeltrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → dom ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∖ I ) ∈ Fin )
79 63 67 78 elrabd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐵 ∧ dom ( 𝑦 ∖ I ) ∈ Fin ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
80 33 79 sylan2b ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
81 3 4 5 8 28 60 80 12 issubgrpd2 ⊢ ( 𝐷 ∈ 𝑉 → { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ∈ ( SubGrp ‘ 𝐺 ) )