cycpmconjslem2

	Ref	Expression
Hypotheses	cycpmconjs.c	$⊢ C = M [{\|.\|}^{-1} [\{P\}]]$
	cycpmconjs.s	$⊢ S = SymGrp (D)$
	cycpmconjs.n	$⊢ N = \|D\|$
	cycpmconjs.m	$⊢ M = toCyc (D)$
	cycpmconjs.b	$⊢ B = {Base}_{S}$
	cycpmconjs.a	$⊢ \underset{˙}{+} = +_{S}$
	cycpmconjs.l	$⊢ \underset{˙}{-} = -_{S}$
	cycpmconjs.p	$⊢ φ \to P \in (0 \dots N)$
	cycpmconjs.d	$⊢ φ \to D \in Fin$
	cycpmconjs.q	$⊢ φ \to Q \in C$
Assertion	cycpmconjslem2	$⊢ φ \to \exists q (q : (0 ..^N) \underset{1-1 onto}{⟶} D \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)}))$

Proof

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

Metamath Proof Explorer

Theorem cycpmconjslem2

Proof