cycpmconjs

Description: All cycles of the same length are conjugate in the symmetric group. (Contributed by Thierry Arnoux, 14-Oct-2023)

	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$
	cycpmconjs.t	$⊢ φ \to T \in C$
Assertion	cycpmconjs	$⊢ φ \to \exists p \in B Q = (p \underset{˙}{+} T) \underset{˙}{-} p$

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		cycpmconjs.t	$⊢ φ \to T \in C$
12	1 2 3 4 5 6 7 8 9 10	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)}))$
13	1 2 3 4 5 6 7 8 9 11	cycpmconjslem2	$⊢ φ \to \exists t (t : (0 ..^N) \underset{1-1 onto}{⟶} D \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)}))$
14	13	ad2antrr	$⊢ ((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to \exists t (t : (0 ..^N) \underset{1-1 onto}{⟶} D \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)}))$
15	9	ad4antr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to D \in Fin$
16		simp-4r	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to q : (0 ..^N) \underset{1-1 onto}{⟶} D$
17		f1ocnv	$⊢ t : (0 ..^N) \underset{1-1 onto}{⟶} D \to t^{-1} : D \underset{1-1 onto}{⟶} (0 ..^N)$
18	17	ad2antlr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to t^{-1} : D \underset{1-1 onto}{⟶} (0 ..^N)$
19		f1oco	$⊢ (q : (0 ..^N) \underset{1-1 onto}{⟶} D \land t^{-1} : D \underset{1-1 onto}{⟶} (0 ..^N)) \to (q \circ t^{-1}) : D \underset{1-1 onto}{⟶} D$
20	16 18 19	syl2anc	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (q \circ t^{-1}) : D \underset{1-1 onto}{⟶} D$
21	2 5	elsymgbas	$⊢ D \in Fin \to (q \circ t^{-1} \in B \leftrightarrow (q \circ t^{-1}) : D \underset{1-1 onto}{⟶} D)$
22	21	biimpar	$⊢ (D \in Fin \land (q \circ t^{-1}) : D \underset{1-1 onto}{⟶} D) \to q \circ t^{-1} \in B$
23	15 20 22	syl2anc	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to q \circ t^{-1} \in B$
24		simpr	$⊢ (((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land p = q \circ t^{-1}) \to p = q \circ t^{-1}$
25	24	oveq1d	$⊢ (((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land p = q \circ t^{-1}) \to p \underset{˙}{+} T = (q \circ t^{-1}) \underset{˙}{+} T$
26	25 24	oveq12d	$⊢ (((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land p = q \circ t^{-1}) \to (p \underset{˙}{+} T) \underset{˙}{-} p = ((q \circ t^{-1}) \underset{˙}{+} T) \underset{˙}{-} (q \circ t^{-1})$
27	26	eqeq2d	$⊢ (((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land p = q \circ t^{-1}) \to (Q = (p \underset{˙}{+} T) \underset{˙}{-} p \leftrightarrow Q = ((q \circ t^{-1}) \underset{˙}{+} T) \underset{˙}{-} (q \circ t^{-1}))$
28		simpllr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})$
29		simpr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})$
30	28 29	eqtr4d	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (q^{-1} \circ Q) \circ q = (t^{-1} \circ T) \circ t$
31	30	coeq1d	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to ((q^{-1} \circ Q) \circ q) \circ q^{-1} = ((t^{-1} \circ T) \circ t) \circ q^{-1}$
32	31	coeq2d	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to q \circ (((q^{-1} \circ Q) \circ q) \circ q^{-1}) = q \circ (((t^{-1} \circ T) \circ t) \circ q^{-1})$
33		coass	$⊢ (q \circ (q^{-1} \circ Q)) \circ (q \circ q^{-1}) = q \circ ((q^{-1} \circ Q) \circ (q \circ q^{-1}))$
34		coass	$⊢ (q \circ q^{-1}) \circ Q = q \circ (q^{-1} \circ Q)$
35	34	coeq1i	$⊢ ((q \circ q^{-1}) \circ Q) \circ (q \circ q^{-1}) = (q \circ (q^{-1} \circ Q)) \circ (q \circ q^{-1})$
36		coass	$⊢ ((q^{-1} \circ Q) \circ q) \circ q^{-1} = (q^{-1} \circ Q) \circ (q \circ q^{-1})$
37	36	coeq2i	$⊢ q \circ (((q^{-1} \circ Q) \circ q) \circ q^{-1}) = q \circ ((q^{-1} \circ Q) \circ (q \circ q^{-1}))$
38	33 35 37	3eqtr4ri	$⊢ q \circ (((q^{-1} \circ Q) \circ q) \circ q^{-1}) = ((q \circ q^{-1}) \circ Q) \circ (q \circ q^{-1})$
39		f1ococnv2	$⊢ q : (0 ..^N) \underset{1-1 onto}{⟶} D \to q \circ q^{-1} = {I ↾}_{D}$
40	16 39	syl	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to q \circ q^{-1} = {I ↾}_{D}$
41	40	coeq1d	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (q \circ q^{-1}) \circ Q = ({I ↾}_{D}) \circ Q$
42	1 2 3 4 5	cycpmgcl	$⊢ (D \in Fin \land P \in (0 \dots N)) \to C \subseteq B$
43	9 8 42	syl2anc	$⊢ φ \to C \subseteq B$
44	43 10	sseldd	$⊢ φ \to Q \in B$
45	2 5	elsymgbas	$⊢ D \in Fin \to (Q \in B \leftrightarrow Q : D \underset{1-1 onto}{⟶} D)$
46	45	biimpa	$⊢ (D \in Fin \land Q \in B) \to Q : D \underset{1-1 onto}{⟶} D$
47	9 44 46	syl2anc	$⊢ φ \to Q : D \underset{1-1 onto}{⟶} D$
48		f1of	$⊢ Q : D \underset{1-1 onto}{⟶} D \to Q : D ⟶ D$
49		fcoi2	$⊢ Q : D ⟶ D \to ({I ↾}_{D}) \circ Q = Q$
50	47 48 49	3syl	$⊢ φ \to ({I ↾}_{D}) \circ Q = Q$
51	50	ad4antr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to ({I ↾}_{D}) \circ Q = Q$
52	41 51	eqtrd	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (q \circ q^{-1}) \circ Q = Q$
53	52 40	coeq12d	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to ((q \circ q^{-1}) \circ Q) \circ (q \circ q^{-1}) = Q \circ ({I ↾}_{D})$
54		fcoi1	$⊢ Q : D ⟶ D \to Q \circ ({I ↾}_{D}) = Q$
55	47 48 54	3syl	$⊢ φ \to Q \circ ({I ↾}_{D}) = Q$
56	55	ad4antr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to Q \circ ({I ↾}_{D}) = Q$
57	53 56	eqtrd	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to ((q \circ q^{-1}) \circ Q) \circ (q \circ q^{-1}) = Q$
58	38 57	syl5eq	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to q \circ (((q^{-1} \circ Q) \circ q) \circ q^{-1}) = Q$
59		coass	$⊢ (q \circ (t^{-1} \circ T)) \circ (t \circ q^{-1}) = q \circ ((t^{-1} \circ T) \circ (t \circ q^{-1}))$
60		coass	$⊢ (q \circ t^{-1}) \circ T = q \circ (t^{-1} \circ T)$
61	60	coeq1i	$⊢ ((q \circ t^{-1}) \circ T) \circ (t \circ q^{-1}) = (q \circ (t^{-1} \circ T)) \circ (t \circ q^{-1})$
62		coass	$⊢ ((t^{-1} \circ T) \circ t) \circ q^{-1} = (t^{-1} \circ T) \circ (t \circ q^{-1})$
63	62	coeq2i	$⊢ q \circ (((t^{-1} \circ T) \circ t) \circ q^{-1}) = q \circ ((t^{-1} \circ T) \circ (t \circ q^{-1}))$
64	59 61 63	3eqtr4i	$⊢ ((q \circ t^{-1}) \circ T) \circ (t \circ q^{-1}) = q \circ (((t^{-1} \circ T) \circ t) \circ q^{-1})$
65	43 11	sseldd	$⊢ φ \to T \in B$
66	65	ad4antr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to T \in B$
67	2 5 6	symgov	$⊢ (q \circ t^{-1} \in B \land T \in B) \to (q \circ t^{-1}) \underset{˙}{+} T = (q \circ t^{-1}) \circ T$
68	23 66 67	syl2anc	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (q \circ t^{-1}) \underset{˙}{+} T = (q \circ t^{-1}) \circ T$
69	68	oveq1d	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to ((q \circ t^{-1}) \underset{˙}{+} T) \underset{˙}{-} (q \circ t^{-1}) = ((q \circ t^{-1}) \circ T) \underset{˙}{-} (q \circ t^{-1})$
70	2	symggrp	$⊢ D \in Fin \to S \in Grp$
71	9 70	syl	$⊢ φ \to S \in Grp$
72	71	ad4antr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to S \in Grp$
73	5 6	grpcl	$⊢ (S \in Grp \land q \circ t^{-1} \in B \land T \in B) \to (q \circ t^{-1}) \underset{˙}{+} T \in B$
74	72 23 66 73	syl3anc	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (q \circ t^{-1}) \underset{˙}{+} T \in B$
75	68 74	eqeltrrd	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to (q \circ t^{-1}) \circ T \in B$
76	2 5 7	symgsubg	$⊢ ((q \circ t^{-1}) \circ T \in B \land q \circ t^{-1} \in B) \to ((q \circ t^{-1}) \circ T) \underset{˙}{-} (q \circ t^{-1}) = ((q \circ t^{-1}) \circ T) \circ {(q \circ t^{-1})}^{-1}$
77	75 23 76	syl2anc	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to ((q \circ t^{-1}) \circ T) \underset{˙}{-} (q \circ t^{-1}) = ((q \circ t^{-1}) \circ T) \circ {(q \circ t^{-1})}^{-1}$
78		cnvco	$⊢ {(q \circ t^{-1})}^{-1} = {t^{-1}}^{-1} \circ q^{-1}$
79		f1orel	$⊢ t : (0 ..^N) \underset{1-1 onto}{⟶} D \to Rel t$
80		dfrel2	$⊢ Rel t \leftrightarrow {t^{-1}}^{-1} = t$
81	79 80	sylib	$⊢ t : (0 ..^N) \underset{1-1 onto}{⟶} D \to {t^{-1}}^{-1} = t$
82	81	coeq1d	$⊢ t : (0 ..^N) \underset{1-1 onto}{⟶} D \to {t^{-1}}^{-1} \circ q^{-1} = t \circ q^{-1}$
83	78 82	syl5eq	$⊢ t : (0 ..^N) \underset{1-1 onto}{⟶} D \to {(q \circ t^{-1})}^{-1} = t \circ q^{-1}$
84	83	coeq2d	$⊢ t : (0 ..^N) \underset{1-1 onto}{⟶} D \to ((q \circ t^{-1}) \circ T) \circ {(q \circ t^{-1})}^{-1} = ((q \circ t^{-1}) \circ T) \circ (t \circ q^{-1})$
85	84	ad2antlr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to ((q \circ t^{-1}) \circ T) \circ {(q \circ t^{-1})}^{-1} = ((q \circ t^{-1}) \circ T) \circ (t \circ q^{-1})$
86	69 77 85	3eqtrrd	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to ((q \circ t^{-1}) \circ T) \circ (t \circ q^{-1}) = ((q \circ t^{-1}) \underset{˙}{+} T) \underset{˙}{-} (q \circ t^{-1})$
87	64 86	syl5eqr	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to q \circ (((t^{-1} \circ T) \circ t) \circ q^{-1}) = ((q \circ t^{-1}) \underset{˙}{+} T) \underset{˙}{-} (q \circ t^{-1})$
88	32 58 87	3eqtr3d	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to Q = ((q \circ t^{-1}) \underset{˙}{+} T) \underset{˙}{-} (q \circ t^{-1})$
89	23 27 88	rspcedvd	$⊢ ((((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land t : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to \exists p \in B Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
90	89	anasss	$⊢ (((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \land (t : (0 ..^N) \underset{1-1 onto}{⟶} D \land (t^{-1} \circ T) \circ t = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)}))) \to \exists p \in B Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
91	14 90	exlimddv	$⊢ ((φ \land q : (0 ..^N) \underset{1-1 onto}{⟶} D) \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)})) \to \exists p \in B Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
92	91	anasss	$⊢ (φ \land (q : (0 ..^N) \underset{1-1 onto}{⟶} D \land (q^{-1} \circ Q) \circ q = (({I ↾}_{(0 ..^P)}) cyclShift 1) \cup ({I ↾}_{(P ..^N)}))) \to \exists p \in B Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
93	12 92	exlimddv	$⊢ φ \to \exists p \in B Q = (p \underset{˙}{+} T) \underset{˙}{-} p$

Metamath Proof Explorer

Theorem cycpmconjs

Proof