cycpmconjslem2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cycpmconjslem2		Structured version Visualization version GIF version

Theorem cycpmconjslem2 33239

Description: Lemma for cycpmconjs 33240. (Contributed by Thierry Arnoux, 14-Oct-2023.)

**Hypotheses**
Ref	Expression
cycpmconjs.c	⊢ 𝐶 = (𝑀 “ (^◡♯ “ {𝑃}))
cycpmconjs.s	⊢ 𝑆 = (SymGrp‘𝐷)
cycpmconjs.n	⊢ 𝑁 = (♯‘𝐷)
cycpmconjs.m	⊢ 𝑀 = (toCyc‘𝐷)
cycpmconjs.b	⊢ 𝐵 = (Base‘𝑆)
cycpmconjs.a	⊢ + = (+_g‘𝑆)
cycpmconjs.l	⊢ − = (-_g‘𝑆)
cycpmconjs.p	⊢ (𝜑 → 𝑃 ∈ (0...𝑁))
cycpmconjs.d	⊢ (𝜑 → 𝐷 ∈ Fin)
cycpmconjs.q	⊢ (𝜑 → 𝑄 ∈ 𝐶)

**Assertion**
Ref	Expression
cycpmconjslem2	⊢ (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))

Distinct variable groups: + ,𝑞 𝐷,𝑞 𝑀,𝑞 𝑁,𝑞 𝑃,𝑞 𝑄,𝑞 Allowed substitution hints: 𝜑(𝑞) 𝐵(𝑞) 𝐶(𝑞) 𝑆(𝑞) − (𝑞)

