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 31324

Description: Lemma for cycpmconjs 31325. (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 13622	. . . . 5 ⊢ (0..^𝑁) ∈ Fin
2		diffi 8979	. . . . 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 8979	. . . . . 6 ⊢ (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ Fin)
6	4, 5	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ Fin)
7	6	ad2antrr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (𝐷 ∖ ran 𝑢) ∈ Fin)
8		cycpmconjs.n	. . . . . . . . . 10 ⊢ 𝑁 = (♯‘𝐷)
9		hashcl 13999	. . . . . . . . . . 11 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
10	4, 9	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
11	8, 10	eqeltrid 2843	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
12		hashfzo0 14073	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0..^𝑁)) = 𝑁)
13	11, 12	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0..^𝑁)) = 𝑁)
14	13, 8	eqtrdi 2795	. . . . . . 7 ⊢ (𝜑 → (♯‘(0..^𝑁)) = (♯‘𝐷))
15	14	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(0..^𝑁)) = (♯‘𝐷))
16		simplr 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃})))
17	16	elin1d 4128	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
18		elrabi 3611	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢 ∈ Word 𝐷)
19		wrdfin 14163	. . . . . . . . 9 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 ∈ Fin)
20	17, 18, 19	3syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ Fin)
21		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
22		dmeq 5801	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
23		eqidd 2739	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
24	21, 22, 23	f1eq123d 6692	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
25	24	elrab 3617	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷))
26	25	simprbi 496	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢:dom 𝑢–1-1→𝐷)
27	17, 26	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢:dom 𝑢–1-1→𝐷)
28		f1fun 6656	. . . . . . . . 9 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → Fun 𝑢)
29	27, 28	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → Fun 𝑢)
30		hashfun 14080	. . . . . . . . 9 ⊢ (𝑢 ∈ Fin → (Fun 𝑢 ↔ (♯‘𝑢) = (♯‘dom 𝑢)))
31	30	biimpa 476	. . . . . . . 8 ⊢ ((𝑢 ∈ Fin ∧ Fun 𝑢) → (♯‘𝑢) = (♯‘dom 𝑢))
32	20, 29, 31	syl2anc 583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = (♯‘dom 𝑢))
33	16	dmexd 7726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ∈ V)
34		hashf1rn 13995	. . . . . . . 8 ⊢ ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
35	33, 27, 34	syl2anc 583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = (♯‘ran 𝑢))
36	32, 35	eqtr3d 2780	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘dom 𝑢) = (♯‘ran 𝑢))
37	15, 36	oveq12d 7273	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
38	1	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^𝑁) ∈ Fin)
39		wrddm 14152	. . . . . . . 8 ⊢ (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
40	17, 18, 39	3syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^(♯‘𝑢)))
41		hashcl 13999	. . . . . . . . . . 11 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
42	17, 18, 19, 41	4syl 19	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℕ₀)
43	42	nn0zd 12353	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℤ)
44	10	nn0zd 12353	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐷) ∈ ℤ)
45	8, 44	eqeltrid 2843	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
46	45	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ ℤ)
47	4	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝐷 ∈ Fin)
48		wrdf 14150	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢:(0..^(♯‘𝑢))⟶𝐷)
49	48	frnd 6592	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → ran 𝑢 ⊆ 𝐷)
50	17, 18, 49	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ran 𝑢 ⊆ 𝐷)
51		hashss 14052	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
52	47, 50, 51	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
53	8	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 = (♯‘𝐷))
54	52, 35, 53	3brtr4d 5102	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ≤ 𝑁)
55		eluz1 12515	. . . . . . . . . 10 ⊢ ((♯‘𝑢) ∈ ℤ → (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) ↔ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)))
56	55	biimpar 477	. . . . . . . . 9 ⊢ (((♯‘𝑢) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
57	43, 46, 54, 56	syl12anc 833	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
58		fzoss2 13343	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
59	57, 58	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
60	40, 59	eqsstrd 3955	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ⊆ (0..^𝑁))
61		hashssdif 14055	. . . . . 6 ⊢ (((0..^𝑁) ∈ Fin ∧ dom 𝑢 ⊆ (0..^𝑁)) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
62	38, 60, 61	syl2anc 583	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
63		hashssdif 14055	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
64	47, 50, 63	syl2anc 583	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
65	37, 62, 64	3eqtr4d 2788	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)))
66		hasheqf1o 13991	. . . . 5 ⊢ ((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) → ((♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)) ↔ ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)))
67	66	biimpa 476	. . . 4 ⊢ (((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) ∧ (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
68	3, 7, 65, 67	syl21anc 834	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
69	27	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢–1-1→𝐷)
70		f1f1orn 6711	. . . . . . 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 484	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
73		disjdif 4402	. . . . . . 7 ⊢ (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅
74	73	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
75		disjdif 4402	. . . . . . 7 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
76	75	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
77		f1oun 6719	. . . . . 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 835	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
79		eqidd 2739	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓) = (𝑢 ∪ 𝑓))
80	60	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 ⊆ (0..^𝑁))
81		undif 4412	. . . . . . 7 ⊢ (dom 𝑢 ⊆ (0..^𝑁) ↔ (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
82	80, 81	sylib 217	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
83		undif 4412	. . . . . . . 8 ⊢ (ran 𝑢 ⊆ 𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
84	50, 83	sylib 217	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
85	84	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
86	79, 82, 85	f1oeq123d 6694	. . . . 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 231	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷)
88		f1ocnv 6712	. . . . . . . . . 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 31322	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑃 ∈ (0...𝑁)) → 𝐶 ⊆ 𝐵)
96	4, 90, 95	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
97		cycpmconjs.q	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ 𝐶)
98	96, 97	sseldd 3918	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ 𝐵)
99	92, 94	symgbasf1o 18897	. . . . . . . . . . 11 ⊢ (𝑄 ∈ 𝐵 → 𝑄:𝐷–1-1-onto→𝐷)
100	98, 99	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
101	100	ad3antrrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑄:𝐷–1-1-onto→𝐷)
102		f1oco 6722	. . . . . . . . 9 ⊢ ((^◡(𝑢 ∪ 𝑓):𝐷–1-1-onto→(0..^𝑁) ∧ 𝑄:𝐷–1-1-onto→𝐷) → (^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁))
103	89, 101, 102	syl2anc 583	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁))
104		f1oco 6722	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁) ∧ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
105	103, 87, 104	syl2anc 583	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
106		f1ofun 6702	. . . . . . 7 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
107		funrel 6435	. . . . . . 7 ⊢ (Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
108	105, 106, 107	3syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
109		f1odm 6704	. . . . . . . 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 13348	. . . . . . . . 9 ⊢ (𝑃 ∈ (0...𝑁) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
112	90, 111	syl 17	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
113	112	ad3antrrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
114	110, 113	eqtrd 2778	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
115		fzodisj 13349	. . . . . . 7 ⊢ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅
116		reldisjun 30843	. . . . . . 7 ⊢ ((Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ∧ dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)) ∧ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
117	115, 116	mp3an3 1448	. . . . . 6 ⊢ ((Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ∧ dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁))) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
118	108, 114, 117	syl2anc 583	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
119		resco 6143	. . . . . . . 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 14159	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 Fn (0..^(♯‘𝑢)))
123	121, 122	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 Fn (0..^(♯‘𝑢)))
124	16	elin2d 4129	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ (^◡♯ “ {𝑃}))
125		hashf 13980	. . . . . . . . . . . . . . . 16 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
126		ffn 6584	. . . . . . . . . . . . . . . 16 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
127		fniniseg 6919	. . . . . . . . . . . . . . . 16 ⊢ (♯ Fn V → (𝑢 ∈ (^◡♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃)))
128	125, 126, 127	mp2b 10	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (^◡♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃))
129	128	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (^◡♯ “ {𝑃}) → (♯‘𝑢) = 𝑃)
130	124, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = 𝑃)
131	130	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) = (0..^𝑃))
132	131	fneq2d 6511	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (𝑢 Fn (0..^(♯‘𝑢)) ↔ 𝑢 Fn (0..^𝑃)))
133	123, 132	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 Fn (0..^𝑃))
134	133	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 Fn (0..^𝑃))
135		f1ofn 6701	. . . . . . . . . 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 2778	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^𝑃))
138	137	ineq1d 4142	. . . . . . . . . . 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 2780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
141	140	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
142		fnunres1 30846	. . . . . . . . 9 ⊢ ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)) = 𝑢)
143	134, 136, 141, 142	syl3anc 1369	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)) = 𝑢)
144	143	coeq2d 5760	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
145		resco 6143	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢))
146		resco 6143	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢))
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢)))
148		cnvun 6035	. . . . . . . . . . . . . . 15 ⊢ ^◡(𝑢 ∪ 𝑓) = (^◡𝑢 ∪ ^◡𝑓)
149	148	reseq1i 5876	. . . . . . . . . . . . . 14 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) = ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢)
150		f1ocnv 6712	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:dom 𝑢–1-1-onto→ran 𝑢 → ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢)
151		f1ofn 6701	. . . . . . . . . . . . . . . 16 ⊢ (^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢 → ^◡𝑢 Fn ran 𝑢)
152	71, 150, 151	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢 Fn ran 𝑢)
153		f1ocnv 6712	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → ^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢))
154		f1ofn 6701	. . . . . . . . . . . . . . . 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 30846	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑢 Fn ran 𝑢 ∧ ^◡𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢) = ^◡𝑢)
157	152, 155, 76, 156	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢) = ^◡𝑢)
158	149, 157	eqtr2id 2792	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢 = (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢))
159		simplr 765	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑀‘𝑢) = 𝑄)
160	159	reseq1d 5879	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = (𝑄 ↾ ran 𝑢))
161	158, 160	coeq12d 5762	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢)) = ((^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)))
162	47	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝐷 ∈ Fin)
163	121	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 ∈ Word 𝐷)
164	93, 162, 163, 69	tocycfvres1 31279	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
165	160, 164	eqtr3d 2780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
166	165	rneqd 5836	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran ((𝑢 cyclShift 1) ∘ ^◡𝑢))
167		1zzd 12281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 1 ∈ ℤ)
168		cshf1o 31136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷 ∧ 1 ∈ ℤ) → (𝑢 cyclShift 1):dom 𝑢–1-1-onto→ran 𝑢)
169	163, 69, 167, 168	syl3anc 1369	. . . . . . . . . . . . . . . . 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 6722	. . . . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢)
173		f1ofo 6707	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢 → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–onto→ran 𝑢)
174		forn 6675	. . . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran 𝑢)
177		ssid 3939	. . . . . . . . . . . . . 14 ⊢ ran 𝑢 ⊆ ran 𝑢
178	176, 177	eqsstrdi 3971	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢)
179		cores 6142	. . . . . . . . . . . . 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 2783	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
182	145, 181	syl5eq 2791	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
183	182	coeq1d 5759	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢))
184		cores 6142	. . . . . . . . . 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 2778	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
187		cores 6142	. . . . . . . . 9 ⊢ (ran 𝑢 ⊆ ran 𝑢 → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
188	177, 187	mp1i 13	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
189	130	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (♯‘𝑢) = 𝑃)
190	91, 92, 8, 93, 162, 163, 69, 189	cycpmconjslem1 31323	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
191	186, 188, 190	3eqtr3d 2786	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
192	120, 144, 191	3eqtrd 2782	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = (( I ↾ (0..^𝑃)) cyclShift 1))
193		resco 6143	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
194	137	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 = (0..^𝑃))
195	194	difeq2d 4053	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = ((0..^𝑁) ∖ (0..^𝑃)))
196		fzodif1 31016	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (0...𝑁) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
197	90, 196	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
198	197	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
199	195, 198	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = (𝑃..^𝑁))
200	199	reseq2d 5880	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
201		fnunres2 30917	. . . . . . . . . . 11 ⊢ ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
202	134, 136, 141, 201	syl3anc 1369	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
203	200, 202	eqtr3d 2780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)) = 𝑓)
204	203	coeq2d 5760	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
205	193, 204	syl5eq 2791	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
206	148	reseq1i 5876	. . . . . . . . . . . 12 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢))
207		fnunres2 30917	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 Fn ran 𝑢 ∧ ^◡𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
208	152, 155, 76, 207	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
209	206, 208	syl5eq 2791	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
210	159	reseq1d 5879	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
211	93, 162, 163, 69	tocycfvres2 31280	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
212	210, 211	eqtr3d 2780	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
213	209, 212	coeq12d 5762	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))))
214	212	rneqd 5836	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ran ( I ↾ (𝐷 ∖ ran 𝑢)))
215		rnresi 5972	. . . . . . . . . . . . . 14 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) = (𝐷 ∖ ran 𝑢)
216	215	eqimssi 3975	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢)
217	214, 216	eqsstrdi 3971	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢))
218		cores 6142	. . . . . . . . . . . 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 6143	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
221	219, 220	eqtr4di 2797	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
222	213, 221	eqtr3d 2780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
223	222	coeq1d 5759	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓))
224		f1of 6700	. . . . . . . . . . . 12 ⊢ (^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢) → ^◡𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢))
225	72, 153, 224	3syl 18	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢))
226		fcoi1 6632	. . . . . . . . . . 11 ⊢ (^◡𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ^◡𝑓)
227	225, 226	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ^◡𝑓)
228	227	coeq1d 5759	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (^◡𝑓 ∘ 𝑓))
229		f1ococnv1 6728	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → (^◡𝑓 ∘ 𝑓) = ( I ↾ ((0..^𝑁) ∖ dom 𝑢)))
230	72, 229	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ 𝑓) = ( I ↾ ((0..^𝑁) ∖ dom 𝑢)))
231	199	reseq2d 5880	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ( I ↾ ((0..^𝑁) ∖ dom 𝑢)) = ( I ↾ (𝑃..^𝑁)))
232	228, 230, 231	3eqtrd 2782	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
233		f1of 6700	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢))
234		frn 6591	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢) → ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢))
235	72, 233, 234	3syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢))
236		cores 6142	. . . . . . . . 9 ⊢ (ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
237	235, 236	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
238	223, 232, 237	3eqtr3rd 2787	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
239	205, 238	eqtrd 2778	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ( I ↾ (𝑃..^𝑁)))
240	192, 239	uneq12d 4094	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
241	118, 240	eqtrd 2778	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
242		vex 3426	. . . . . 6 ⊢ 𝑢 ∈ V
243		vex 3426	. . . . . 6 ⊢ 𝑓 ∈ V
244	242, 243	unex 7574	. . . . 5 ⊢ (𝑢 ∪ 𝑓) ∈ V
245		f1oeq1 6688	. . . . . 6 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (𝑞:(0..^𝑁)–1-1-onto→𝐷 ↔ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷))
246		cnveq 5771	. . . . . . . . 9 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ^◡𝑞 = ^◡(𝑢 ∪ 𝑓))
247	246	coeq1d 5759	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (^◡𝑞 ∘ 𝑄) = (^◡(𝑢 ∪ 𝑓) ∘ 𝑄))
248		id 22	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → 𝑞 = (𝑢 ∪ 𝑓))
249	247, 248	coeq12d 5762	. . . . . . 7 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
250	249	eqeq1d 2740	. . . . . 6 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))) ↔ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
251	245, 250	anbi12d 630	. . . . 5 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ((𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) ↔ ((𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))))
252	244, 251	spcev 3535	. . . 4 ⊢ (((𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
253	87, 241, 252	syl2anc 583	. . 3 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
254	68, 253	exlimddv 1939	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
255		nfcv 2906	. . 3 ⊢ Ⅎ𝑢𝑀
256	93, 92, 94	tocycf 31286	. . . 4 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵)
257		ffn 6584	. . . 4 ⊢ (𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
258	4, 256, 257	3syl 18	. . 3 ⊢ (𝜑 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
259	97, 91	eleqtrdi 2849	. . 3 ⊢ (𝜑 → 𝑄 ∈ (𝑀 “ (^◡♯ “ {𝑃})))
260	255, 258, 259	fvelimad 6818	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))(𝑀‘𝑢) = 𝑄)
261	254, 260	r19.29a 3217	1 ⊢ (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∃wex 1783 ∈ wcel 2108 {crab 3067 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 {csn 4558 class class class wbr 5070 I cid 5479 ^◡ccnv 5579 dom cdm 5580 ran crn 5581 ↾ cres 5582 “ cima 5583 ∘ ccom 5584 Rel wrel 5585 Fun wfun 6412 Fn wfn 6413 ⟶wf 6414 –1-1→wf1 6415 –onto→wfo 6416 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 Fincfn 8691 0cc0 10802 1c1 10803 +∞cpnf 10937 ≤ cle 10941 − cmin 11135 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ...cfz 13168 ..^cfzo 13311 ♯chash 13972 Word cword 14145 cyclShift ccsh 14429 Basecbs 16840 +_gcplusg 16888 -_gcsg 18494 SymGrpcsymg 18889 toCycctocyc 31275

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-oadd 8271 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-xnn0 12236 df-z 12250 df-uz 12512 df-rp 12660 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-hash 13973 df-word 14146 df-concat 14202 df-substr 14282 df-pfx 14312 df-csh 14430 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-tset 16907 df-efmnd 18423 df-symg 18890 df-tocyc 31276

This theorem is referenced by: cycpmconjs 31325

W3C validator