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 ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
cycpmco2.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
cycpmco2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
cycpmco2.w ⊢ ( 𝜑 → 𝑊 ∈ dom 𝑀 )
cycpmco2.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
cycpmco2.j ⊢ ( 𝜑 → 𝐽 ∈ ran 𝑊 )
cycpmco2.e ⊢ 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 )
cycpmco2.1 ⊢ 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
Assertion cycpmco2rn ( 𝜑 → ran 𝑈 = ( ran 𝑊 ∪ { 𝐼 } ) )

Proof

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