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 33441

Description: Lemma for cycpmconjs 33442. (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 14009	. . . . 5 ⊢ (0..^𝑁) ∈ Fin
2		diffi 9158	. . . . 5 ⊢ ((0..^𝑁) ∈ Fin → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
3	1, 2	mp1i 14	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
4		cycpmconjs.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ Fin)
5		diffi 9158	. . . . . 6 ⊢ (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ Fin)
6	4, 5	syl 18	. . . . 5 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ Fin)
7	6	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (𝐷 ∖ ran 𝑢) ∈ Fin)
8		cycpmconjs.n	. . . . . . . . . 10 ⊢ 𝑁 = (♯‘𝐷)
9		hashcl 14391	. . . . . . . . . . 11 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
10	4, 9	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
11	8, 10	eqeltrid 2865	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
12		hashfzo0 14466	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0..^𝑁)) = 𝑁)
13	11, 12	syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0..^𝑁)) = 𝑁)
14	13, 8	eqtrdi 2812	. . . . . . 7 ⊢ (𝜑 → (♯‘(0..^𝑁)) = (♯‘𝐷))
15	14	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(0..^𝑁)) = (♯‘𝐷))
16		simplr 780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃})))
17	16	elin1d 4156	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
18		elrabi 3645	. . . . . . . . 9 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢 ∈ Word 𝐷)
19		wrdfin 14568	. . . . . . . . 9 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 ∈ Fin)
20	17, 18, 19	3syl 19	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ Fin)
21		id 23	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
22		dmeq 5893	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
23		eqidd 2762	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
24	21, 22, 23	f1eq123d 6812	. . . . . . . . . 10 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
25	24, 17	elrabrd 3652	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢:dom 𝑢–1-1→𝐷)
26		f1fun 6776	. . . . . . . . 9 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → Fun 𝑢)
27	25, 26	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → Fun 𝑢)
28		hashfundm 14478	. . . . . . . 8 ⊢ ((𝑢 ∈ Fin ∧ Fun 𝑢) → (♯‘𝑢) = (♯‘dom 𝑢))
29	20, 27, 28	syl2anc 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = (♯‘dom 𝑢))
30	16	dmexd 7899	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ∈ V)
31		hashf1rn 14387	. . . . . . . 8 ⊢ ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
32	30, 25, 31	syl2anc 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = (♯‘ran 𝑢))
33	29, 32	eqtr3d 2798	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘dom 𝑢) = (♯‘ran 𝑢))
34	15, 33	oveq12d 7428	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
35	1	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^𝑁) ∈ Fin)
36		wrddm 14557	. . . . . . . 8 ⊢ (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
37	17, 18, 36	3syl 19	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^(♯‘𝑢)))
38		hashcl 14391	. . . . . . . . . . 11 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
39	17, 18, 19, 38	4syl 20	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℕ₀)
40	39	nn0zd 12615	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ∈ ℤ)
41	10	nn0zd 12615	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐷) ∈ ℤ)
42	8, 41	eqeltrid 2865	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
43	42	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ ℤ)
44	4	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝐷 ∈ Fin)
45		wrdf 14554	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢:(0..^(♯‘𝑢))⟶𝐷)
46	45	frnd 6714	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → ran 𝑢 ⊆ 𝐷)
47	17, 18, 46	3syl 19	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ran 𝑢 ⊆ 𝐷)
48		hashss 14444	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
49	44, 47, 48	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
50	8	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 = (♯‘𝐷))
51	49, 32, 50	3brtr4d 5142	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) ≤ 𝑁)
52		eluz1 12865	. . . . . . . . . 10 ⊢ ((♯‘𝑢) ∈ ℤ → (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) ↔ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)))
53	52	biimpar 482	. . . . . . . . 9 ⊢ (((♯‘𝑢) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
54	40, 43, 51, 53	syl12anc 849	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑁 ∈ (ℤ_≥‘(♯‘𝑢)))
55		fzoss2 13715	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘(♯‘𝑢)) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
56	54, 55	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
57	37, 56	eqsstrd 3970	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 ⊆ (0..^𝑁))
58		hashssdif 14448	. . . . . 6 ⊢ (((0..^𝑁) ∈ Fin ∧ dom 𝑢 ⊆ (0..^𝑁)) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
59	35, 57, 58	syl2anc 595	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
60		hashssdif 14448	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
61	44, 47, 60	syl2anc 595	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
62	34, 59, 61	3eqtr4d 2806	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)))
63		hasheqf1o 14384	. . . . 5 ⊢ ((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) → ((♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)) ↔ ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)))
64	63	biimpa 481	. . . 4 ⊢ (((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) ∧ (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
65	3, 7, 62, 64	syl21anc 850	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
66	25	adantr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢–1-1→𝐷)
67		f1f1orn 6832	. . . . . . 7 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → 𝑢:dom 𝑢–1-1-onto→ran 𝑢)
68	66, 67	syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢–1-1-onto→ran 𝑢)
69		simpr 489	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
70		disjdif 4432	. . . . . . 7 ⊢ (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅
71	70	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
72		disjdif 4432	. . . . . . 7 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
73	72	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
74		f1oun 6840	. . . . . 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 𝑢)))
75	68, 69, 71, 73, 74	syl22anc 851	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
76		eqidd 2762	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓) = (𝑢 ∪ 𝑓))
77	57	adantr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 ⊆ (0..^𝑁))
78		undif 4442	. . . . . . 7 ⊢ (dom 𝑢 ⊆ (0..^𝑁) ↔ (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
79	77, 78	sylib 221	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
80		undif 4442	. . . . . . . 8 ⊢ (ran 𝑢 ⊆ 𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
81	47, 80	sylib 221	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
82	81	adantr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
83	76, 79, 82	f1oeq123d 6814	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) ↔ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷))
84	75, 83	mpbid 235	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷)
85		f1ocnv 6833	. . . . . . . . . 10 ⊢ ((𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷 → ^◡(𝑢 ∪ 𝑓):𝐷–1-1-onto→(0..^𝑁))
86	84, 85	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡(𝑢 ∪ 𝑓):𝐷–1-1-onto→(0..^𝑁))
87		cycpmconjs.p	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ (0...𝑁))
88		cycpmconjs.c	. . . . . . . . . . . . . 14 ⊢ 𝐶 = (𝑀 “ (^◡♯ “ {𝑃}))
89		cycpmconjs.s	. . . . . . . . . . . . . 14 ⊢ 𝑆 = (SymGrp‘𝐷)
90		cycpmconjs.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (toCyc‘𝐷)
91		cycpmconjs.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝑆)
92	88, 89, 8, 90, 91	cycpmgcl 33439	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑃 ∈ (0...𝑁)) → 𝐶 ⊆ 𝐵)
93	4, 87, 92	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
94		cycpmconjs.q	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ 𝐶)
95	93, 94	sseldd 3937	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ 𝐵)
96	89, 91	symgbasf1o 19444	. . . . . . . . . . 11 ⊢ (𝑄 ∈ 𝐵 → 𝑄:𝐷–1-1-onto→𝐷)
97	95, 96	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
98	97	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑄:𝐷–1-1-onto→𝐷)
99		f1oco 6844	. . . . . . . . 9 ⊢ ((^◡(𝑢 ∪ 𝑓):𝐷–1-1-onto→(0..^𝑁) ∧ 𝑄:𝐷–1-1-onto→𝐷) → (^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁))
100	86, 98, 99	syl2anc 595	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁))
101		f1oco 6844	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄):𝐷–1-1-onto→(0..^𝑁) ∧ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
102	100, 84, 101	syl2anc 595	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
103		f1ofun 6822	. . . . . . 7 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
104		funrel 6553	. . . . . . 7 ⊢ (Fun ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
105	102, 103, 104	3syl 19	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
106		f1odm 6824	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = (0..^𝑁))
107	102, 106	syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = (0..^𝑁))
108		fzosplit 13720	. . . . . . . . 9 ⊢ (𝑃 ∈ (0...𝑁) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
109	87, 108	syl 18	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
110	109	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
111	107, 110	eqtrd 2796	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
112		reldmun 6033	. . . . . 6 ⊢ ((Rel ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ∧ dom ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁))) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
113	105, 111, 112	syl2anc 595	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))))
114		resco 6251	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)))
115	114	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃))))
116	17, 18	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ Word 𝐷)
117		wrdfn 14564	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Word 𝐷 → 𝑢 Fn (0..^(♯‘𝑢)))
118	116, 117	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 Fn (0..^(♯‘𝑢)))
119	16	elin2d 4157	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 ∈ (^◡♯ “ {𝑃}))
120		hashf 14373	. . . . . . . . . . . . . . . 16 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
121		ffn 6705	. . . . . . . . . . . . . . . 16 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
122		fniniseg 7055	. . . . . . . . . . . . . . . 16 ⊢ (♯ Fn V → (𝑢 ∈ (^◡♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃)))
123	120, 121, 122	mp2b 10	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (^◡♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃))
124	123	simprbi 502	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (^◡♯ “ {𝑃}) → (♯‘𝑢) = 𝑃)
125	119, 124	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (♯‘𝑢) = 𝑃)
126	125	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (0..^(♯‘𝑢)) = (0..^𝑃))
127	126	fneq2d 6629	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (𝑢 Fn (0..^(♯‘𝑢)) ↔ 𝑢 Fn (0..^𝑃)))
128	118, 127	mpbid 235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → 𝑢 Fn (0..^𝑃))
129	128	adantr 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 Fn (0..^𝑃))
130		f1ofn 6821	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢))
131	69, 130	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢))
132	37, 126	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → dom 𝑢 = (0..^𝑃))
133	132	ineq1d 4171	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)))
134	70	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
135	133, 134	eqtr3d 2798	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
136	135	adantr 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
137		fnunres1 6647	. . . . . . . . 9 ⊢ ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)) = 𝑢)
138	129, 131, 136, 137	syl3anc 1396	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (0..^𝑃)) = 𝑢)
139	138	coeq2d 5848	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (0..^𝑃))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
140		resco 6251	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢))
141		resco 6251	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢))
142	141	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) = (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢)))
143		cnvun 6139	. . . . . . . . . . . . . . 15 ⊢ ^◡(𝑢 ∪ 𝑓) = (^◡𝑢 ∪ ^◡𝑓)
144	143	reseq1i 5974	. . . . . . . . . . . . . 14 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) = ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢)
145		f1ocnv 6833	. . . . . . . . . . . . . . . 16 ⊢ (𝑢:dom 𝑢–1-1-onto→ran 𝑢 → ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢)
146		f1ofn 6821	. . . . . . . . . . . . . . . 16 ⊢ (^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢 → ^◡𝑢 Fn ran 𝑢)
147	66, 67, 145, 146	4syl 20	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢 Fn ran 𝑢)
148		f1ocnv 6833	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → ^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢))
149		f1ofn 6821	. . . . . . . . . . . . . . . 16 ⊢ (^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢) → ^◡𝑓 Fn (𝐷 ∖ ran 𝑢))
150	69, 148, 149	3syl 19	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑓 Fn (𝐷 ∖ ran 𝑢))
151		fnunres1 6647	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑢 Fn ran 𝑢 ∧ ^◡𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢) = ^◡𝑢)
152	147, 150, 73, 151	syl3anc 1396	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∪ ^◡𝑓) ↾ ran 𝑢) = ^◡𝑢)
153	144, 152	eqtr2id 2809	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢 = (^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢))
154		simplr 780	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑀‘𝑢) = 𝑄)
155	154	reseq1d 5977	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = (𝑄 ↾ ran 𝑢))
156	153, 155	coeq12d 5850	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑢 ∘ ((𝑀‘𝑢) ↾ ran 𝑢)) = ((^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)))
157	44	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝐷 ∈ Fin)
158	116	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 ∈ Word 𝐷)
159	90, 157, 158, 66	tocycfvres1 33396	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
160	155, 159	eqtr3d 2798	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ ^◡𝑢))
161	160	rneqd 5928	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran ((𝑢 cyclShift 1) ∘ ^◡𝑢))
162		1zzd 12624	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 1 ∈ ℤ)
163		cshf1o 33248	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷 ∧ 1 ∈ ℤ) → (𝑢 cyclShift 1):dom 𝑢–1-1-onto→ran 𝑢)
164	158, 66, 162, 163	syl3anc 1396	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 cyclShift 1):dom 𝑢–1-1-onto→ran 𝑢)
165	68, 145	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢)
166		f1oco 6844	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑢 cyclShift 1):dom 𝑢–1-1-onto→ran 𝑢 ∧ ^◡𝑢:ran 𝑢–1-1-onto→dom 𝑢) → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢)
167	164, 165, 166	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢)
168		f1ofo 6828	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–1-1-onto→ran 𝑢 → ((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–onto→ran 𝑢)
169		forn 6795	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 cyclShift 1) ∘ ^◡𝑢):ran 𝑢–onto→ran 𝑢 → ran ((𝑢 cyclShift 1) ∘ ^◡𝑢) = ran 𝑢)
170	167, 168, 169	3syl 19	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran ((𝑢 cyclShift 1) ∘ ^◡𝑢) = ran 𝑢)
171	161, 170	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran 𝑢)
172		ssid 3958	. . . . . . . . . . . . . 14 ⊢ ran 𝑢 ⊆ ran 𝑢
173	171, 172	eqsstrdi 3980	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢)
174		cores 6250	. . . . . . . . . . . . 13 ⊢ (ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢 → ((^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)))
175	173, 174	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)))
176	142, 156, 175	3eqtrrd 2801	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ ran 𝑢)) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
177	140, 176	eqtrid 2808	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢))
178	177	coeq1d 5847	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢))
179		cores 6250	. . . . . . . . . 10 ⊢ (ran 𝑢 ⊆ ran 𝑢 → (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
180	172, 179	mp1i 14	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡𝑢 ∘ (𝑀‘𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
181	178, 180	eqtrd 2796	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢))
182		cores 6250	. . . . . . . . 9 ⊢ (ran 𝑢 ⊆ ran 𝑢 → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
183	172, 182	mp1i 14	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢))
184	125	adantr 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (♯‘𝑢) = 𝑃)
185	88, 89, 8, 90, 157, 158, 66, 184	cycpmconjslem1 33440	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∘ (𝑀‘𝑢)) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
186	181, 183, 185	3eqtr3d 2804	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
187	115, 139, 186	3eqtrd 2800	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) = (( I ↾ (0..^𝑃)) cyclShift 1))
188		resco 6251	. . . . . . . 8 ⊢ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
189	132	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 = (0..^𝑃))
190	189	difeq2d 4080	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = ((0..^𝑁) ∖ (0..^𝑃)))
191		fzodif1 33103	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (0...𝑁) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
192	87, 191	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
193	192	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
194	190, 193	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = (𝑃..^𝑁))
195	194	reseq2d 5978	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)))
196		fnunres2 6648	. . . . . . . . . . 11 ⊢ ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
197	129, 131, 136, 196	syl3anc 1396	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
198	195, 197	eqtr3d 2798	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁)) = 𝑓)
199	198	coeq2d 5848	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ ((𝑢 ∪ 𝑓) ↾ (𝑃..^𝑁))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
200	188, 199	eqtrid 2808	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
201	143	reseq1i 5974	. . . . . . . . . . . 12 ⊢ (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢))
202		fnunres2 6648	. . . . . . . . . . . . 13 ⊢ ((^◡𝑢 Fn ran 𝑢 ∧ ^◡𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
203	147, 150, 73, 202	syl3anc 1396	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑢 ∪ ^◡𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
204	201, 203	eqtrid 2808	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ^◡𝑓)
205	154	reseq1d 5977	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
206	90, 157, 158, 66	tocycfvres2 33397	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
207	205, 206	eqtr3d 2798	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
208	204, 207	coeq12d 5850	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))))
209	207	rneqd 5928	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ran ( I ↾ (𝐷 ∖ ran 𝑢)))
210		rnresi 6077	. . . . . . . . . . . . . 14 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) = (𝐷 ∖ ran 𝑢)
211	210	eqimssi 3996	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢)
212	209, 211	eqsstrdi 3980	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢))
213		cores 6250	. . . . . . . . . . . 12 ⊢ (ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))))
214	212, 213	syl 18	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))))
215		resco 6251	. . . . . . . . . . 11 ⊢ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) = (^◡(𝑢 ∪ 𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
216	214, 215	eqtr4di 2814	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
217	208, 216	eqtr3d 2798	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
218	217	coeq1d 5847	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓))
219		f1of 6820	. . . . . . . . . . 11 ⊢ (^◡𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢) → ^◡𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢))
220		fcoi1 6752	. . . . . . . . . . 11 ⊢ (^◡𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ^◡𝑓)
221	69, 148, 219, 220	4syl 20	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = ^◡𝑓)
222	221	coeq1d 5847	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (^◡𝑓 ∘ 𝑓))
223		f1ococnv1 6850	. . . . . . . . . 10 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → (^◡𝑓 ∘ 𝑓) = ( I ↾ ((0..^𝑁) ∖ dom 𝑢)))
224	69, 223	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (^◡𝑓 ∘ 𝑓) = ( I ↾ ((0..^𝑁) ∖ dom 𝑢)))
225	194	reseq2d 5978	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ( I ↾ ((0..^𝑁) ∖ dom 𝑢)) = ( I ↾ (𝑃..^𝑁)))
226	222, 224, 225	3eqtrd 2800	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
227		f1of 6820	. . . . . . . . 9 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢))
228		frn 6713	. . . . . . . . 9 ⊢ (𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢) → ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢))
229		cores 6250	. . . . . . . . 9 ⊢ (ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
230	69, 227, 228, 229	4syl 20	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓))
231	218, 226, 230	3eqtr3rd 2805	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
232	200, 231	eqtrd 2796	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁)) = ( I ↾ (𝑃..^𝑁)))
233	187, 232	uneq12d 4122	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (0..^𝑃)) ∪ (((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) ↾ (𝑃..^𝑁))) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
234	113, 233	eqtrd 2796	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
235		vex 3457	. . . . . 6 ⊢ 𝑢 ∈ V
236		vex 3457	. . . . . 6 ⊢ 𝑓 ∈ V
237	235, 236	unex 7742	. . . . 5 ⊢ (𝑢 ∪ 𝑓) ∈ V
238		f1oeq1 6808	. . . . . 6 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (𝑞:(0..^𝑁)–1-1-onto→𝐷 ↔ (𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷))
239		cnveq 5859	. . . . . . . . 9 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ^◡𝑞 = ^◡(𝑢 ∪ 𝑓))
240	239	coeq1d 5847	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (^◡𝑞 ∘ 𝑄) = (^◡(𝑢 ∪ 𝑓) ∘ 𝑄))
241		id 23	. . . . . . . 8 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → 𝑞 = (𝑢 ∪ 𝑓))
242	240, 241	coeq12d 5850	. . . . . . 7 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)))
243	242	eqeq1d 2763	. . . . . 6 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → (((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))) ↔ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
244	238, 243	anbi12d 643	. . . . 5 ⊢ (𝑞 = (𝑢 ∪ 𝑓) → ((𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) ↔ ((𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))))
245	237, 244	spcev 3564	. . . 4 ⊢ (((𝑢 ∪ 𝑓):(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡(𝑢 ∪ 𝑓) ∘ 𝑄) ∘ (𝑢 ∪ 𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
246	84, 234, 245	syl2anc 595	. . 3 ⊢ ((((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
247	65, 246	exlimddv 1963	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))) ∧ (𝑀‘𝑢) = 𝑄) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
248		nfcv 2923	. . 3 ⊢ Ⅎ𝑢𝑀
249	90, 89, 91	tocycf 33403	. . . 4 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵)
250		ffn 6705	. . . 4 ⊢ (𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
251	4, 249, 250	3syl 19	. . 3 ⊢ (𝜑 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
252	94, 88	eleqtrdi 2871	. . 3 ⊢ (𝜑 → 𝑄 ∈ (𝑀 “ (^◡♯ “ {𝑃})))
253	248, 251, 252	fvelimad 6948	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {𝑃}))(𝑀‘𝑢) = 𝑄)
254	247, 253	r19.29a 3171	1 ⊢ (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((^◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1568 ∃wex 1807 ∈ wcel 2141 {crab 3414 Vcvv 3453 ∖ cdif 3901 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 {csn 4588 class class class wbr 5108 I cid 5555 ^◡ccnv 5660 dom cdm 5661 ran crn 5662 ↾ cres 5663 “ cima 5664 ∘ ccom 5665 Rel wrel 5666 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 –onto→wfo 6534 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 Fincfn 8942 0cc0 11099 1c1 11100 +∞cpnf 11239 ≤ cle 11243 − cmin 11440 ℕ₀cn0 12503 ℤcz 12590 ℤ_≥cuz 12861 ...cfz 13534 ..^cfzo 13681 ♯chash 14365 Word cword 14549 cyclShift ccsh 14824 Basecbs 17268 +_gcplusg 17309 -_gcsg 19001 SymGrpcsymg 19438 toCycctocyc 33392

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-oadd 8456 df-er 8693 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-sup 9401 df-inf 9402 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-rp 13016 df-fz 13535 df-fzo 13682 df-fl 13824 df-mod 13902 df-hash 14366 df-word 14550 df-concat 14607 df-substr 14678 df-pfx 14708 df-csh 14825 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-tset 17328 df-efmnd 18927 df-symg 19439 df-tocyc 33393

This theorem is referenced by: cycpmconjs 33442

W3C validator