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	$⊢ φ \to D \in V$
	cycpmco2.w	$⊢ φ \to W \in dom M$
	cycpmco2.i	$⊢ φ \to I \in (D ∖ ran W)$
	cycpmco2.j	$⊢ φ \to J \in ran W$
	cycpmco2.e	$⊢ E = W^{-1} (J) + 1$
	cycpmco2.1	$⊢ U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
Assertion	cycpmco2rn	$⊢ φ \to ran U = ran W \cup \{I\}$

Proof

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

Metamath Proof Explorer

Theorem cycpmco2rn

Proof