cycpmconjslem1

	Ref	Expression
Hypotheses	cycpmconjs.c	$⊢ C = M [{\|.\|}^{-1} [\{P\}]]$
	cycpmconjs.s	$⊢ S = SymGrp (D)$
	cycpmconjs.n	$⊢ N = \|D\|$
	cycpmconjs.m	$⊢ M = toCyc (D)$
	cycpmconjslem1.d	$⊢ φ \to D \in V$
	cycpmconjslem1.w	$⊢ φ \to W \in Word D$
	cycpmconjslem1.1	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
	cycpmconjslem1.2	$⊢ φ \to \|W\| = P$
Assertion	cycpmconjslem1	$⊢ φ \to (W^{-1} \circ M (W)) \circ W = ({I ↾}_{(0 ..^P)}) cyclShift 1$

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		cycpmconjslem1.d	$⊢ φ \to D \in V$
6		cycpmconjslem1.w	$⊢ φ \to W \in Word D$
7		cycpmconjslem1.1	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
8		cycpmconjslem1.2	$⊢ φ \to \|W\| = P$
9		resco	$⊢ {(W^{-1} \circ M (W)) ↾}_{ran W} = W^{-1} \circ ({M (W) ↾}_{ran W})$
10	9	coeq1i	$⊢ ({(W^{-1} \circ M (W)) ↾}_{ran W}) \circ W = (W^{-1} \circ ({M (W) ↾}_{ran W})) \circ W$
11		ssid	$⊢ ran W \subseteq ran W$
12		cores	$⊢ ran W \subseteq ran W \to ({(W^{-1} \circ M (W)) ↾}_{ran W}) \circ W = (W^{-1} \circ M (W)) \circ W$
13	11 12	ax-mp	$⊢ ({(W^{-1} \circ M (W)) ↾}_{ran W}) \circ W = (W^{-1} \circ M (W)) \circ W$
14		coass	$⊢ (W^{-1} \circ ({M (W) ↾}_{ran W})) \circ W = W^{-1} \circ (({M (W) ↾}_{ran W}) \circ W)$
15	10 13 14	3eqtr3i	$⊢ (W^{-1} \circ M (W)) \circ W = W^{-1} \circ (({M (W) ↾}_{ran W}) \circ W)$
16	4 5 6 7	tocycfvres1	$⊢ φ \to {M (W) ↾}_{ran W} = (W cyclShift 1) \circ W^{-1}$
17	16	coeq1d	$⊢ φ \to ({M (W) ↾}_{ran W}) \circ W = ((W cyclShift 1) \circ W^{-1}) \circ W$
18		coass	$⊢ ((W cyclShift 1) \circ W^{-1}) \circ W = (W cyclShift 1) \circ (W^{-1} \circ W)$
19		f1f1orn	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W \underset{1-1 onto}{⟶} ran W$
20		f1ococnv1	$⊢ W : dom W \underset{1-1 onto}{⟶} ran W \to W^{-1} \circ W = {I ↾}_{dom W}$
21	7 19 20	3syl	$⊢ φ \to W^{-1} \circ W = {I ↾}_{dom W}$
22	21	coeq2d	$⊢ φ \to (W cyclShift 1) \circ (W^{-1} \circ W) = (W cyclShift 1) \circ ({I ↾}_{dom W})$
23		coires1	$⊢ (W cyclShift 1) \circ ({I ↾}_{dom W}) = {(W cyclShift 1) ↾}_{dom W}$
24	22 23	eqtr2di	$⊢ φ \to {(W cyclShift 1) ↾}_{dom W} = (W cyclShift 1) \circ (W^{-1} \circ W)$
25	18 24	eqtr4id	$⊢ φ \to ((W cyclShift 1) \circ W^{-1}) \circ W = {(W cyclShift 1) ↾}_{dom W}$
26		1zzd	$⊢ φ \to 1 \in ℤ$
27		cshwfn	$⊢ (W \in Word D \land 1 \in ℤ) \to (W cyclShift 1) Fn (0 ..^\|W\|)$
28	6 26 27	syl2anc	$⊢ φ \to (W cyclShift 1) Fn (0 ..^\|W\|)$
29		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
30	6 29	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
31	30	fneq2d	$⊢ φ \to ((W cyclShift 1) Fn dom W \leftrightarrow (W cyclShift 1) Fn (0 ..^\|W\|))$
32	28 31	mpbird	$⊢ φ \to (W cyclShift 1) Fn dom W$
33		fnresdm	$⊢ (W cyclShift 1) Fn dom W \to {(W cyclShift 1) ↾}_{dom W} = W cyclShift 1$
34	32 33	syl	$⊢ φ \to {(W cyclShift 1) ↾}_{dom W} = W cyclShift 1$
35	17 25 34	3eqtrd	$⊢ φ \to ({M (W) ↾}_{ran W}) \circ W = W cyclShift 1$
36	35	coeq2d	$⊢ φ \to W^{-1} \circ (({M (W) ↾}_{ran W}) \circ W) = W^{-1} \circ (W cyclShift 1)$
37	15 36	eqtrid	$⊢ φ \to (W^{-1} \circ M (W)) \circ W = W^{-1} \circ (W cyclShift 1)$
38		wrdfn	$⊢ W \in Word D \to W Fn (0 ..^\|W\|)$
39	6 38	syl	$⊢ φ \to W Fn (0 ..^\|W\|)$
40		df-f	$⊢ W : (0 ..^\|W\|) ⟶ ran W \leftrightarrow (W Fn (0 ..^\|W\|) \land ran W \subseteq ran W)$
41	39 11 40	sylanblrc	$⊢ φ \to W : (0 ..^\|W\|) ⟶ ran W$
42		iswrdi	$⊢ W : (0 ..^\|W\|) ⟶ ran W \to W \in Word ran W$
43	41 42	syl	$⊢ φ \to W \in Word ran W$
44		f1ocnv	$⊢ W : dom W \underset{1-1 onto}{⟶} ran W \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
45		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
46	7 19 44 45	4syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
47		cshco	$⊢ (W \in Word ran W \land 1 \in ℤ \land W^{-1} : ran W ⟶ dom W) \to W^{-1} \circ (W cyclShift 1) = (W^{-1} \circ W) cyclShift 1$
48	43 26 46 47	syl3anc	$⊢ φ \to W^{-1} \circ (W cyclShift 1) = (W^{-1} \circ W) cyclShift 1$
49	8	oveq2d	$⊢ φ \to (0 ..^\|W\|) = (0 ..^P)$
50	30 49	eqtrd	$⊢ φ \to dom W = (0 ..^P)$
51	50	reseq2d	$⊢ φ \to {I ↾}_{dom W} = {I ↾}_{(0 ..^P)}$
52	21 51	eqtrd	$⊢ φ \to W^{-1} \circ W = {I ↾}_{(0 ..^P)}$
53	52	oveq1d	$⊢ φ \to (W^{-1} \circ W) cyclShift 1 = ({I ↾}_{(0 ..^P)}) cyclShift 1$
54	37 48 53	3eqtrd	$⊢ φ \to (W^{-1} \circ M (W)) \circ W = ({I ↾}_{(0 ..^P)}) cyclShift 1$

Metamath Proof Explorer

Theorem cycpmconjslem1

Proof