Metamath Proof Explorer

Theorem cycpmco2rn

Description: The orbit of the composition of a cyclic permutation and a well-chosen transposition is one element more than the orbit of the original permutation. (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c ⊢ M = toCyc ⁡ D
cycpmco2.s ⊢ S = SymGrp ⁡ D
cycpmco2.d ⊢ φ → D ∈ V
cycpmco2.w ⊢ φ → W ∈ dom ⁡ M
cycpmco2.i ⊢ φ → I ∈ D ∖ ran ⁡ W
cycpmco2.j ⊢ φ → J ∈ ran ⁡ W
cycpmco2.e ⊢ E = W -1 ⁡ J + 1
cycpmco2.1 ⊢ U = W splice E E ⟨“ I ”⟩
Assertion cycpmco2rn ⊢ φ → ran ⁡ U = ran ⁡ W ∪ I

Proof

Step Hyp Ref Expression
1 cycpmco2.c ⊢ M = toCyc ⁡ D
2 cycpmco2.s ⊢ S = SymGrp ⁡ D
3 cycpmco2.d ⊢ φ → D ∈ V
4 cycpmco2.w ⊢ φ → W ∈ dom ⁡ M
5 cycpmco2.i ⊢ φ → I ∈ D ∖ ran ⁡ W
6 cycpmco2.j ⊢ φ → J ∈ ran ⁡ W
7 cycpmco2.e ⊢ E = W -1 ⁡ J + 1
8 cycpmco2.1 ⊢ U = W splice E E ⟨“ I ”⟩
9 un23 ⊢ W 0 ..^ E ∪ I ∪ W E ..^ W = W 0 ..^ E ∪ W E ..^ W ∪ I
10 ovexd ⊢ φ → W -1 ⁡ J + 1 ∈ V
11 7 10 eqeltrid ⊢ φ → E ∈ V
12 5 eldifad ⊢ φ → I ∈ D
13 12 s1cld ⊢ φ → ⟨“ I ”⟩ ∈ Word D
14 splval ⊢ W ∈ dom ⁡ M ∧ E ∈ V ∧ E ∈ V ∧ ⟨“ I ”⟩ ∈ Word D → W splice E E ⟨“ I ”⟩ = W prefix E ++ ⟨“ I ”⟩ ++ W substr E W
15 4 11 11 13 14 syl13anc ⊢ φ → W splice E E ⟨“ I ”⟩ = W prefix E ++ ⟨“ I ”⟩ ++ W substr E W
16 8 15 syl5eq ⊢ φ → U = W prefix E ++ ⟨“ I ”⟩ ++ W substr E W
17 16 rneqd ⊢ φ → ran ⁡ U = ran ⁡ W prefix E ++ ⟨“ I ”⟩ ++ W substr E W
18 ssrab2 ⊢ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⊆ Word D
19 eqid ⊢ Base S = Base S
20 1 2 19 tocycf ⊢ D ∈ V → M : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ Base S
21 3 20 syl ⊢ φ → M : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ Base S
22 21 fdmd ⊢ φ → dom ⁡ M = w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D
23 4 22 eleqtrd ⊢ φ → W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D
24 18 23 sseldi ⊢ φ → W ∈ Word D
25 pfxcl ⊢ W ∈ Word D → W prefix E ∈ Word D
26 24 25 syl ⊢ φ → W prefix E ∈ Word D
27 ccatcl ⊢ W prefix E ∈ Word D ∧ ⟨“ I ”⟩ ∈ Word D → W prefix E ++ ⟨“ I ”⟩ ∈ Word D
28 26 13 27 syl2anc ⊢ φ → W prefix E ++ ⟨“ I ”⟩ ∈ Word D
29 swrdcl ⊢ W ∈ Word D → W substr E W ∈ Word D
30 24 29 syl ⊢ φ → W substr E W ∈ Word D
31 ccatrn ⊢ W prefix E ++ ⟨“ I ”⟩ ∈ Word D ∧ W substr E W ∈ Word D → ran ⁡ W prefix E ++ ⟨“ I ”⟩ ++ W substr E W = ran ⁡ W prefix E ++ ⟨“ I ”⟩ ∪ ran ⁡ W substr E W
32 28 30 31 syl2anc ⊢ φ → ran ⁡ W prefix E ++ ⟨“ I ”⟩ ++ W substr E W = ran ⁡ W prefix E ++ ⟨“ I ”⟩ ∪ ran ⁡ W substr E W
33 ccatrn ⊢ W prefix E ∈ Word D ∧ ⟨“ I ”⟩ ∈ Word D → ran ⁡ W prefix E ++ ⟨“ I ”⟩ = ran ⁡ W prefix E ∪ ran ⁡ ⟨“ I ”⟩
34 26 13 33 syl2anc ⊢ φ → ran ⁡ W prefix E ++ ⟨“ I ”⟩ = ran ⁡ W prefix E ∪ ran ⁡ ⟨“ I ”⟩
35 id ⊢ w = W → w = W
36 dmeq ⊢ w = W → dom ⁡ w = dom ⁡ W
37 eqidd ⊢ w = W → D = D
38 35 36 37 f1eq123d ⊢ w = W → w : dom ⁡ w ⟶ 1-1 D ↔ W : dom ⁡ W ⟶ 1-1 D
39 38 elrab ⊢ W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ↔ W ∈ Word D ∧ W : dom ⁡ W ⟶ 1-1 D
40 23 39 sylib ⊢ φ → W ∈ Word D ∧ W : dom ⁡ W ⟶ 1-1 D
41 40 simprd ⊢ φ → W : dom ⁡ W ⟶ 1-1 D
42 f1cnv ⊢ W : dom ⁡ W ⟶ 1-1 D → W -1 : ran ⁡ W ⟶ 1-1 onto dom ⁡ W
43 f1of ⊢ W -1 : ran ⁡ W ⟶ 1-1 onto dom ⁡ W → W -1 : ran ⁡ W ⟶ dom ⁡ W
44 41 42 43 3syl ⊢ φ → W -1 : ran ⁡ W ⟶ dom ⁡ W
45 44 6 ffvelrnd ⊢ φ → W -1 ⁡ J ∈ dom ⁡ W
46 wrddm ⊢ W ∈ Word D → dom ⁡ W = 0 ..^ W
47 24 46 syl ⊢ φ → dom ⁡ W = 0 ..^ W
48 45 47 eleqtrd ⊢ φ → W -1 ⁡ J ∈ 0 ..^ W
49 fzofzp1 ⊢ W -1 ⁡ J ∈ 0 ..^ W → W -1 ⁡ J + 1 ∈ 0 … W
50 48 49 syl ⊢ φ → W -1 ⁡ J + 1 ∈ 0 … W
51 7 50 eqeltrid ⊢ φ → E ∈ 0 … W
52 pfxrn3 ⊢ W ∈ Word D ∧ E ∈ 0 … W → ran ⁡ W prefix E = W 0 ..^ E
53 24 51 52 syl2anc ⊢ φ → ran ⁡ W prefix E = W 0 ..^ E
54 s1rn ⊢ I ∈ D → ran ⁡ ⟨“ I ”⟩ = I
55 12 54 syl ⊢ φ → ran ⁡ ⟨“ I ”⟩ = I
56 53 55 uneq12d ⊢ φ → ran ⁡ W prefix E ∪ ran ⁡ ⟨“ I ”⟩ = W 0 ..^ E ∪ I
57 34 56 eqtrd ⊢ φ → ran ⁡ W prefix E ++ ⟨“ I ”⟩ = W 0 ..^ E ∪ I
58 lencl ⊢ W ∈ Word D → W ∈ ℕ 0
59 nn0fz0 ⊢ W ∈ ℕ 0 ↔ W ∈ 0 … W
60 59 biimpi ⊢ W ∈ ℕ 0 → W ∈ 0 … W
61 24 58 60 3syl ⊢ φ → W ∈ 0 … W
62 swrdrn3 ⊢ W ∈ Word D ∧ E ∈ 0 … W ∧ W ∈ 0 … W → ran ⁡ W substr E W = W E ..^ W
63 24 51 61 62 syl3anc ⊢ φ → ran ⁡ W substr E W = W E ..^ W
64 57 63 uneq12d ⊢ φ → ran ⁡ W prefix E ++ ⟨“ I ”⟩ ∪ ran ⁡ W substr E W = W 0 ..^ E ∪ I ∪ W E ..^ W
65 17 32 64 3eqtrd ⊢ φ → ran ⁡ U = W 0 ..^ E ∪ I ∪ W E ..^ W
66 fzosplit ⊢ E ∈ 0 … W → 0 ..^ W = 0 ..^ E ∪ E ..^ W
67 51 66 syl ⊢ φ → 0 ..^ W = 0 ..^ E ∪ E ..^ W
68 67 imaeq2d ⊢ φ → W 0 ..^ W = W 0 ..^ E ∪ E ..^ W
69 wrdf ⊢ W ∈ Word D → W : 0 ..^ W ⟶ D
70 24 69 syl ⊢ φ → W : 0 ..^ W ⟶ D
71 70 ffnd ⊢ φ → W Fn 0 ..^ W
72 fnima ⊢ W Fn 0 ..^ W → W 0 ..^ W = ran ⁡ W
73 71 72 syl ⊢ φ → W 0 ..^ W = ran ⁡ W
74 elfzuz3 ⊢ E ∈ 0 … W → W ∈ ℤ ≥ E
75 fzoss2 ⊢ W ∈ ℤ ≥ E → 0 ..^ E ⊆ 0 ..^ W
76 51 74 75 3syl ⊢ φ → 0 ..^ E ⊆ 0 ..^ W
77 fz0ssnn0 ⊢ 0 … W ⊆ ℕ 0
78 77 51 sseldi ⊢ φ → E ∈ ℕ 0
79 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
80 78 79 eleqtrdi ⊢ φ → E ∈ ℤ ≥ 0
81 fzoss1 ⊢ E ∈ ℤ ≥ 0 → E ..^ W ⊆ 0 ..^ W
82 80 81 syl ⊢ φ → E ..^ W ⊆ 0 ..^ W
83 unima ⊢ W Fn 0 ..^ W ∧ 0 ..^ E ⊆ 0 ..^ W ∧ E ..^ W ⊆ 0 ..^ W → W 0 ..^ E ∪ E ..^ W = W 0 ..^ E ∪ W E ..^ W
84 71 76 82 83 syl3anc ⊢ φ → W 0 ..^ E ∪ E ..^ W = W 0 ..^ E ∪ W E ..^ W
85 68 73 84 3eqtr3d ⊢ φ → ran ⁡ W = W 0 ..^ E ∪ W E ..^ W
86 85 uneq1d ⊢ φ → ran ⁡ W ∪ I = W 0 ..^ E ∪ W E ..^ W ∪ I
87 9 65 86 3eqtr4a ⊢ φ → ran ⁡ U = ran ⁡ W ∪ I