cycpmconjslem2

	Ref	Expression
Hypotheses	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	cycpmconjslem2	⊢ ( 𝜑 → ∃ 𝑞 ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ^◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cycpmconjs.c	⊢ 𝐶 = ( 𝑀 “ ( ^◡ ♯ “ { 𝑃 } ) )
2		cycpmconjs.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3		cycpmconjs.n	⊢ 𝑁 = ( ♯ ‘ 𝐷 )
4		cycpmconjs.m	⊢ 𝑀 = ( toCyc ‘ 𝐷 )
5		cycpmconjs.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
6		cycpmconjs.a	⊢ + = ( +_g ‘ 𝑆 )
7		cycpmconjs.l	⊢ − = ( -_g ‘ 𝑆 )
8		cycpmconjs.p	⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... 𝑁 ) )
9		cycpmconjs.d	⊢ ( 𝜑 → 𝐷 ∈ Fin )
10		cycpmconjs.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐶 )
11		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
12		diffi	⊢ ( ( 0 ..^ 𝑁 ) ∈ Fin → ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ∈ Fin )
13	11 12	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ∈ Fin )
14		diffi	⊢ ( 𝐷 ∈ Fin → ( 𝐷 ∖ ran 𝑢 ) ∈ Fin )
15	9 14	syl	⊢ ( 𝜑 → ( 𝐷 ∖ ran 𝑢 ) ∈ Fin )
16	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( 𝐷 ∖ ran 𝑢 ) ∈ Fin )
17		hashcl	⊢ ( 𝐷 ∈ Fin → ( ♯ ‘ 𝐷 ) ∈ ℕ₀ )
18	9 17	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) ∈ ℕ₀ )
19	3 18	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
20		hashfzo0	⊢ ( 𝑁 ∈ ℕ₀ → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
21	19 20	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
22	21 3	eqtrdi	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = ( ♯ ‘ 𝐷 ) )
23	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = ( ♯ ‘ 𝐷 ) )
24		simplr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) )
25	24	elin1d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
26		elrabi	⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } → 𝑢 ∈ Word 𝐷 )
27		wrdfin	⊢ ( 𝑢 ∈ Word 𝐷 → 𝑢 ∈ Fin )
28	25 26 27	3syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑢 ∈ Fin )
29		id	⊢ ( 𝑤 = 𝑢 → 𝑤 = 𝑢 )
30		dmeq	⊢ ( 𝑤 = 𝑢 → dom 𝑤 = dom 𝑢 )
31		eqidd	⊢ ( 𝑤 = 𝑢 → 𝐷 = 𝐷 )
32	29 30 31	f1eq123d	⊢ ( 𝑤 = 𝑢 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) )
33	32	elrab	⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑢 ∈ Word 𝐷 ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) )
34	33	simprbi	⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } → 𝑢 : dom 𝑢 –1-1→ 𝐷 )
35	25 34	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑢 : dom 𝑢 –1-1→ 𝐷 )
36		f1fun	⊢ ( 𝑢 : dom 𝑢 –1-1→ 𝐷 → Fun 𝑢 )
37	35 36	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → Fun 𝑢 )
38		hashfun	⊢ ( 𝑢 ∈ Fin → ( Fun 𝑢 ↔ ( ♯ ‘ 𝑢 ) = ( ♯ ‘ dom 𝑢 ) ) )
39	38	biimpa	⊢ ( ( 𝑢 ∈ Fin ∧ Fun 𝑢 ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ dom 𝑢 ) )
40	28 37 39	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ dom 𝑢 ) )
41	24	dmexd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → dom 𝑢 ∈ V )
42		hashf1rn	⊢ ( ( dom 𝑢 ∈ V ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ran 𝑢 ) )
43	41 35 42	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ran 𝑢 ) )
44	40 43	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ dom 𝑢 ) = ( ♯ ‘ ran 𝑢 ) )
45	23 44	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) − ( ♯ ‘ dom 𝑢 ) ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) )
46	11	a1i	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( 0 ..^ 𝑁 ) ∈ Fin )
47		wrddm	⊢ ( 𝑢 ∈ Word 𝐷 → dom 𝑢 = ( 0 ..^ ( ♯ ‘ 𝑢 ) ) )
48	25 26 47	3syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → dom 𝑢 = ( 0 ..^ ( ♯ ‘ 𝑢 ) ) )
49		hashcl	⊢ ( 𝑢 ∈ Fin → ( ♯ ‘ 𝑢 ) ∈ ℕ₀ )
50	25 26 27 49	4syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ 𝑢 ) ∈ ℕ₀ )
51	50	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ 𝑢 ) ∈ ℤ )
52	18	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) ∈ ℤ )
53	3 52	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
54	53	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑁 ∈ ℤ )
55	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝐷 ∈ Fin )
56		wrdf	⊢ ( 𝑢 ∈ Word 𝐷 → 𝑢 : ( 0 ..^ ( ♯ ‘ 𝑢 ) ) ⟶ 𝐷 )
57	56	frnd	⊢ ( 𝑢 ∈ Word 𝐷 → ran 𝑢 ⊆ 𝐷 )
58	25 26 57	3syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ran 𝑢 ⊆ 𝐷 )
59		hashss	⊢ ( ( 𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷 ) → ( ♯ ‘ ran 𝑢 ) ≤ ( ♯ ‘ 𝐷 ) )
60	55 58 59	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ ran 𝑢 ) ≤ ( ♯ ‘ 𝐷 ) )
61	3	a1i	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑁 = ( ♯ ‘ 𝐷 ) )
62	60 43 61	3brtr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ 𝑢 ) ≤ 𝑁 )
63		eluz1	⊢ ( ( ♯ ‘ 𝑢 ) ∈ ℤ → ( 𝑁 ∈ ( ℤ_≥ ‘ ( ♯ ‘ 𝑢 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑢 ) ≤ 𝑁 ) ) )
64	63	biimpar	⊢ ( ( ( ♯ ‘ 𝑢 ) ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑢 ) ≤ 𝑁 ) ) → 𝑁 ∈ ( ℤ_≥ ‘ ( ♯ ‘ 𝑢 ) ) )
65	51 54 62 64	syl12anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑁 ∈ ( ℤ_≥ ‘ ( ♯ ‘ 𝑢 ) ) )
66		fzoss2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ ( ♯ ‘ 𝑢 ) ) → ( 0 ..^ ( ♯ ‘ 𝑢 ) ) ⊆ ( 0 ..^ 𝑁 ) )
67	65 66	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( 0 ..^ ( ♯ ‘ 𝑢 ) ) ⊆ ( 0 ..^ 𝑁 ) )
68	48 67	eqsstrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → dom 𝑢 ⊆ ( 0 ..^ 𝑁 ) )
69		hashssdif	⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ dom 𝑢 ⊆ ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) − ( ♯ ‘ dom 𝑢 ) ) )
70	46 68 69	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) − ( ♯ ‘ dom 𝑢 ) ) )
71		hashssdif	⊢ ( ( 𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷 ) → ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) )
72	55 58 71	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) )
73	45 70 72	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) )
74		hasheqf1o	⊢ ( ( ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ∈ Fin ∧ ( 𝐷 ∖ ran 𝑢 ) ∈ Fin ) → ( ( ♯ ‘ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) ↔ ∃ 𝑓 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) )
75	74	biimpa	⊢ ( ( ( ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ∈ Fin ∧ ( 𝐷 ∖ ran 𝑢 ) ∈ Fin ) ∧ ( ♯ ‘ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) ) → ∃ 𝑓 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) )
76	13 16 73 75	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ∃ 𝑓 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) )
77	35	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 𝑢 : dom 𝑢 –1-1→ 𝐷 )
78		f1f1orn	⊢ ( 𝑢 : dom 𝑢 –1-1→ 𝐷 → 𝑢 : dom 𝑢 –1-1-onto→ ran 𝑢 )
79	77 78	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 𝑢 : dom 𝑢 –1-1-onto→ ran 𝑢 )
80		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) )
81		disjdif	⊢ ( dom 𝑢 ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ∅
82	81	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( dom 𝑢 ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ∅ )
83		disjdif	⊢ ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅
84	83	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅ )
85		f1oun	⊢ ( ( ( 𝑢 : dom 𝑢 –1-1-onto→ ran 𝑢 ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) ∧ ( ( dom 𝑢 ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ∅ ∧ ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅ ) ) → ( 𝑢 ∪ 𝑓 ) : ( dom 𝑢 ∪ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) –1-1-onto→ ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) )
86	79 80 82 84 85	syl22anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( 𝑢 ∪ 𝑓 ) : ( dom 𝑢 ∪ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) –1-1-onto→ ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) )
87		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( 𝑢 ∪ 𝑓 ) = ( 𝑢 ∪ 𝑓 ) )
88	68	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → dom 𝑢 ⊆ ( 0 ..^ 𝑁 ) )
89		undif	⊢ ( dom 𝑢 ⊆ ( 0 ..^ 𝑁 ) ↔ ( dom 𝑢 ∪ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( 0 ..^ 𝑁 ) )
90	88 89	sylib	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( dom 𝑢 ∪ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( 0 ..^ 𝑁 ) )
91		undif	⊢ ( ran 𝑢 ⊆ 𝐷 ↔ ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) = 𝐷 )
92	58 91	sylib	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) = 𝐷 )
93	92	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) = 𝐷 )
94	87 90 93	f1oeq123d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑢 ∪ 𝑓 ) : ( dom 𝑢 ∪ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) –1-1-onto→ ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) ↔ ( 𝑢 ∪ 𝑓 ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) )
95	86 94	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( 𝑢 ∪ 𝑓 ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 )
96		f1ocnv	⊢ ( ( 𝑢 ∪ 𝑓 ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 → ^◡ ( 𝑢 ∪ 𝑓 ) : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) )
97	95 96	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ^◡ ( 𝑢 ∪ 𝑓 ) : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) )
98	1 2 3 4 5	cycpmgcl	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ⊆ 𝐵 )
99	9 8 98	syl2anc	⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
100	99 10	sseldd	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
101	2 5	symgbasf1o	⊢ ( 𝑄 ∈ 𝐵 → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
102	100 101	syl	⊢ ( 𝜑 → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
103	102	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
104		f1oco	⊢ ( ( ^◡ ( 𝑢 ∪ 𝑓 ) : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) ∧ 𝑄 : 𝐷 –1-1-onto→ 𝐷 ) → ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) )
105	97 103 104	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) )
106		f1oco	⊢ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) ∧ ( 𝑢 ∪ 𝑓 ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
107	105 95 106	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
108		f1ofun	⊢ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) → Fun ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) )
109		funrel	⊢ ( Fun ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) → Rel ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) )
110	107 108 109	3syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → Rel ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) )
111		f1odm	⊢ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) → dom ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( 0 ..^ 𝑁 ) )
112	107 111	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → dom ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( 0 ..^ 𝑁 ) )
113		fzosplit	⊢ ( 𝑃 ∈ ( 0 ... 𝑁 ) → ( 0 ..^ 𝑁 ) = ( ( 0 ..^ 𝑃 ) ∪ ( 𝑃 ..^ 𝑁 ) ) )
114	8 113	syl	⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) = ( ( 0 ..^ 𝑃 ) ∪ ( 𝑃 ..^ 𝑁 ) ) )
115	114	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( 0 ..^ 𝑁 ) = ( ( 0 ..^ 𝑃 ) ∪ ( 𝑃 ..^ 𝑁 ) ) )
116	112 115	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → dom ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( 0 ..^ 𝑃 ) ∪ ( 𝑃 ..^ 𝑁 ) ) )
117		fzodisj	⊢ ( ( 0 ..^ 𝑃 ) ∩ ( 𝑃 ..^ 𝑁 ) ) = ∅
118		reldisjun	⊢ ( ( Rel ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ∧ dom ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( 0 ..^ 𝑃 ) ∪ ( 𝑃 ..^ 𝑁 ) ) ∧ ( ( 0 ..^ 𝑃 ) ∩ ( 𝑃 ..^ 𝑁 ) ) = ∅ ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 0 ..^ 𝑃 ) ) ∪ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 𝑃 ..^ 𝑁 ) ) ) )
119	117 118	mp3an3	⊢ ( ( Rel ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ∧ dom ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( 0 ..^ 𝑃 ) ∪ ( 𝑃 ..^ 𝑁 ) ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 0 ..^ 𝑃 ) ) ∪ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 𝑃 ..^ 𝑁 ) ) ) )
120	110 116 119	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 0 ..^ 𝑃 ) ) ∪ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 𝑃 ..^ 𝑁 ) ) ) )
121		resco	⊢ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 0 ..^ 𝑃 ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( ( 𝑢 ∪ 𝑓 ) ↾ ( 0 ..^ 𝑃 ) ) )
122	121	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 0 ..^ 𝑃 ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( ( 𝑢 ∪ 𝑓 ) ↾ ( 0 ..^ 𝑃 ) ) ) )
123	25 26	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑢 ∈ Word 𝐷 )
124		wrdfn	⊢ ( 𝑢 ∈ Word 𝐷 → 𝑢 Fn ( 0 ..^ ( ♯ ‘ 𝑢 ) ) )
125	123 124	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑢 Fn ( 0 ..^ ( ♯ ‘ 𝑢 ) ) )
126	24	elin2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑢 ∈ ( ^◡ ♯ “ { 𝑃 } ) )
127		hashf	⊢ ♯ : V ⟶ ( ℕ₀ ∪ { +∞ } )
128		ffn	⊢ ( ♯ : V ⟶ ( ℕ₀ ∪ { +∞ } ) → ♯ Fn V )
129		fniniseg	⊢ ( ♯ Fn V → ( 𝑢 ∈ ( ^◡ ♯ “ { 𝑃 } ) ↔ ( 𝑢 ∈ V ∧ ( ♯ ‘ 𝑢 ) = 𝑃 ) ) )
130	127 128 129	mp2b	⊢ ( 𝑢 ∈ ( ^◡ ♯ “ { 𝑃 } ) ↔ ( 𝑢 ∈ V ∧ ( ♯ ‘ 𝑢 ) = 𝑃 ) )
131	130	simprbi	⊢ ( 𝑢 ∈ ( ^◡ ♯ “ { 𝑃 } ) → ( ♯ ‘ 𝑢 ) = 𝑃 )
132	126 131	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ♯ ‘ 𝑢 ) = 𝑃 )
133	132	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( 0 ..^ ( ♯ ‘ 𝑢 ) ) = ( 0 ..^ 𝑃 ) )
134	133	fneq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( 𝑢 Fn ( 0 ..^ ( ♯ ‘ 𝑢 ) ) ↔ 𝑢 Fn ( 0 ..^ 𝑃 ) ) )
135	125 134	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → 𝑢 Fn ( 0 ..^ 𝑃 ) )
136	135	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 𝑢 Fn ( 0 ..^ 𝑃 ) )
137		f1ofn	⊢ ( 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) → 𝑓 Fn ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) )
138	80 137	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 𝑓 Fn ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) )
139	48 133	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → dom 𝑢 = ( 0 ..^ 𝑃 ) )
140	139	ineq1d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( dom 𝑢 ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( ( 0 ..^ 𝑃 ) ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) )
141	81	a1i	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( dom 𝑢 ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ∅ )
142	140 141	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ( ( 0 ..^ 𝑃 ) ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ∅ )
143	142	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 0 ..^ 𝑃 ) ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ∅ )
144		fnunres1	⊢ ( ( 𝑢 Fn ( 0 ..^ 𝑃 ) ∧ 𝑓 Fn ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ∧ ( ( 0 ..^ 𝑃 ) ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ∅ ) → ( ( 𝑢 ∪ 𝑓 ) ↾ ( 0 ..^ 𝑃 ) ) = 𝑢 )
145	136 138 143 144	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑢 ∪ 𝑓 ) ↾ ( 0 ..^ 𝑃 ) ) = 𝑢 )
146	145	coeq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( ( 𝑢 ∪ 𝑓 ) ↾ ( 0 ..^ 𝑃 ) ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑢 ) )
147		resco	⊢ ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ran 𝑢 ) = ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ ( 𝑄 ↾ ran 𝑢 ) )
148		resco	⊢ ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ↾ ran 𝑢 ) = ( ^◡ 𝑢 ∘ ( ( 𝑀 ‘ 𝑢 ) ↾ ran 𝑢 ) )
149	148	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ↾ ran 𝑢 ) = ( ^◡ 𝑢 ∘ ( ( 𝑀 ‘ 𝑢 ) ↾ ran 𝑢 ) ) )
150		cnvun	⊢ ^◡ ( 𝑢 ∪ 𝑓 ) = ( ^◡ 𝑢 ∪ ^◡ 𝑓 )
151	150	reseq1i	⊢ ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ran 𝑢 ) = ( ( ^◡ 𝑢 ∪ ^◡ 𝑓 ) ↾ ran 𝑢 )
152		f1ocnv	⊢ ( 𝑢 : dom 𝑢 –1-1-onto→ ran 𝑢 → ^◡ 𝑢 : ran 𝑢 –1-1-onto→ dom 𝑢 )
153		f1ofn	⊢ ( ^◡ 𝑢 : ran 𝑢 –1-1-onto→ dom 𝑢 → ^◡ 𝑢 Fn ran 𝑢 )
154	79 152 153	3syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ^◡ 𝑢 Fn ran 𝑢 )
155		f1ocnv	⊢ ( 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) → ^◡ 𝑓 : ( 𝐷 ∖ ran 𝑢 ) –1-1-onto→ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) )
156		f1ofn	⊢ ( ^◡ 𝑓 : ( 𝐷 ∖ ran 𝑢 ) –1-1-onto→ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) → ^◡ 𝑓 Fn ( 𝐷 ∖ ran 𝑢 ) )
157	80 155 156	3syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ^◡ 𝑓 Fn ( 𝐷 ∖ ran 𝑢 ) )
158		fnunres1	⊢ ( ( ^◡ 𝑢 Fn ran 𝑢 ∧ ^◡ 𝑓 Fn ( 𝐷 ∖ ran 𝑢 ) ∧ ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅ ) → ( ( ^◡ 𝑢 ∪ ^◡ 𝑓 ) ↾ ran 𝑢 ) = ^◡ 𝑢 )
159	154 157 84 158	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ 𝑢 ∪ ^◡ 𝑓 ) ↾ ran 𝑢 ) = ^◡ 𝑢 )
160	151 159	syl5req	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ^◡ 𝑢 = ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ran 𝑢 ) )
161		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( 𝑀 ‘ 𝑢 ) = 𝑄 )
162	161	reseq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑀 ‘ 𝑢 ) ↾ ran 𝑢 ) = ( 𝑄 ↾ ran 𝑢 ) )
163	160 162	coeq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ^◡ 𝑢 ∘ ( ( 𝑀 ‘ 𝑢 ) ↾ ran 𝑢 ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ran 𝑢 ) ∘ ( 𝑄 ↾ ran 𝑢 ) ) )
164	55	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 𝐷 ∈ Fin )
165	123	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 𝑢 ∈ Word 𝐷 )
166	4 164 165 77	tocycfvres1	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑀 ‘ 𝑢 ) ↾ ran 𝑢 ) = ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) )
167	162 166	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( 𝑄 ↾ ran 𝑢 ) = ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) )
168	167	rneqd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ran ( 𝑄 ↾ ran 𝑢 ) = ran ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) )
169		1zzd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → 1 ∈ ℤ )
170		cshf1o	⊢ ( ( 𝑢 ∈ Word 𝐷 ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ∧ 1 ∈ ℤ ) → ( 𝑢 cyclShift 1 ) : dom 𝑢 –1-1-onto→ ran 𝑢 )
171	165 77 169 170	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( 𝑢 cyclShift 1 ) : dom 𝑢 –1-1-onto→ ran 𝑢 )
172	79 152	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ^◡ 𝑢 : ran 𝑢 –1-1-onto→ dom 𝑢 )
173		f1oco	⊢ ( ( ( 𝑢 cyclShift 1 ) : dom 𝑢 –1-1-onto→ ran 𝑢 ∧ ^◡ 𝑢 : ran 𝑢 –1-1-onto→ dom 𝑢 ) → ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) : ran 𝑢 –1-1-onto→ ran 𝑢 )
174	171 172 173	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) : ran 𝑢 –1-1-onto→ ran 𝑢 )
175		f1ofo	⊢ ( ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) : ran 𝑢 –1-1-onto→ ran 𝑢 → ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) : ran 𝑢 –onto→ ran 𝑢 )
176		forn	⊢ ( ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) : ran 𝑢 –onto→ ran 𝑢 → ran ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) = ran 𝑢 )
177	174 175 176	3syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ran ( ( 𝑢 cyclShift 1 ) ∘ ^◡ 𝑢 ) = ran 𝑢 )
178	168 177	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ran ( 𝑄 ↾ ran 𝑢 ) = ran 𝑢 )
179		ssid	⊢ ran 𝑢 ⊆ ran 𝑢
180	178 179	eqsstrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ran ( 𝑄 ↾ ran 𝑢 ) ⊆ ran 𝑢 )
181		cores	⊢ ( ran ( 𝑄 ↾ ran 𝑢 ) ⊆ ran 𝑢 → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ran 𝑢 ) ∘ ( 𝑄 ↾ ran 𝑢 ) ) = ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ ( 𝑄 ↾ ran 𝑢 ) ) )
182	180 181	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ran 𝑢 ) ∘ ( 𝑄 ↾ ran 𝑢 ) ) = ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ ( 𝑄 ↾ ran 𝑢 ) ) )
183	149 163 182	3eqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ ( 𝑄 ↾ ran 𝑢 ) ) = ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ↾ ran 𝑢 ) )
184	147 183	syl5eq	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ran 𝑢 ) = ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ↾ ran 𝑢 ) )
185	184	coeq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ran 𝑢 ) ∘ 𝑢 ) = ( ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ↾ ran 𝑢 ) ∘ 𝑢 ) )
186		cores	⊢ ( ran 𝑢 ⊆ ran 𝑢 → ( ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ↾ ran 𝑢 ) ∘ 𝑢 ) = ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ∘ 𝑢 ) )
187	179 186	mp1i	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ↾ ran 𝑢 ) ∘ 𝑢 ) = ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ∘ 𝑢 ) )
188	185 187	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ran 𝑢 ) ∘ 𝑢 ) = ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ∘ 𝑢 ) )
189		cores	⊢ ( ran 𝑢 ⊆ ran 𝑢 → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ran 𝑢 ) ∘ 𝑢 ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑢 ) )
190	179 189	mp1i	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ran 𝑢 ) ∘ 𝑢 ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑢 ) )
191	132	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ♯ ‘ 𝑢 ) = 𝑃 )
192	1 2 3 4 164 165 77 191	cycpmconjslem1	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ 𝑢 ∘ ( 𝑀 ‘ 𝑢 ) ) ∘ 𝑢 ) = ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) )
193	188 190 192	3eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑢 ) = ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) )
194	122 146 193	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 0 ..^ 𝑃 ) ) = ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) )
195		resco	⊢ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 𝑃 ..^ 𝑁 ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( ( 𝑢 ∪ 𝑓 ) ↾ ( 𝑃 ..^ 𝑁 ) ) )
196	139	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → dom 𝑢 = ( 0 ..^ 𝑃 ) )
197	196	difeq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) = ( ( 0 ..^ 𝑁 ) ∖ ( 0 ..^ 𝑃 ) ) )
198		fzodif1	⊢ ( 𝑃 ∈ ( 0 ... 𝑁 ) → ( ( 0 ..^ 𝑁 ) ∖ ( 0 ..^ 𝑃 ) ) = ( 𝑃 ..^ 𝑁 ) )
199	8 198	syl	⊢ ( 𝜑 → ( ( 0 ..^ 𝑁 ) ∖ ( 0 ..^ 𝑃 ) ) = ( 𝑃 ..^ 𝑁 ) )
200	199	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 0 ..^ 𝑁 ) ∖ ( 0 ..^ 𝑃 ) ) = ( 𝑃 ..^ 𝑁 ) )
201	197 200	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) = ( 𝑃 ..^ 𝑁 ) )
202	201	reseq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑢 ∪ 𝑓 ) ↾ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( ( 𝑢 ∪ 𝑓 ) ↾ ( 𝑃 ..^ 𝑁 ) ) )
203		fnunres2	⊢ ( ( 𝑢 Fn ( 0 ..^ 𝑃 ) ∧ 𝑓 Fn ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ∧ ( ( 0 ..^ 𝑃 ) ∩ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ∅ ) → ( ( 𝑢 ∪ 𝑓 ) ↾ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = 𝑓 )
204	136 138 143 203	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑢 ∪ 𝑓 ) ↾ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = 𝑓 )
205	202 204	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑢 ∪ 𝑓 ) ↾ ( 𝑃 ..^ 𝑁 ) ) = 𝑓 )
206	205	coeq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( ( 𝑢 ∪ 𝑓 ) ↾ ( 𝑃 ..^ 𝑁 ) ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑓 ) )
207	195 206	syl5eq	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 𝑃 ..^ 𝑁 ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑓 ) )
208	150	reseq1i	⊢ ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( ( ^◡ 𝑢 ∪ ^◡ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) )
209		fnunres2	⊢ ( ( ^◡ 𝑢 Fn ran 𝑢 ∧ ^◡ 𝑓 Fn ( 𝐷 ∖ ran 𝑢 ) ∧ ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅ ) → ( ( ^◡ 𝑢 ∪ ^◡ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ^◡ 𝑓 )
210	154 157 84 209	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ 𝑢 ∪ ^◡ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ^◡ 𝑓 )
211	208 210	syl5eq	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ^◡ 𝑓 )
212	161	reseq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑀 ‘ 𝑢 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
213	4 164 165 77	tocycfvres2	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( 𝑀 ‘ 𝑢 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
214	212 213	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
215	211 214	coeq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∘ ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) = ( ^◡ 𝑓 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) )
216	214	rneqd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ran ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ran ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
217		rnresi	⊢ ran ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( 𝐷 ∖ ran 𝑢 )
218	217	eqimssi	⊢ ran ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ⊆ ( 𝐷 ∖ ran 𝑢 )
219	216 218	eqsstrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ran ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ⊆ ( 𝐷 ∖ ran 𝑢 ) )
220		cores	⊢ ( ran ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ⊆ ( 𝐷 ∖ ran 𝑢 ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∘ ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) = ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) )
221	219 220	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∘ ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) = ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) )
222		resco	⊢ ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
223	221 222	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∘ ( 𝑄 ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
224	215 223	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ^◡ 𝑓 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
225	224	coeq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ 𝑓 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) ∘ 𝑓 ) = ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∘ 𝑓 ) )
226		f1of	⊢ ( ^◡ 𝑓 : ( 𝐷 ∖ ran 𝑢 ) –1-1-onto→ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) → ^◡ 𝑓 : ( 𝐷 ∖ ran 𝑢 ) ⟶ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) )
227	80 155 226	3syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ^◡ 𝑓 : ( 𝐷 ∖ ran 𝑢 ) ⟶ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) )
228		fcoi1	⊢ ( ^◡ 𝑓 : ( 𝐷 ∖ ran 𝑢 ) ⟶ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) → ( ^◡ 𝑓 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) = ^◡ 𝑓 )
229	227 228	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ^◡ 𝑓 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) = ^◡ 𝑓 )
230	229	coeq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ 𝑓 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) ∘ 𝑓 ) = ( ^◡ 𝑓 ∘ 𝑓 ) )
231		f1ococnv1	⊢ ( 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) → ( ^◡ 𝑓 ∘ 𝑓 ) = ( I ↾ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) )
232	80 231	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ^◡ 𝑓 ∘ 𝑓 ) = ( I ↾ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) )
233	201	reseq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( I ↾ ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ) = ( I ↾ ( 𝑃 ..^ 𝑁 ) ) )
234	230 232 233	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ 𝑓 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ) ∘ 𝑓 ) = ( I ↾ ( 𝑃 ..^ 𝑁 ) ) )
235		f1of	⊢ ( 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) → 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ⟶ ( 𝐷 ∖ ran 𝑢 ) )
236		frn	⊢ ( 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) ⟶ ( 𝐷 ∖ ran 𝑢 ) → ran 𝑓 ⊆ ( 𝐷 ∖ ran 𝑢 ) )
237	80 235 236	3syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ran 𝑓 ⊆ ( 𝐷 ∖ ran 𝑢 ) )
238		cores	⊢ ( ran 𝑓 ⊆ ( 𝐷 ∖ ran 𝑢 ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∘ 𝑓 ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑓 ) )
239	237 238	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∘ 𝑓 ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑓 ) )
240	225 234 239	3eqtr3rd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ 𝑓 ) = ( I ↾ ( 𝑃 ..^ 𝑁 ) ) )
241	207 240	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 𝑃 ..^ 𝑁 ) ) = ( I ↾ ( 𝑃 ..^ 𝑁 ) ) )
242	194 241	uneq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 0 ..^ 𝑃 ) ) ∪ ( ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) ↾ ( 𝑃 ..^ 𝑁 ) ) ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) )
243	120 242	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) )
244		vex	⊢ 𝑢 ∈ V
245		vex	⊢ 𝑓 ∈ V
246	244 245	unex	⊢ ( 𝑢 ∪ 𝑓 ) ∈ V
247		f1oeq1	⊢ ( 𝑞 = ( 𝑢 ∪ 𝑓 ) → ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ↔ ( 𝑢 ∪ 𝑓 ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) )
248		cnveq	⊢ ( 𝑞 = ( 𝑢 ∪ 𝑓 ) → ^◡ 𝑞 = ^◡ ( 𝑢 ∪ 𝑓 ) )
249	248	coeq1d	⊢ ( 𝑞 = ( 𝑢 ∪ 𝑓 ) → ( ^◡ 𝑞 ∘ 𝑄 ) = ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) )
250		id	⊢ ( 𝑞 = ( 𝑢 ∪ 𝑓 ) → 𝑞 = ( 𝑢 ∪ 𝑓 ) )
251	249 250	coeq12d	⊢ ( 𝑞 = ( 𝑢 ∪ 𝑓 ) → ( ( ^◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) )
252	251	eqeq1d	⊢ ( 𝑞 = ( 𝑢 ∪ 𝑓 ) → ( ( ( ^◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ↔ ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )
253	247 252	anbi12d	⊢ ( 𝑞 = ( 𝑢 ∪ 𝑓 ) → ( ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ^◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ↔ ( ( 𝑢 ∪ 𝑓 ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ) )
254	246 253	spcev	⊢ ( ( ( 𝑢 ∪ 𝑓 ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ^◡ ( 𝑢 ∪ 𝑓 ) ∘ 𝑄 ) ∘ ( 𝑢 ∪ 𝑓 ) ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ∃ 𝑞 ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ^◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )
255	95 243 254	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) ∧ 𝑓 : ( ( 0 ..^ 𝑁 ) ∖ dom 𝑢 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑢 ) ) → ∃ 𝑞 ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ^◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )
256	76 255	exlimddv	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑄 ) → ∃ 𝑞 ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ^◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )
257		nfcv	⊢ Ⅎ 𝑢 𝑀
258	4 2 5	tocycf	⊢ ( 𝐷 ∈ Fin → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ 𝐵 )
259		ffn	⊢ ( 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ 𝐵 → 𝑀 Fn { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
260	9 258 259	3syl	⊢ ( 𝜑 → 𝑀 Fn { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
261	10 1	eleqtrdi	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑀 “ ( ^◡ ♯ “ { 𝑃 } ) ) )
262	257 260 261	fvelimad	⊢ ( 𝜑 → ∃ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ^◡ ♯ “ { 𝑃 } ) ) ( 𝑀 ‘ 𝑢 ) = 𝑄 )
263	256 262	r19.29a	⊢ ( 𝜑 → ∃ 𝑞 ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ^◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )

Metamath Proof Explorer

Theorem cycpmconjslem2

Proof