cycpmcl

Description: Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	tocycval.1	$⊢ C = toCyc (D)$
	tocycfv.d	$⊢ φ \to D \in V$
	tocycfv.w	$⊢ φ \to W \in Word D$
	tocycfv.1	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
	cycpmcl.s	$⊢ S = SymGrp (D)$
Assertion	cycpmcl	$⊢ φ \to C (W) \in {Base}_{S}$

Proof

Step	Hyp	Ref	Expression
1		tocycval.1	$⊢ C = toCyc (D)$
2		tocycfv.d	$⊢ φ \to D \in V$
3		tocycfv.w	$⊢ φ \to W \in Word D$
4		tocycfv.1	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
5		cycpmcl.s	$⊢ S = SymGrp (D)$
6		f1oi	$⊢ ({I ↾}_{(D ∖ ran W)}) : D ∖ ran W \underset{1-1 onto}{⟶} D ∖ ran W$
7	6	a1i	$⊢ φ \to ({I ↾}_{(D ∖ ran W)}) : D ∖ ran W \underset{1-1 onto}{⟶} D ∖ ran W$
8		1zzd	$⊢ φ \to 1 \in ℤ$
9		cshwf	$⊢ (W \in Word D \land 1 \in ℤ) \to (W cyclShift 1) : (0 ..^\|W\|) ⟶ D$
10	3 8 9	syl2anc	$⊢ φ \to (W cyclShift 1) : (0 ..^\|W\|) ⟶ D$
11	10	ffnd	$⊢ φ \to (W cyclShift 1) Fn (0 ..^\|W\|)$
12		df-f1	$⊢ W : dom W \underset{1-1}{⟶} D \leftrightarrow (W : dom W ⟶ D \land Fun W^{-1})$
13	4 12	sylib	$⊢ φ \to (W : dom W ⟶ D \land Fun W^{-1})$
14	13	simprd	$⊢ φ \to Fun W^{-1}$
15		eqid	$⊢ W cyclShift 1 = W cyclShift 1$
16		cshinj	$⊢ (W \in Word D \land Fun W^{-1} \land 1 \in ℤ) \to (W cyclShift 1 = W cyclShift 1 \to Fun {(W cyclShift 1)}^{-1})$
17	15 16	mpi	$⊢ (W \in Word D \land Fun W^{-1} \land 1 \in ℤ) \to Fun {(W cyclShift 1)}^{-1}$
18	3 14 8 17	syl3anc	$⊢ φ \to Fun {(W cyclShift 1)}^{-1}$
19		f1orn	$⊢ (W cyclShift 1) : (0 ..^\|W\|) \underset{1-1 onto}{⟶} ran (W cyclShift 1) \leftrightarrow ((W cyclShift 1) Fn (0 ..^\|W\|) \land Fun {(W cyclShift 1)}^{-1})$
20	11 18 19	sylanbrc	$⊢ φ \to (W cyclShift 1) : (0 ..^\|W\|) \underset{1-1 onto}{⟶} ran (W cyclShift 1)$
21		eqidd	$⊢ φ \to W cyclShift 1 = W cyclShift 1$
22		wrdf	$⊢ W \in Word D \to W : (0 ..^\|W\|) ⟶ D$
23	3 22	syl	$⊢ φ \to W : (0 ..^\|W\|) ⟶ D$
24	23	fdmd	$⊢ φ \to dom W = (0 ..^\|W\|)$
25		cshwrnid	$⊢ (W \in Word D \land 1 \in ℤ) \to ran (W cyclShift 1) = ran W$
26	3 8 25	syl2anc	$⊢ φ \to ran (W cyclShift 1) = ran W$
27	26	eqcomd	$⊢ φ \to ran W = ran (W cyclShift 1)$
28	21 24 27	f1oeq123d	$⊢ φ \to ((W cyclShift 1) : dom W \underset{1-1 onto}{⟶} ran W \leftrightarrow (W cyclShift 1) : (0 ..^\|W\|) \underset{1-1 onto}{⟶} ran (W cyclShift 1))$
29	20 28	mpbird	$⊢ φ \to (W cyclShift 1) : dom W \underset{1-1 onto}{⟶} ran W$
30		f1f1orn	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W \underset{1-1 onto}{⟶} ran W$
31		f1ocnv	$⊢ W : dom W \underset{1-1 onto}{⟶} ran W \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
32	4 30 31	3syl	$⊢ φ \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
33		f1oco	$⊢ ((W cyclShift 1) : dom W \underset{1-1 onto}{⟶} ran W \land W^{-1} : ran W \underset{1-1 onto}{⟶} dom W) \to ((W cyclShift 1) \circ W^{-1}) : ran W \underset{1-1 onto}{⟶} ran W$
34	29 32 33	syl2anc	$⊢ φ \to ((W cyclShift 1) \circ W^{-1}) : ran W \underset{1-1 onto}{⟶} ran W$
35		incom	$⊢ ran W \cap (D ∖ ran W) = (D ∖ ran W) \cap ran W$
36		disjdif	$⊢ ran W \cap (D ∖ ran W) = \emptyset$
37	35 36	eqtr3i	$⊢ (D ∖ ran W) \cap ran W = \emptyset$
38	37	a1i	$⊢ φ \to (D ∖ ran W) \cap ran W = \emptyset$
39		f1oun	$⊢ ((({I ↾}_{(D ∖ ran W)}) : D ∖ ran W \underset{1-1 onto}{⟶} D ∖ ran W \land ((W cyclShift 1) \circ W^{-1}) : ran W \underset{1-1 onto}{⟶} ran W) \land ((D ∖ ran W) \cap ran W = \emptyset \land (D ∖ ran W) \cap ran W = \emptyset)) \to (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) : (D ∖ ran W) \cup ran W \underset{1-1 onto}{⟶} (D ∖ ran W) \cup ran W$
40	7 34 38 38 39	syl22anc	$⊢ φ \to (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) : (D ∖ ran W) \cup ran W \underset{1-1 onto}{⟶} (D ∖ ran W) \cup ran W$
41	1 2 3 4	tocycfv	$⊢ φ \to C (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
42		uncom	$⊢ ran W \cup (D ∖ ran W) = (D ∖ ran W) \cup ran W$
43	23	frnd	$⊢ φ \to ran W \subseteq D$
44		undif	$⊢ ran W \subseteq D \leftrightarrow ran W \cup (D ∖ ran W) = D$
45	43 44	sylib	$⊢ φ \to ran W \cup (D ∖ ran W) = D$
46	42 45	syl5reqr	$⊢ φ \to D = (D ∖ ran W) \cup ran W$
47	41 46 46	f1oeq123d	$⊢ φ \to (C (W) : D \underset{1-1 onto}{⟶} D \leftrightarrow (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) : (D ∖ ran W) \cup ran W \underset{1-1 onto}{⟶} (D ∖ ran W) \cup ran W)$
48	40 47	mpbird	$⊢ φ \to C (W) : D \underset{1-1 onto}{⟶} D$
49		fvex	$⊢ C (W) \in V$
50		eqid	$⊢ {Base}_{S} = {Base}_{S}$
51	5 50	elsymgbas2	$⊢ C (W) \in V \to (C (W) \in {Base}_{S} \leftrightarrow C (W) : D \underset{1-1 onto}{⟶} D)$
52	49 51	ax-mp	$⊢ C (W) \in {Base}_{S} \leftrightarrow C (W) : D \underset{1-1 onto}{⟶} D$
53	48 52	sylibr	$⊢ φ \to C (W) \in {Base}_{S}$

Metamath Proof Explorer

Theorem cycpmcl

Proof