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

Metamath Proof Explorer

Theorem cycpmconjslem2

Proof