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 32854

Description: Lemma for cycpmconjs 32855. (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 13963	. . . . 5 ⊢ (0..^𝑁) ∈ Fin
2		diffi 9195	. . . . 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 9195	. . . . . 6 ⊢ (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ Fin)
6	4, 5	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ Fin)
7	6	ad2antrr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (𝐷 ∖ ran 𝑢) ∈ Fin)
8		cycpmconjs.n	. . . . . . . . . 10 ⊢ 𝑁 = (♯‘𝐷)
9		hashcl 14339	. . . . . . . . . . 11 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
10	4, 9	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
11	8, 10	eqeltrid 2832	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
12		hashfzo0 14413	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0..^𝑁)) = 𝑁)
13	11, 12	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0..^𝑁)) = 𝑁)
14	13, 8	eqtrdi 2783	. . . . . . 7 ⊢ (𝜑 → (♯‘(0..^𝑁)) = (♯‘𝐷))
15	14	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(0..^𝑁)) = (♯‘𝐷))
16		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃})))
17	16	elin1d 4194	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
18		elrabi 3674	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢 ∈ Word 𝐷)
19		wrdfin 14506	. . . . . . . . 9 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 ∈ Fin)
20	17, 18, 19	3syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ Fin)
21		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
22		dmeq 5900	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
23		eqidd 2728	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
24	21, 22, 23	f1eq123d 6825	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
25	24	elrab 3680	. . . . . . . . . . 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 6789	. . . . . . . . 9 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → Fun 𝑢)
29	27, 28	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → Fun 𝑢)
30		hashfun 14420	. . . . . . . . 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 7905	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ∈ V)
34		hashf1rn 14335	. . . . . . . 8 ⊢ ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
35	33, 27, 34	syl2anc 583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = (♯‘ran 𝑢))
36	32, 35	eqtr3d 2769	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘dom 𝑢) = (♯‘ran 𝑢))
37	15, 36	oveq12d 7432	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
38	1	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^𝑁) ∈ Fin)
39		wrddm 14495	. . . . . . . 8 ⊢ (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
40	17, 18, 39	3syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^(♯‘𝑢)))
41		hashcl 14339	. . . . . . . . . . 11 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
42	17, 18, 19, 41	4syl 19	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℕ₀)
43	42	nn0zd 12606	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℤ)
44	10	nn0zd 12606	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐷) ∈ ℤ)
45	8, 44	eqeltrid 2832	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
46	45	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ ℤ)
47	4	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝐷 ∈ Fin)
48		wrdf 14493	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢:(0..^(♯‘𝑢))⟶𝐷)
49	48	frnd 6724	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → ran 𝑢 ⊆ 𝐷)
50	17, 18, 49	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ran 𝑢 ⊆ 𝐷)
51		hashss 14392	. . . . . . . . . . 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 5174	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ≤ 𝑁)
55		eluz1 12848	. . . . . . . . . 10 ⊢ ((♯‘𝑢) ∈ ℤ → (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) ↔ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)))
56	55	biimpar 477	. . . . . . . . 9 ⊢ (((♯‘𝑢) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
57	43, 46, 54, 56	syl12anc 836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
58		fzoss2 13684	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
59	57, 58	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
60	40, 59	eqsstrd 4016	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ⊆ (0..^𝑁))
61		hashssdif 14395	. . . . . 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 14395	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
64	47, 50, 63	syl2anc 583	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
65	37, 62, 64	3eqtr4d 2777	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)))
66		hasheqf1o 14332	. . . . 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 837	. . 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 6844	. . . . . . 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 4467	. . . . . . 7 ⊢ (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅
74	73	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
75		disjdif 4467	. . . . . . 7 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
76	75	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
77		f1oun 6852	. . . . . 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 838	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
79		eqidd 2728	. . . . . 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 4477	. . . . . . 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 4477	. . . . . . . 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 6827	. . . . 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 6845	. . . . . . . . . 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 32852	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑃 ∈ (0...𝑁)) → 𝐶 ⊆ 𝐵)
96	4, 90, 95	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
97		cycpmconjs.q	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ 𝐶)
98	96, 97	sseldd 3979	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ 𝐵)
99	92, 94	symgbasf1o 19320	. . . . . . . . . . 11 ⊢ (𝑄 ∈ 𝐵 → 𝑄:𝐷–1-1-onto→𝐷)
100	98, 99	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
101	100	ad3antrrr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑄:𝐷–1-1-onto→𝐷)
102		f1oco 6856	. . . . . . . . 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 6856	. . . . . . . 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 6835	. . . . . . 7 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
107		funrel 6564	. . . . . . 7 ⊢ (Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
108	105, 106, 107	3syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
109		f1odm 6837	. . . . . . . 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 13689	. . . . . . . . 9 ⊢ (𝑃 ∈ (0...𝑁) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
112	90, 111	syl 17	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
113	112	ad3antrrr 729	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
114	110, 113	eqtrd 2767	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
115		fzodisj 13690	. . . . . . 7 ⊢ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅
116		reldisjun 6030	. . . . . . 7 ⊢ ((Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ∧ dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)) ∧ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
117	115, 116	mp3an3 1447	. . . . . 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 6248	. . . . . . . 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 14502	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 Fn (0..^(♯‘𝑢)))
123	121, 122	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 Fn (0..^(♯‘𝑢)))
124	16	elin2d 4195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ (^◡♯ “ {𝑃}))
125		hashf 14321	. . . . . . . . . . . . . . . 16 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
126		ffn 6716	. . . . . . . . . . . . . . . 16 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
127		fniniseg 7063	. . . . . . . . . . . . . . . 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 7430	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) = (0..^𝑃))
132	131	fneq2d 6642	. . . . . . . . . . 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 6834	. . . . . . . . . 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 2767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^𝑃))
138	137	ineq1d 4207	. . . . . . . . . . 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 2769	. . . . . . . . . 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 6660	. . . . . . . . 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 5859	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
145		resco 6248	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢))
146		resco 6248	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢))
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢)))
148		cnvun 6141	. . . . . . . . . . . . . . 15 ⊢ ^◡(𝑢 ∪ 𝑓) = (^◡𝑢 ∪ ^◡𝑓)
149	148	reseq1i 5975	. . . . . . . . . . . . . 14 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) = ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢)
150		f1ocnv 6845	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:dom 𝑢–1-1-onto→ran 𝑢 → ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢)
151		f1ofn 6834	. . . . . . . . . . . . . . . 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 6845	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → ^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢))
154		f1ofn 6834	. . . . . . . . . . . . . . . 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 6660	. . . . . . . . . . . . . . 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 2780	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢 = (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢))
159		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑀‘𝑢) = 𝑄)
160	159	reseq1d 5978	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = (𝑄 ↾ ran 𝑢))
161	158, 160	coeq12d 5861	. . . . . . . . . . . 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 32809	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
165	160, 164	eqtr3d 2769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
166	165	rneqd 5934	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran ((𝑢 cyclShift 1) ∘ ^◡𝑢))
167		1zzd 12615	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 1 ∈ ℤ)
168		cshf1o 32665	. . . . . . . . . . . . . . . . . 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 6856	. . . . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢 → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–onto→ran 𝑢)
174		forn 6808	. . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran 𝑢)
177		ssid 4000	. . . . . . . . . . . . . 14 ⊢ ran 𝑢 ⊆ ran 𝑢
178	176, 177	eqsstrdi 4032	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢)
179		cores 6247	. . . . . . . . . . . . 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 2772	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
182	145, 181	eqtrid 2779	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
183	182	coeq1d 5858	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢))
184		cores 6247	. . . . . . . . . 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 2767	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
187		cores 6247	. . . . . . . . 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 32853	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
191	186, 188, 190	3eqtr3d 2775	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
192	120, 144, 191	3eqtrd 2771	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = (( I ↾ (0..^𝑃)) cyclShift 1))
193		resco 6248	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
194	137	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 = (0..^𝑃))
195	194	difeq2d 4118	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = ((0..^𝑁) ∖ (0..^𝑃)))
196		fzodif1 32545	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (0...𝑁) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
197	90, 196	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
198	197	ad3antrrr 729	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
199	195, 198	eqtrd 2767	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = (𝑃..^𝑁))
200	199	reseq2d 5979	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
201		fnunres2 6661	. . . . . . . . . . 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 2769	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)) = 𝑓)
204	203	coeq2d 5859	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
205	193, 204	eqtrid 2779	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
206	148	reseq1i 5975	. . . . . . . . . . . 12 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢))
207		fnunres2 6661	. . . . . . . . . . . . 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	eqtrid 2779	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
210	159	reseq1d 5978	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
211	93, 162, 163, 69	tocycfvres2 32810	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
212	210, 211	eqtr3d 2769	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
213	209, 212	coeq12d 5861	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))))
214	212	rneqd 5934	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ran ( I ↾ (𝐷 ∖ ran 𝑢)))
215		rnresi 6072	. . . . . . . . . . . . . 14 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) = (𝐷 ∖ ran 𝑢)
216	215	eqimssi 4038	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢)
217	214, 216	eqsstrdi 4032	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢))
218		cores 6247	. . . . . . . . . . . 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 6248	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
221	219, 220	eqtr4di 2785	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
222	213, 221	eqtr3d 2769	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
223	222	coeq1d 5858	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓))
224		f1of 6833	. . . . . . . . . . . 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 6765	. . . . . . . . . . 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 5858	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (^◡𝑓 ∘ 𝑓))
229		f1ococnv1 6862	. . . . . . . . . 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 5979	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ( I ↾ ((0..^𝑁) ∖ dom 𝑢)) = ( I ↾ (𝑃..^𝑁)))
232	228, 230, 231	3eqtrd 2771	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
233		f1of 6833	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢))
234		frn 6723	. . . . . . . . . 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 6247	. . . . . . . . 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 2776	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
239	205, 238	eqtrd 2767	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ( I ↾ (𝑃..^𝑁)))
240	192, 239	uneq12d 4160	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
241	118, 240	eqtrd 2767	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
242		vex 3473	. . . . . 6 ⊢ 𝑢 ∈ V
243		vex 3473	. . . . . 6 ⊢ 𝑓 ∈ V
244	242, 243	unex 7742	. . . . 5 ⊢ (𝑢 ∪ 𝑓) ∈ V
245		f1oeq1 6821	. . . . . 6 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (𝑞:(0..^𝑁)–1-1-onto→𝐷 ↔ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷))
246		cnveq 5870	. . . . . . . . 9 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ^◡𝑞 = ^◡(𝑢 ∪ 𝑓))
247	246	coeq1d 5858	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (^◡𝑞 ∘ 𝑄) = (^◡(𝑢 ∪ 𝑓) ∘ 𝑄))
248		id 22	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → 𝑞 = (𝑢 ∪ 𝑓))
249	247, 248	coeq12d 5861	. . . . . . 7 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
250	249	eqeq1d 2729	. . . . . 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 3591	. . . 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 1931	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
255		nfcv 2898	. . 3 ⊢ Ⅎ𝑢𝑀
256	93, 92, 94	tocycf 32816	. . . 4 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵)
257		ffn 6716	. . . 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 2838	. . 3 ⊢ (𝜑 → 𝑄 ∈ (𝑀 “ (^◡♯ “ {𝑃})))
260	255, 258, 259	fvelimad 6960	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))(𝑀‘𝑢) = 𝑄)
261	254, 260	r19.29a 3157	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 1534 ∃wex 1774 ∈ wcel 2099 {crab 3427 Vcvv 3469 ∖ cdif 3941 ∪ cun 3942 ∩ cin 3943 ⊆ wss 3944 ∅c0 4318 {csn 4624 class class class wbr 5142 I cid 5569 ^◡ccnv 5671 dom cdm 5672 ran crn 5673 ↾ cres 5674 “ cima 5675 ∘ ccom 5676 Rel wrel 5677 Fun wfun 6536 Fn wfn 6537 ⟶wf 6538 –1-1→wf1 6539 –onto→wfo 6540 –1-1-onto→wf1o 6541 ‘cfv 6542 (class class class)co 7414 Fincfn 8955 0cc0 11130 1c1 11131 +∞cpnf 11267 ≤ cle 11271 − cmin 11466 ℕ₀cn0 12494 ℤcz 12580 ℤ_≥cuz 12844 ...cfz 13508 ..^cfzo 13651 ♯chash 14313 Word cword 14488 cyclShift ccsh 14762 Basecbs 17171 +_gcplusg 17224 -_gcsg 18883 SymGrpcsymg 19312 toCycctocyc 32805

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207 ax-pre-sup 11208

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-oadd 8484 df-er 8718 df-map 8838 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9457 df-inf 9458 df-dju 9916 df-card 9954 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-div 11894 df-nn 12235 df-2 12297 df-3 12298 df-4 12299 df-5 12300 df-6 12301 df-7 12302 df-8 12303 df-9 12304 df-n0 12495 df-xnn0 12567 df-z 12581 df-uz 12845 df-rp 12999 df-fz 13509 df-fzo 13652 df-fl 13781 df-mod 13859 df-hash 14314 df-word 14489 df-concat 14545 df-substr 14615 df-pfx 14645 df-csh 14763 df-struct 17107 df-sets 17124 df-slot 17142 df-ndx 17154 df-base 17172 df-ress 17201 df-plusg 17237 df-tset 17243 df-efmnd 18812 df-symg 19313 df-tocyc 32806

This theorem is referenced by: cycpmconjs 32855

W3C validator