Proof of Theorem cycpmconjslem2 Dummy variables 𝑓 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzofi 13930	. . . . 5 ⊢ (0..^𝑁) ∈ Fin
2		diffi 9102	. . . . 5 ⊢ ((0..^𝑁) ∈ Fin → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
3	1, 2	mp1i 13	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
4		cycpmconjs.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ Fin)
5		diffi 9102	. . . . . 6 ⊢ (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ Fin)
6	4, 5	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ Fin)
7	6	ad2antrr 728	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (𝐷 ∖ ran 𝑢) ∈ Fin)
8		cycpmconjs.n	. . . . . . . . . 10 ⊢ 𝑁 = (♯‘𝐷)
9		hashcl 14312	. . . . . . . . . . 11 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
10	4, 9	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
11	8, 10	eqeltrid 2840	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
12		hashfzo0 14386	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0..^𝑁)) = 𝑁)
13	11, 12	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0..^𝑁)) = 𝑁)
14	13, 8	eqtrdi 2787	. . . . . . 7 ⊢ (𝜑 → (♯‘(0..^𝑁)) = (♯‘𝐷))
15	14	ad2antrr 728	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(0..^𝑁)) = (♯‘𝐷))
16		simplr 770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃})))
17	16	elin1d 4136	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
18		elrabi 3628	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢 ∈ Word 𝐷)
19		wrdfin 14488	. . . . . . . . 9 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 ∈ Fin)
20	17, 18, 19	3syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ Fin)
21		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
22		dmeq 5848	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
23		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
24	21, 22, 23	f1eq123d 6762	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
25	24	elrab 3632	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷))
26	25	simprbi 498	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢:dom 𝑢–1-1→𝐷)
27	17, 26	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢:dom 𝑢–1-1→𝐷)
28		f1fun 6728	. . . . . . . . 9 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → Fun 𝑢)
29	27, 28	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → Fun 𝑢)
30		hashfun 14393	. . . . . . . . 9 ⊢ (𝑢 ∈ Fin → (Fun 𝑢 ↔ (♯‘𝑢) = (♯‘dom 𝑢)))
31	30	biimpa 477	. . . . . . . 8 ⊢ ((𝑢 ∈ Fin ∧ Fun 𝑢) → (♯‘𝑢) = (♯‘dom 𝑢))
32	20, 29, 31	syl2anc 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = (♯‘dom 𝑢))
33	16	dmexd 7846	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ∈ V)
34		hashf1rn 14308	. . . . . . . 8 ⊢ ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
35	33, 27, 34	syl2anc 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = (♯‘ran 𝑢))
36	32, 35	eqtr3d 2773	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘dom 𝑢) = (♯‘ran 𝑢))
37	15, 36	oveq12d 7377	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
38	1	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^𝑁) ∈ Fin)
39		wrddm 14477	. . . . . . . 8 ⊢ (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
40	17, 18, 39	3syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^(♯‘𝑢)))
41		hashcl 14312	. . . . . . . . . . 11 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
42	17, 18, 19, 41	4syl 19	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℕ₀)
43	42	nn0zd 12543	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℤ)
44	10	nn0zd 12543	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐷) ∈ ℤ)
45	8, 44	eqeltrid 2840	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
46	45	ad2antrr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ ℤ)
47	4	ad2antrr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝐷 ∈ Fin)
48		wrdf 14474	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢:(0..^(♯‘𝑢))⟶𝐷)
49	48	frnd 6666	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → ran 𝑢 ⊆ 𝐷)
50	17, 18, 49	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ran 𝑢 ⊆ 𝐷)
51		hashss 14365	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
52	47, 50, 51	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
53	8	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 = (♯‘𝐷))
54	52, 35, 53	3brtr4d 5107	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ≤ 𝑁)
55		eluz1 12786	. . . . . . . . . 10 ⊢ ((♯‘𝑢) ∈ ℤ → (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) ↔ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)))
56	55	biimpar 478	. . . . . . . . 9 ⊢ (((♯‘𝑢) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
57	43, 46, 54, 56	syl12anc 838	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
58		fzoss2 13636	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
59	57, 58	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
60	40, 59	eqsstrd 3952	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ⊆ (0..^𝑁))
61		hashssdif 14368	. . . . . 6 ⊢ (((0..^𝑁) ∈ Fin ∧ dom 𝑢 ⊆ (0..^𝑁)) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
62	38, 60, 61	syl2anc 586	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
63		hashssdif 14368	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
64	47, 50, 63	syl2anc 586	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
65	37, 62, 64	3eqtr4d 2781	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)))
66		hasheqf1o 14305	. . . . 5 ⊢ ((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) → ((♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)) ↔ ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)))
67	66	biimpa 477	. . . 4 ⊢ (((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) ∧ (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
68	3, 7, 65, 67	syl21anc 839	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
69	27	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢–1-1→𝐷)
70		f1f1orn 6781	. . . . . . 7 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → 𝑢:dom 𝑢–1-1-onto→ran 𝑢)
71	69, 70	syl 17	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢–1-1-onto→ran 𝑢)
72		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
73		disjdif 4403	. . . . . . 7 ⊢ (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅
74	73	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
75		disjdif 4403	. . . . . . 7 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
76	75	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
77		f1oun 6789	. . . . . 6 ⊢ (((𝑢:dom 𝑢–1-1-onto→ran 𝑢 ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) ∧ ((dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅ ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)) → (𝑢 ∪ 𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
78	71, 72, 74, 76, 77	syl22anc 840	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
79		eqidd 2737	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓) = (𝑢 ∪ 𝑓))
80	60	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 ⊆ (0..^𝑁))
81		undif 4413	. . . . . . 7 ⊢ (dom 𝑢 ⊆ (0..^𝑁) ↔ (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
82	80, 81	sylib 219	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
83		undif 4413	. . . . . . . 8 ⊢ (ran 𝑢 ⊆ 𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
84	50, 83	sylib 219	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
85	84	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
86	79, 82, 85	f1oeq123d 6764	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) ↔ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷))
87	78, 86	mpbid 233	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷)
88		f1ocnv 6782	. . . . . . . . . 10 ⊢ ((𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷 → ^◡(𝑢 ∪ 𝑓):𝐷–1-1-onto→(0..^𝑁))
89	87, 88	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡(𝑢 ∪ 𝑓):𝐷–1-1-onto→(0..^𝑁))
90		cycpmconjs.p	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ (0...𝑁))
91		cycpmconjs.c	. . . . . . . . . . . . . 14 ⊢ 𝐶 = (𝑀 “ (^◡♯ “ {𝑃}))
92		cycpmconjs.s	. . . . . . . . . . . . . 14 ⊢ 𝑆 = (SymGrp‘𝐷)
93		cycpmconjs.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (toCyc‘𝐷)
94		cycpmconjs.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝑆)
95	91, 92, 8, 93, 94	cycpmgcl 33237	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑃 ∈ (0...𝑁)) → 𝐶 ⊆ 𝐵)
96	4, 90, 95	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
97		cycpmconjs.q	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ 𝐶)
98	96, 97	sseldd 3919	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ 𝐵)
99	92, 94	symgbasf1o 19344	. . . . . . . . . . 11 ⊢ (𝑄 ∈ 𝐵 → 𝑄:𝐷–1-1-onto→𝐷)
100	98, 99	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
101	100	ad3antrrr 732	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑄:𝐷–1-1-onto→𝐷)
102		f1oco 6793	. . . . . . . . 9 ⊢ ((^◡(𝑢 ∪ 𝑓):𝐷–1-1-onto→(0..^𝑁) ∧ 𝑄:𝐷–1-1-onto→𝐷) → (^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁))
103	89, 101, 102	syl2anc 586	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁))
104		f1oco 6793	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁) ∧ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
105	103, 87, 104	syl2anc 586	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
106		f1ofun 6772	. . . . . . 7 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
107		funrel 6505	. . . . . . 7 ⊢ (Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
108	105, 106, 107	3syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
109		f1odm 6774	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = (0..^𝑁))
110	105, 109	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = (0..^𝑁))
111		fzosplit 13641	. . . . . . . . 9 ⊢ (𝑃 ∈ (0...𝑁) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
112	90, 111	syl 17	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
113	112	ad3antrrr 732	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
114	110, 113	eqtrd 2771	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
115		fzodisj 13642	. . . . . . 7 ⊢ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅
116		reldisjun 5987	. . . . . . 7 ⊢ ((Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ∧ dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)) ∧ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
117	115, 116	mp3an3 1454	. . . . . 6 ⊢ ((Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ∧ dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁))) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
118	108, 114, 117	syl2anc 586	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
119		resco 6204	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)))
120	119	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃))))
121	17, 18	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ Word 𝐷)
122		wrdfn 14484	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 Fn (0..^(♯‘𝑢)))
123	121, 122	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 Fn (0..^(♯‘𝑢)))
124	16	elin2d 4137	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ (^◡♯ “ {𝑃}))
125		hashf 14294	. . . . . . . . . . . . . . . 16 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
126		ffn 6658	. . . . . . . . . . . . . . . 16 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
127		fniniseg 7004	. . . . . . . . . . . . . . . 16 ⊢ (♯ Fn V → (𝑢 ∈ (^◡♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃)))
128	125, 126, 127	mp2b 10	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (^◡♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃))
129	128	simprbi 498	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (^◡♯ “ {𝑃}) → (♯‘𝑢) = 𝑃)
130	124, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = 𝑃)
131	130	oveq2d 7375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) = (0..^𝑃))
132	131	fneq2d 6582	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (𝑢 Fn (0..^(♯‘𝑢)) ↔ 𝑢 Fn (0..^𝑃)))
133	123, 132	mpbid 233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 Fn (0..^𝑃))
134	133	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 Fn (0..^𝑃))
135		f1ofn 6771	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢))
136	72, 135	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢))
137	40, 131	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^𝑃))
138	137	ineq1d 4151	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)))
139	73	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
140	138, 139	eqtr3d 2773	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
141	140	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
142		fnunres1 6600	. . . . . . . . 9 ⊢ ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)) = 𝑢)
143	134, 136, 141, 142	syl3anc 1375	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)) = 𝑢)
144	143	coeq2d 5807	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
145		resco 6204	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢))
146		resco 6204	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢))
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢)))
148		cnvun 6096	. . . . . . . . . . . . . . 15 ⊢ ^◡(𝑢 ∪ 𝑓) = (^◡𝑢 ∪ ^◡𝑓)
149	148	reseq1i 5930	. . . . . . . . . . . . . 14 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) = ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢)
150		f1ocnv 6782	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:dom 𝑢–1-1-onto→ran 𝑢 → ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢)
151		f1ofn 6771	. . . . . . . . . . . . . . . 16 ⊢ (^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢 → ^◡𝑢 Fn ran 𝑢)
152	69, 70, 150, 151	4syl 19	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢 Fn ran 𝑢)
153		f1ocnv 6782	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → ^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢))
154		f1ofn 6771	. . . . . . . . . . . . . . . 16 ⊢ (^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢) → ^◡𝑓 Fn (𝐷 ∖ ran 𝑢))
155	72, 153, 154	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑓 Fn (𝐷 ∖ ran 𝑢))
156		fnunres1 6600	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑢 Fn ran 𝑢 ∧ ^◡𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢) = ^◡𝑢)
157	152, 155, 76, 156	syl3anc 1375	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢) = ^◡𝑢)
158	149, 157	eqtr2id 2784	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢 = (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢))
159		simplr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑀‘𝑢) = 𝑄)
160	159	reseq1d 5933	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = (𝑄 ↾ ran 𝑢))
161	158, 160	coeq12d 5809	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢)) = ((^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)))
162	47	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝐷 ∈ Fin)
163	121	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 ∈ Word 𝐷)
164	93, 162, 163, 69	tocycfvres1 33194	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
165	160, 164	eqtr3d 2773	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
166	165	rneqd 5883	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran ((𝑢 cyclShift 1) ∘ ^◡𝑢))
167		1zzd 12552	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 1 ∈ ℤ)
168		cshf1o 33044	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷 ∧ 1 ∈ ℤ) → (𝑢 cyclShift 1):dom 𝑢–1-1-onto→ran 𝑢)
169	163, 69, 167, 168	syl3anc 1375	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 cyclShift 1):dom 𝑢–1-1-onto→ran 𝑢)
170	71, 150	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢)
171		f1oco 6793	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑢 cyclShift 1):dom 𝑢–1-1-onto→ran 𝑢 ∧ ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢) → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢)
172	169, 170, 171	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢)
173		f1ofo 6777	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢 → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–onto→ran 𝑢)
174		forn 6745	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–onto→ran 𝑢 → ran ((𝑢 cyclShift 1) ∘ ^◡𝑢) = ran 𝑢)
175	172, 173, 174	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran ((𝑢 cyclShift 1) ∘ ^◡𝑢) = ran 𝑢)
176	166, 175	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran 𝑢)
177		ssid 3940	. . . . . . . . . . . . . 14 ⊢ ran 𝑢 ⊆ ran 𝑢
178	176, 177	eqsstrdi 3962	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢)
179		cores 6203	. . . . . . . . . . . . 13 ⊢ (ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢 → ((^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)))
180	178, 179	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)))
181	147, 161, 180	3eqtrrd 2776	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
182	145, 181	eqtrid 2783	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
183	182	coeq1d 5806	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢))
184		cores 6203	. . . . . . . . . 10 ⊢ (ran 𝑢 ⊆ ran 𝑢 → (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
185	177, 184	mp1i 13	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
186	183, 185	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
187		cores 6203	. . . . . . . . 9 ⊢ (ran 𝑢 ⊆ ran 𝑢 → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
188	177, 187	mp1i 13	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
189	130	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (♯‘𝑢) = 𝑃)
190	91, 92, 8, 93, 162, 163, 69, 189	cycpmconjslem1 33238	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
191	186, 188, 190	3eqtr3d 2779	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
192	120, 144, 191	3eqtrd 2775	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = (( I ↾ (0..^𝑃)) cyclShift 1))
193		resco 6204	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
194	137	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 = (0..^𝑃))
195	194	difeq2d 4060	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = ((0..^𝑁) ∖ (0..^𝑃)))
196		fzodif1 32887	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (0...𝑁) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
197	90, 196	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
198	197	ad3antrrr 732	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
199	195, 198	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = (𝑃..^𝑁))
200	199	reseq2d 5934	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
201		fnunres2 6601	. . . . . . . . . . 11 ⊢ ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
202	134, 136, 141, 201	syl3anc 1375	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
203	200, 202	eqtr3d 2773	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)) = 𝑓)
204	203	coeq2d 5807	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
205	193, 204	eqtrid 2783	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
206	148	reseq1i 5930	. . . . . . . . . . . 12 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢))
207		fnunres2 6601	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 Fn ran 𝑢 ∧ ^◡𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
208	152, 155, 76, 207	syl3anc 1375	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
209	206, 208	eqtrid 2783	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
210	159	reseq1d 5933	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
211	93, 162, 163, 69	tocycfvres2 33195	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
212	210, 211	eqtr3d 2773	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
213	209, 212	coeq12d 5809	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))))
214	212	rneqd 5883	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ran ( I ↾ (𝐷 ∖ ran 𝑢)))
215		rnresi 6030	. . . . . . . . . . . . . 14 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) = (𝐷 ∖ ran 𝑢)
216	215	eqimssi 3978	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢)
217	214, 216	eqsstrdi 3962	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢))
218		cores 6203	. . . . . . . . . . . 12 ⊢ (ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))))
219	217, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))))
220		resco 6204	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
221	219, 220	eqtr4di 2789	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
222	213, 221	eqtr3d 2773	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
223	222	coeq1d 5806	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓))
224		f1of 6770	. . . . . . . . . . 11 ⊢ (^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢) → ^◡𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢))
225		fcoi1 6704	. . . . . . . . . . 11 ⊢ (^◡𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ^◡𝑓)
226	72, 153, 224, 225	4syl 19	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ^◡𝑓)
227	226	coeq1d 5806	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (^◡𝑓 ∘ 𝑓))
228		f1ococnv1 6799	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → (^◡𝑓 ∘ 𝑓) = ( I ↾ ((0..^𝑁) ∖ dom 𝑢)))
229	72, 228	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ 𝑓) = ( I ↾ ((0..^𝑁) ∖ dom 𝑢)))
230	199	reseq2d 5934	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ( I ↾ ((0..^𝑁) ∖ dom 𝑢)) = ( I ↾ (𝑃..^𝑁)))
231	227, 229, 230	3eqtrd 2775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
232		f1of 6770	. . . . . . . . 9 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢))
233		frn 6665	. . . . . . . . 9 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢) → ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢))
234		cores 6203	. . . . . . . . 9 ⊢ (ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
235	72, 232, 233, 234	4syl 19	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
236	223, 231, 235	3eqtr3rd 2780	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
237	205, 236	eqtrd 2771	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ( I ↾ (𝑃..^𝑁)))
238	192, 237	uneq12d 4102	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
239	118, 238	eqtrd 2771	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
240		vex 3432	. . . . . 6 ⊢ 𝑢 ∈ V
241		vex 3432	. . . . . 6 ⊢ 𝑓 ∈ V
242	240, 241	unex 7690	. . . . 5 ⊢ (𝑢 ∪ 𝑓) ∈ V
243		f1oeq1 6758	. . . . . 6 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (𝑞:(0..^𝑁)–1-1-onto→𝐷 ↔ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷))
244		cnveq 5818	. . . . . . . . 9 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ^◡𝑞 = ^◡(𝑢 ∪ 𝑓))
245	244	coeq1d 5806	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (^◡𝑞 ∘ 𝑄) = (^◡(𝑢 ∪ 𝑓) ∘ 𝑄))
246		id 22	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → 𝑞 = (𝑢 ∪ 𝑓))
247	245, 246	coeq12d 5809	. . . . . . 7 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
248	247	eqeq1d 2738	. . . . . 6 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))) ↔ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
249	243, 248	anbi12d 634	. . . . 5 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ((𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) ↔ ((𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))))
250	242, 249	spcev 3547	. . . 4 ⊢ (((𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
251	87, 239, 250	syl2anc 586	. . 3 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
252	68, 251	exlimddv 1938	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
253		nfcv 2898	. . 3 ⊢ Ⅎ𝑢𝑀
254	93, 92, 94	tocycf 33201	. . . 4 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵)
255		ffn 6658	. . . 4 ⊢ (𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
256	4, 254, 255	3syl 18	. . 3 ⊢ (𝜑 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
257	97, 91	eleqtrdi 2846	. . 3 ⊢ (𝜑 → 𝑄 ∈ (𝑀 “ (^◡♯ “ {𝑃})))
258	253, 256, 257	fvelimad 6897	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))(𝑀‘𝑢) = 𝑄)
259	252, 258	r19.29a 3144	1 ⊢ (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1543 ∃wex 1782 ∈ wcel 2115 {crab 3388 Vcvv 3428 ∖ cdif 3883 ∪ cun 3884 ∩ cin 3885 ⊆ wss 3886 ∅c0 4264 {csn 4558 class class class wbr 5075 I cid 5515 ^◡ccnv 5620 dom cdm 5621 ran crn 5622 ↾ cres 5623 “ cima 5624 ∘ ccom 5625 Rel wrel 5626 Fun wfun 6482 Fn wfn 6483 ⟶wf 6484 –1-1→wf1 6485 –onto→wfo 6486 –1-1-onto→wf1o 6487 ‘cfv 6488 (class class class)co 7359 Fincfn 8886 0cc0 11032 1c1 11033 +∞cpnf 11170 ≤ cle 11174 − cmin 11371 ℕ₀cn0 12431 ℤcz 12518 ℤ_≥cuz 12782 ...cfz 13455 ..^cfzo 13602 ♯chash 14286 Word cword 14469 cyclShift ccsh 14744 Basecbs 17173 +_gcplusg 17214 -_gcsg 18905 SymGrpcsymg 19338 toCycctocyc 33190

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1970 ax-7 2011 ax-8 2117 ax-9 2125 ax-10 2148 ax-11 2164 ax-12 2185 ax-ext 2708 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7681 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110

This theorem depends on definitions: df-bi 208 df-an 397 df-or 850 df-3or 1089 df-3an 1090 df-tru 1546 df-fal 1556 df-ex 1783 df-nf 1787 df-sb 2070 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3061 df-rmo 3341 df-reu 3342 df-rab 3389 df-v 3430 df-sbc 3727 df-csb 3835 df-dif 3889 df-un 3891 df-in 3893 df-ss 3903 df-pss 3906 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4842 df-int 4881 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-riota 7316 df-ov 7362 df-oprab 7363 df-mpo 7364 df-om 7810 df-1st 7934 df-2nd 7935 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-oadd 8402 df-er 8636 df-map 8768 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-sup 9348 df-inf 9349 df-dju 9819 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-xnn0 12505 df-z 12519 df-uz 12783 df-rp 12937 df-fz 13456 df-fzo 13603 df-fl 13745 df-mod 13823 df-hash 14287 df-word 14470 df-concat 14527 df-substr 14598 df-pfx 14628 df-csh 14745 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-tset 17233 df-efmnd 18831 df-symg 19339 df-tocyc 33191

This theorem is referenced by: cycpmconjs 33240

W3C validator