tocycfv

Description: Function value of a permutation cycle built from a word. (Contributed by Thierry Arnoux, 18-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$
Assertion	tocycfv	$⊢ φ \to C (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$

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	1	tocycval	$⊢ D \in V \to C = (w \in \{u \in Word D \| u : dom u \underset{1-1}{⟶} D\} ⟼ ({I ↾}_{(D ∖ ran w)}) \cup ((w cyclShift 1) \circ w^{-1}))$
6	2 5	syl	$⊢ φ \to C = (w \in \{u \in Word D \| u : dom u \underset{1-1}{⟶} D\} ⟼ ({I ↾}_{(D ∖ ran w)}) \cup ((w cyclShift 1) \circ w^{-1}))$
7		simpr	$⊢ (φ \land w = W) \to w = W$
8	7	rneqd	$⊢ (φ \land w = W) \to ran w = ran W$
9	8	difeq2d	$⊢ (φ \land w = W) \to D ∖ ran w = D ∖ ran W$
10	9	reseq2d	$⊢ (φ \land w = W) \to {I ↾}_{(D ∖ ran w)} = {I ↾}_{(D ∖ ran W)}$
11	7	oveq1d	$⊢ (φ \land w = W) \to w cyclShift 1 = W cyclShift 1$
12	7	cnveqd	$⊢ (φ \land w = W) \to w^{-1} = W^{-1}$
13	11 12	coeq12d	$⊢ (φ \land w = W) \to (w cyclShift 1) \circ w^{-1} = (W cyclShift 1) \circ W^{-1}$
14	10 13	uneq12d	$⊢ (φ \land w = W) \to ({I ↾}_{(D ∖ ran w)}) \cup ((w cyclShift 1) \circ w^{-1}) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
15		id	$⊢ u = W \to u = W$
16		dmeq	$⊢ u = W \to dom u = dom W$
17		eqidd	$⊢ u = W \to D = D$
18	15 16 17	f1eq123d	$⊢ u = W \to (u : dom u \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
19	18 3 4	elrabd	$⊢ φ \to W \in \{u \in Word D \| u : dom u \underset{1-1}{⟶} D\}$
20	2	difexd	$⊢ φ \to D ∖ ran W \in V$
21	20	resiexd	$⊢ φ \to {I ↾}_{(D ∖ ran W)} \in V$
22		cshwcl	$⊢ W \in Word D \to W cyclShift 1 \in Word D$
23	3 22	syl	$⊢ φ \to W cyclShift 1 \in Word D$
24		cnvexg	$⊢ W \in Word D \to W^{-1} \in V$
25	3 24	syl	$⊢ φ \to W^{-1} \in V$
26		coexg	$⊢ (W cyclShift 1 \in Word D \land W^{-1} \in V) \to (W cyclShift 1) \circ W^{-1} \in V$
27	23 25 26	syl2anc	$⊢ φ \to (W cyclShift 1) \circ W^{-1} \in V$
28		unexg	$⊢ ({I ↾}_{(D ∖ ran W)} \in V \land (W cyclShift 1) \circ W^{-1} \in V) \to ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1}) \in V$
29	21 27 28	syl2anc	$⊢ φ \to ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1}) \in V$
30	6 14 19 29	fvmptd	$⊢ φ \to C (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$

Metamath Proof Explorer

Theorem tocycfv

Proof