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 32782

Description: Lemma for cycpmconjs 32783. (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 13936	. . . . 5 ⊢ (0..^𝑁) ∈ Fin
2		diffi 9175	. . . . 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 9175	. . . . . 6 ⊢ (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ Fin)
6	4, 5	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ Fin)
7	6	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (𝐷 ∖ ran 𝑢) ∈ Fin)
8		cycpmconjs.n	. . . . . . . . . 10 ⊢ 𝑁 = (♯‘𝐷)
9		hashcl 14313	. . . . . . . . . . 11 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
10	4, 9	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
11	8, 10	eqeltrid 2829	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
12		hashfzo0 14387	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0..^𝑁)) = 𝑁)
13	11, 12	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0..^𝑁)) = 𝑁)
14	13, 8	eqtrdi 2780	. . . . . . 7 ⊢ (𝜑 → (♯‘(0..^𝑁)) = (♯‘𝐷))
15	14	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(0..^𝑁)) = (♯‘𝐷))
16		simplr 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃})))
17	16	elin1d 4190	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
18		elrabi 3669	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢 ∈ Word 𝐷)
19		wrdfin 14479	. . . . . . . . 9 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 ∈ Fin)
20	17, 18, 19	3syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ Fin)
21		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
22		dmeq 5893	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
23		eqidd 2725	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
24	21, 22, 23	f1eq123d 6815	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
25	24	elrab 3675	. . . . . . . . . . 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 6779	. . . . . . . . 9 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → Fun 𝑢)
29	27, 28	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → Fun 𝑢)
30		hashfun 14394	. . . . . . . . 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 7889	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ∈ V)
34		hashf1rn 14309	. . . . . . . 8 ⊢ ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
35	33, 27, 34	syl2anc 583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = (♯‘ran 𝑢))
36	32, 35	eqtr3d 2766	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘dom 𝑢) = (♯‘ran 𝑢))
37	15, 36	oveq12d 7419	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
38	1	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^𝑁) ∈ Fin)
39		wrddm 14468	. . . . . . . 8 ⊢ (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
40	17, 18, 39	3syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^(♯‘𝑢)))
41		hashcl 14313	. . . . . . . . . . 11 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
42	17, 18, 19, 41	4syl 19	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℕ₀)
43	42	nn0zd 12581	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℤ)
44	10	nn0zd 12581	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐷) ∈ ℤ)
45	8, 44	eqeltrid 2829	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
46	45	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ ℤ)
47	4	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝐷 ∈ Fin)
48		wrdf 14466	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢:(0..^(♯‘𝑢))⟶𝐷)
49	48	frnd 6715	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → ran 𝑢 ⊆ 𝐷)
50	17, 18, 49	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ran 𝑢 ⊆ 𝐷)
51		hashss 14366	. . . . . . . . . . 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 5170	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ≤ 𝑁)
55		eluz1 12823	. . . . . . . . . 10 ⊢ ((♯‘𝑢) ∈ ℤ → (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) ↔ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)))
56	55	biimpar 477	. . . . . . . . 9 ⊢ (((♯‘𝑢) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
57	43, 46, 54, 56	syl12anc 834	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
58		fzoss2 13657	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
59	57, 58	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
60	40, 59	eqsstrd 4012	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ⊆ (0..^𝑁))
61		hashssdif 14369	. . . . . 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 14369	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
64	47, 50, 63	syl2anc 583	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
65	37, 62, 64	3eqtr4d 2774	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)))
66		hasheqf1o 14306	. . . . 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 835	. . 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 6834	. . . . . . 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 4463	. . . . . . 7 ⊢ (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅
74	73	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
75		disjdif 4463	. . . . . . 7 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
76	75	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
77		f1oun 6842	. . . . . 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 836	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
79		eqidd 2725	. . . . . 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 4473	. . . . . . 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 4473	. . . . . . . 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 6817	. . . . 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 6835	. . . . . . . . . 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 32780	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑃 ∈ (0...𝑁)) → 𝐶 ⊆ 𝐵)
96	4, 90, 95	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
97		cycpmconjs.q	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ 𝐶)
98	96, 97	sseldd 3975	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ 𝐵)
99	92, 94	symgbasf1o 19284	. . . . . . . . . . 11 ⊢ (𝑄 ∈ 𝐵 → 𝑄:𝐷–1-1-onto→𝐷)
100	98, 99	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
101	100	ad3antrrr 727	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑄:𝐷–1-1-onto→𝐷)
102		f1oco 6846	. . . . . . . . 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 6846	. . . . . . . 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 6825	. . . . . . 7 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
107		funrel 6555	. . . . . . 7 ⊢ (Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
108	105, 106, 107	3syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
109		f1odm 6827	. . . . . . . 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 13662	. . . . . . . . 9 ⊢ (𝑃 ∈ (0...𝑁) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
112	90, 111	syl 17	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
113	112	ad3antrrr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
114	110, 113	eqtrd 2764	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
115		fzodisj 13663	. . . . . . 7 ⊢ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅
116		reldisjun 6022	. . . . . . 7 ⊢ ((Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ∧ dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)) ∧ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
117	115, 116	mp3an3 1446	. . . . . 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 6239	. . . . . . . 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 14475	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 Fn (0..^(♯‘𝑢)))
123	121, 122	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 Fn (0..^(♯‘𝑢)))
124	16	elin2d 4191	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ (^◡♯ “ {𝑃}))
125		hashf 14295	. . . . . . . . . . . . . . . 16 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
126		ffn 6707	. . . . . . . . . . . . . . . 16 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
127		fniniseg 7051	. . . . . . . . . . . . . . . 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 7417	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) = (0..^𝑃))
132	131	fneq2d 6633	. . . . . . . . . . 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 6824	. . . . . . . . . 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 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^𝑃))
138	137	ineq1d 4203	. . . . . . . . . . 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 2766	. . . . . . . . . 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 6651	. . . . . . . . 9 ⊢ ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)) = 𝑢)
143	134, 136, 141, 142	syl3anc 1368	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)) = 𝑢)
144	143	coeq2d 5852	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
145		resco 6239	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢))
146		resco 6239	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢))
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢)))
148		cnvun 6132	. . . . . . . . . . . . . . 15 ⊢ ^◡(𝑢 ∪ 𝑓) = (^◡𝑢 ∪ ^◡𝑓)
149	148	reseq1i 5967	. . . . . . . . . . . . . 14 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) = ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢)
150		f1ocnv 6835	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:dom 𝑢–1-1-onto→ran 𝑢 → ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢)
151		f1ofn 6824	. . . . . . . . . . . . . . . 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 6835	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → ^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢))
154		f1ofn 6824	. . . . . . . . . . . . . . . 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 6651	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑢 Fn ran 𝑢 ∧ ^◡𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢) = ^◡𝑢)
157	152, 155, 76, 156	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢) = ^◡𝑢)
158	149, 157	eqtr2id 2777	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢 = (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢))
159		simplr 766	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑀‘𝑢) = 𝑄)
160	159	reseq1d 5970	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = (𝑄 ↾ ran 𝑢))
161	158, 160	coeq12d 5854	. . . . . . . . . . . 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 32737	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
165	160, 164	eqtr3d 2766	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
166	165	rneqd 5927	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran ((𝑢 cyclShift 1) ∘ ^◡𝑢))
167		1zzd 12590	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 1 ∈ ℤ)
168		cshf1o 32593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷 ∧ 1 ∈ ℤ) → (𝑢 cyclShift 1):dom 𝑢–1-1-onto→ran 𝑢)
169	163, 69, 167, 168	syl3anc 1368	. . . . . . . . . . . . . . . . 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 6846	. . . . . . . . . . . . . . . . 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 6830	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢 → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–onto→ran 𝑢)
174		forn 6798	. . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran 𝑢)
177		ssid 3996	. . . . . . . . . . . . . 14 ⊢ ran 𝑢 ⊆ ran 𝑢
178	176, 177	eqsstrdi 4028	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢)
179		cores 6238	. . . . . . . . . . . . 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 2769	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
182	145, 181	eqtrid 2776	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
183	182	coeq1d 5851	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢))
184		cores 6238	. . . . . . . . . 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 2764	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
187		cores 6238	. . . . . . . . 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 32781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
191	186, 188, 190	3eqtr3d 2772	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
192	120, 144, 191	3eqtrd 2768	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = (( I ↾ (0..^𝑃)) cyclShift 1))
193		resco 6239	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
194	137	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 = (0..^𝑃))
195	194	difeq2d 4114	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = ((0..^𝑁) ∖ (0..^𝑃)))
196		fzodif1 32473	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (0...𝑁) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
197	90, 196	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
198	197	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
199	195, 198	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = (𝑃..^𝑁))
200	199	reseq2d 5971	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
201		fnunres2 6652	. . . . . . . . . . 11 ⊢ ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
202	134, 136, 141, 201	syl3anc 1368	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
203	200, 202	eqtr3d 2766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)) = 𝑓)
204	203	coeq2d 5852	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
205	193, 204	eqtrid 2776	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
206	148	reseq1i 5967	. . . . . . . . . . . 12 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢))
207		fnunres2 6652	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 Fn ran 𝑢 ∧ ^◡𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
208	152, 155, 76, 207	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
209	206, 208	eqtrid 2776	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
210	159	reseq1d 5970	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
211	93, 162, 163, 69	tocycfvres2 32738	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
212	210, 211	eqtr3d 2766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
213	209, 212	coeq12d 5854	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))))
214	212	rneqd 5927	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ran ( I ↾ (𝐷 ∖ ran 𝑢)))
215		rnresi 6064	. . . . . . . . . . . . . 14 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) = (𝐷 ∖ ran 𝑢)
216	215	eqimssi 4034	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢)
217	214, 216	eqsstrdi 4028	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢))
218		cores 6238	. . . . . . . . . . . 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 6239	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
221	219, 220	eqtr4di 2782	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
222	213, 221	eqtr3d 2766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
223	222	coeq1d 5851	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓))
224		f1of 6823	. . . . . . . . . . . 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 6755	. . . . . . . . . . 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 5851	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (^◡𝑓 ∘ 𝑓))
229		f1ococnv1 6852	. . . . . . . . . 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 5971	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ( I ↾ ((0..^𝑁) ∖ dom 𝑢)) = ( I ↾ (𝑃..^𝑁)))
232	228, 230, 231	3eqtrd 2768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
233		f1of 6823	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢))
234		frn 6714	. . . . . . . . . 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 6238	. . . . . . . . 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 2773	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
239	205, 238	eqtrd 2764	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ( I ↾ (𝑃..^𝑁)))
240	192, 239	uneq12d 4156	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
241	118, 240	eqtrd 2764	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
242		vex 3470	. . . . . 6 ⊢ 𝑢 ∈ V
243		vex 3470	. . . . . 6 ⊢ 𝑓 ∈ V
244	242, 243	unex 7726	. . . . 5 ⊢ (𝑢 ∪ 𝑓) ∈ V
245		f1oeq1 6811	. . . . . 6 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (𝑞:(0..^𝑁)–1-1-onto→𝐷 ↔ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷))
246		cnveq 5863	. . . . . . . . 9 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ^◡𝑞 = ^◡(𝑢 ∪ 𝑓))
247	246	coeq1d 5851	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (^◡𝑞 ∘ 𝑄) = (^◡(𝑢 ∪ 𝑓) ∘ 𝑄))
248		id 22	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → 𝑞 = (𝑢 ∪ 𝑓))
249	247, 248	coeq12d 5854	. . . . . . 7 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
250	249	eqeq1d 2726	. . . . . 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 3588	. . . 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 1930	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
255		nfcv 2895	. . 3 ⊢ Ⅎ𝑢𝑀
256	93, 92, 94	tocycf 32744	. . . 4 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵)
257		ffn 6707	. . . 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 2835	. . 3 ⊢ (𝜑 → 𝑄 ∈ (𝑀 “ (^◡♯ “ {𝑃})))
260	255, 258, 259	fvelimad 6949	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))(𝑀‘𝑢) = 𝑄)
261	254, 260	r19.29a 3154	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 1533 ∃wex 1773 ∈ wcel 2098 {crab 3424 Vcvv 3466 ∖ cdif 3937 ∪ cun 3938 ∩ cin 3939 ⊆ wss 3940 ∅c0 4314 {csn 4620 class class class wbr 5138 I cid 5563 ^◡ccnv 5665 dom cdm 5666 ran crn 5667 ↾ cres 5668 “ cima 5669 ∘ ccom 5670 Rel wrel 5671 Fun wfun 6527 Fn wfn 6528 ⟶wf 6529 –1-1→wf1 6530 –onto→wfo 6531 –1-1-onto→wf1o 6532 ‘cfv 6533 (class class class)co 7401 Fincfn 8935 0cc0 11106 1c1 11107 +∞cpnf 11242 ≤ cle 11246 − cmin 11441 ℕ₀cn0 12469 ℤcz 12555 ℤ_≥cuz 12819 ...cfz 13481 ..^cfzo 13624 ♯chash 14287 Word cword 14461 cyclShift ccsh 14735 Basecbs 17143 +_gcplusg 17196 -_gcsg 18855 SymGrpcsymg 19276 toCycctocyc 32733

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-tp 4625 df-op 4627 df-uni 4900 df-int 4941 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-om 7849 df-1st 7968 df-2nd 7969 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-oadd 8465 df-er 8699 df-map 8818 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-inf 9434 df-dju 9892 df-card 9930 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-xnn0 12542 df-z 12556 df-uz 12820 df-rp 12972 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-hash 14288 df-word 14462 df-concat 14518 df-substr 14588 df-pfx 14618 df-csh 14736 df-struct 17079 df-sets 17096 df-slot 17114 df-ndx 17126 df-base 17144 df-ress 17173 df-plusg 17209 df-tset 17215 df-efmnd 18784 df-symg 19277 df-tocyc 32734

This theorem is referenced by: cycpmconjs 32783

W3C validator