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 25	elrabrd	$⊢ ((φ \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$
34		f1fun	$⊢ u : dom u \underset{1-1}{⟶} D \to Fun u$
35	33 34	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$
36		hashfundm	$⊢ (u \in Fin \land Fun u) \to \|u\| = \|dom u\|$
37	28 35 36	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\|$
38	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$
39		hashf1rn	$⊢ (dom u \in V \land u : dom u \underset{1-1}{⟶} D) \to \|u\| = \|ran u\|$
40	38 33 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\| = \|ran u\|$
41	37 40	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\|$
42	23 41	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\|$
43	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$
44		wrddm	$⊢ u \in Word D \to dom u = (0 ..^\|u\|)$
45	25 26 44	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\|)$
46		hashcl	$⊢ u \in Fin \to \|u\| \in ℕ_{0}$
47	25 26 27 46	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}$
48	47	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 ℤ$
49	18	nn0zd	$⊢ φ \to \|D\| \in ℤ$
50	3 49	eqeltrid	$⊢ φ \to N \in ℤ$
51	50	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 ℤ$
52	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$
53		wrdf	$⊢ u \in Word D \to u : (0 ..^\|u\|) ⟶ D$
54	53	frnd	$⊢ u \in Word D \to ran u \subseteq D$
55	25 26 54	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$
56		hashss	$⊢ (D \in Fin \land ran u \subseteq D) \to \|ran u\| \leq \|D\|$
57	52 55 56	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\|$
58	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\|$
59	57 40 58	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$
60		eluz1	$⊢ \|u\| \in ℤ \to (N \in ℤ_{\geq \|u\|} \leftrightarrow (N \in ℤ \land \|u\| \leq N))$
61	60	biimpar	$⊢ (\|u\| \in ℤ \land (N \in ℤ \land \|u\| \leq N)) \to N \in ℤ_{\geq \|u\|}$
62	48 51 59 61	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\|}$
63		fzoss2	$⊢ N \in ℤ_{\geq \|u\|} \to (0 ..^\|u\|) \subseteq (0 ..^N)$
64	62 63	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)$
65	45 64	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)$
66		hashssdif	$⊢ ((0 ..^N) \in Fin \land dom u \subseteq (0 ..^N)) \to \|(0 ..^N) ∖ dom u\| = \|(0 ..^N)\| - \|dom u\|$
67	43 65 66	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\|$
68		hashssdif	$⊢ (D \in Fin \land ran u \subseteq D) \to \|D ∖ ran u\| = \|D\| - \|ran u\|$
69	52 55 68	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\|$
70	42 67 69	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\|$
71		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)$
72	71	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$
73	13 16 70 72	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$
74	33	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$
75		f1f1orn	$⊢ u : dom u \underset{1-1}{⟶} D \to u : dom u \underset{1-1 onto}{⟶} ran u$
76	74 75	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$
77		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$
78		disjdif	$⊢ dom u \cap ((0 ..^N) ∖ dom u) = \emptyset$
79	78	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$
80		disjdif	$⊢ ran u \cap (D ∖ ran u) = \emptyset$
81	80	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$
82		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)$
83	76 77 79 81 82	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)$
84		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$
85	65	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)$
86		undif	$⊢ dom u \subseteq (0 ..^N) \leftrightarrow dom u \cup ((0 ..^N) ∖ dom u) = (0 ..^N)$
87	85 86	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)$
88		undif	$⊢ ran u \subseteq D \leftrightarrow ran u \cup (D ∖ ran u) = D$
89	55 88	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$
90	89	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$
91	84 87 90	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)$
92	83 91	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$
93		f1ocnv	$⊢ (u \cup f) : (0 ..^N) \underset{1-1 onto}{⟶} D \to {(u \cup f)}^{-1} : D \underset{1-1 onto}{⟶} (0 ..^N)$
94	92 93	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)$
95	1 2 3 4 5	cycpmgcl	$⊢ (D \in Fin \land P \in (0 \dots N)) \to C \subseteq B$
96	9 8 95	syl2anc	$⊢ φ \to C \subseteq B$
97	96 10	sseldd	$⊢ φ \to Q \in B$
98	2 5	symgbasf1o	$⊢ Q \in B \to Q : D \underset{1-1 onto}{⟶} D$
99	97 98	syl	$⊢ φ \to Q : D \underset{1-1 onto}{⟶} D$
100	99	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$
101		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)$
102	94 100 101	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)$
103		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)$
104	102 92 103	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)$
105		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))$
106		funrel	$⊢ Fun (({(u \cup f)}^{-1} \circ Q) \circ (u \cup f)) \to Rel (({(u \cup f)}^{-1} \circ Q) \circ (u \cup f))$
107	104 105 106	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))$
108		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)$
109	104 108	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)$
110		fzosplit	$⊢ P \in (0 \dots N) \to (0 ..^N) = (0 ..^P) \cup (P ..^N)$
111	8 110	syl	$⊢ φ \to (0 ..^N) = (0 ..^P) \cup (P ..^N)$
112	111	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)$
113	109 112	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)$
114		reldmun	$⊢ (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)})$
115	107 113 114	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)})$
116		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)})$
117	116	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)})$
118	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$
119		wrdfn	$⊢ u \in Word D \to u Fn (0 ..^\|u\|)$
120	118 119	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\|)$
121	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\}]$
122		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
123		ffn	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to \|.\| Fn V$
124		fniniseg	$⊢ \|.\| Fn V \to (u \in {\|.\|}^{-1} [\{P\}] \leftrightarrow (u \in V \land \|u\| = P))$
125	122 123 124	mp2b	$⊢ u \in {\|.\|}^{-1} [\{P\}] \leftrightarrow (u \in V \land \|u\| = P)$
126	125	simprbi	$⊢ u \in {\|.\|}^{-1} [\{P\}] \to \|u\| = P$
127	121 126	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$
128	127	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)$
129	128	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))$
130	120 129	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)$
131	130	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)$
132		f1ofn	$⊢ f : (0 ..^N) ∖ dom u \underset{1-1 onto}{⟶} D ∖ ran u \to f Fn ((0 ..^N) ∖ dom u)$
133	77 132	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)$
134	45 128	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)$
135	134	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)$
136	78	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$
137	135 136	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$
138	137	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$
139		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$
140	131 133 138 139	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$
141	140	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$
142		resco	$⊢ {({(u \cup f)}^{-1} \circ Q) ↾}_{ran u} = {(u \cup f)}^{-1} \circ ({Q ↾}_{ran u})$
143		resco	$⊢ {(u^{-1} \circ M (u)) ↾}_{ran u} = u^{-1} \circ ({M (u) ↾}_{ran u})$
144	143	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})$
145		cnvun	$⊢ {(u \cup f)}^{-1} = u^{-1} \cup f^{-1}$
146	145	reseq1i	$⊢ {{(u \cup f)}^{-1} ↾}_{ran u} = {(u^{-1} \cup f^{-1}) ↾}_{ran u}$
147		f1ocnv	$⊢ u : dom u \underset{1-1 onto}{⟶} ran u \to u^{-1} : ran u \underset{1-1 onto}{⟶} dom u$
148		f1ofn	$⊢ u^{-1} : ran u \underset{1-1 onto}{⟶} dom u \to u^{-1} Fn ran u$
149	74 75 147 148	4syl	$⊢ (((φ \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$
150		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$
151		f1ofn	$⊢ f^{-1} : D ∖ ran u \underset{1-1 onto}{⟶} (0 ..^N) ∖ dom u \to f^{-1} Fn (D ∖ ran u)$
152	77 150 151	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)$
153		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}$
154	149 152 81 153	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}$
155	146 154	eqtr2id	$⊢ (((φ \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}$
156		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$
157	156	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}$
158	155 157	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})$
159	52	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$
160	118	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$
161	4 159 160 74	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}$
162	157 161	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}$
163	162	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})$
164		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 ℤ$
165		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$
166	160 74 164 165	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$
167	76 147	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$
168		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$
169	166 167 168	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$
170		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$
171		forn	$⊢ ((u cyclShift 1) \circ u^{-1}) : ran u \underset{onto}{⟶} ran u \to ran ((u cyclShift 1) \circ u^{-1}) = ran u$
172	169 170 171	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$
173	163 172	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$
174		ssid	$⊢ ran u \subseteq ran u$
175	173 174	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$
176		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})$
177	175 176	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})$
178	144 158 177	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}$
179	142 178	eqtrid	$⊢ (((φ \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}$
180	179	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$
181		cores	$⊢ ran u \subseteq ran u \to ({(u^{-1} \circ M (u)) ↾}_{ran u}) \circ u = (u^{-1} \circ M (u)) \circ u$
182	174 181	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$
183	180 182	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$
184		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$
185	174 184	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$
186	127	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$
187	1 2 3 4 159 160 74 186	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$
188	183 185 187	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$
189	117 141 188	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$
190		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)})$
191	134	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)$
192	191	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)$
193		fzodif1	$⊢ P \in (0 \dots N) \to (0 ..^N) ∖ (0 ..^P) = (P ..^N)$
194	8 193	syl	$⊢ φ \to (0 ..^N) ∖ (0 ..^P) = (P ..^N)$
195	194	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)$
196	192 195	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)$
197	196	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)}$
198		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$
199	131 133 138 198	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$
200	197 199	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$
201	200	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$
202	190 201	eqtrid	$⊢ (((φ \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$
203	145	reseq1i	$⊢ {{(u \cup f)}^{-1} ↾}_{(D ∖ ran u)} = {(u^{-1} \cup f^{-1}) ↾}_{(D ∖ ran u)}$
204		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}$
205	149 152 81 204	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}$
206	203 205	eqtrid	$⊢ (((φ \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}$
207	156	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)}$
208	4 159 160 74	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)}$
209	207 208	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)}$
210	206 209	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)})$
211	209	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)})$
212		rnresi	$⊢ ran ({I ↾}_{(D ∖ ran u)}) = D ∖ ran u$
213	212	eqimssi	$⊢ ran ({I ↾}_{(D ∖ ran u)}) \subseteq D ∖ ran u$
214	211 213	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$
215		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)})$
216	214 215	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)})$
217		resco	$⊢ {({(u \cup f)}^{-1} \circ Q) ↾}_{(D ∖ ran u)} = {(u \cup f)}^{-1} \circ ({Q ↾}_{(D ∖ ran u)})$
218	216 217	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)}$
219	210 218	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)}$
220	219	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$
221		f1of	$⊢ f^{-1} : D ∖ ran u \underset{1-1 onto}{⟶} (0 ..^N) ∖ dom u \to f^{-1} : D ∖ ran u ⟶ (0 ..^N) ∖ dom u$
222		fcoi1	$⊢ f^{-1} : D ∖ ran u ⟶ (0 ..^N) ∖ dom u \to f^{-1} \circ ({I ↾}_{(D ∖ ran u)}) = f^{-1}$
223	77 150 221 222	4syl	$⊢ (((φ \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}$
224	223	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$
225		f1ococnv1	$⊢ f : (0 ..^N) ∖ dom u \underset{1-1 onto}{⟶} D ∖ ran u \to f^{-1} \circ f = {I ↾}_{((0 ..^N) ∖ dom u)}$
226	77 225	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)}$
227	196	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)}$
228	224 226 227	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)}$
229		f1of	$⊢ f : (0 ..^N) ∖ dom u \underset{1-1 onto}{⟶} D ∖ ran u \to f : (0 ..^N) ∖ dom u ⟶ D ∖ ran u$
230		frn	$⊢ f : (0 ..^N) ∖ dom u ⟶ D ∖ ran u \to ran f \subseteq D ∖ ran u$
231		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$
232	77 229 230 231	4syl	$⊢ (((φ \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$
233	220 228 232	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)}$
234	202 233	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)}$
235	189 234	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)})$
236	115 235	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)})$
237		vex	$⊢ u \in V$
238		vex	$⊢ f \in V$
239	237 238	unex	$⊢ u \cup f \in V$
240		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)$
241		cnveq	$⊢ q = u \cup f \to q^{-1} = {(u \cup f)}^{-1}$
242	241	coeq1d	$⊢ q = u \cup f \to q^{-1} \circ Q = {(u \cup f)}^{-1} \circ Q$
243		id	$⊢ q = u \cup f \to q = u \cup f$
244	242 243	coeq12d	$⊢ q = u \cup f \to (q^{-1} \circ Q) \circ q = ({(u \cup f)}^{-1} \circ Q) \circ (u \cup f)$
245	244	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)}))$
246	240 245	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)})))$
247	239 246	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)}))$
248	92 236 247	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)}))$
249	73 248	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)}))$
250		nfcv	$⊢ \underline{Ⅎ} u M$
251	4 2 5	tocycf	$⊢ D \in Fin \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ B$
252		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\}$
253	9 251 252	3syl	$⊢ φ \to M Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
254	10 1	eleqtrdi	$⊢ φ \to Q \in M [{\|.\|}^{-1} [\{P\}]]$
255	250 253 254	fvelimad	$⊢ φ \to \exists u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}]) M (u) = Q$
256	249 255	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