tocyc01

Description: Permutation cycles built from the empty set or a singleton are the identity. (Contributed by Thierry Arnoux, 21-Nov-2023)

		Ref	Expression
	Hypothesis	tocyc01.1	$⊢ C = toCyc (D)$
	Assertion	tocyc01	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to C (W) = {I ↾}_{D}$

Proof

Step	Hyp	Ref	Expression
1		tocyc01.1	$⊢ C = toCyc (D)$
2		simpl	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to D \in V$
3		simpr	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])$
4	3	elin1d	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to W \in dom C$
5		eqid	$⊢ SymGrp (D) = SymGrp (D)$
6		eqid	$⊢ {Base}_{SymGrp (D)} = {Base}_{SymGrp (D)}$
7	1 5 6	tocycf	$⊢ D \in V \to C : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{SymGrp (D)}$
8		fdm	$⊢ C : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{SymGrp (D)} \to dom C = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
9	2 7 8	3syl	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to dom C = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
10	4 9	eleqtrd	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
11		id	$⊢ w = W \to w = W$
12		dmeq	$⊢ w = W \to dom w = dom W$
13		eqidd	$⊢ w = W \to D = D$
14	11 12 13	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
15	14	elrab	$⊢ W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \leftrightarrow (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
16	10 15	sylib	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
17	16	simpld	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to W \in Word D$
18	16	simprd	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to W : dom W \underset{1-1}{⟶} D$
19	1 2 17 18	tocycfv	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to C (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
20	19	adantr	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 0) \to C (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
21		hasheq0	$⊢ W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}]) \to (\|W\| = 0 \leftrightarrow W = \emptyset)$
22	3 21	syl	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to (\|W\| = 0 \leftrightarrow W = \emptyset)$
23	22	biimpa	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 0) \to W = \emptyset$
24		rneq	$⊢ W = \emptyset \to ran W = ran \emptyset$
25		rn0	$⊢ ran \emptyset = \emptyset$
26	24 25	eqtrdi	$⊢ W = \emptyset \to ran W = \emptyset$
27	26	difeq2d	$⊢ W = \emptyset \to D ∖ ran W = D ∖ \emptyset$
28		dif0	$⊢ D ∖ \emptyset = D$
29	27 28	eqtrdi	$⊢ W = \emptyset \to D ∖ ran W = D$
30	29	reseq2d	$⊢ W = \emptyset \to {I ↾}_{(D ∖ ran W)} = {I ↾}_{D}$
31		cnveq	$⊢ W = \emptyset \to W^{-1} = \emptyset^{-1}$
32		cnv0	$⊢ \emptyset^{-1} = \emptyset$
33	31 32	eqtrdi	$⊢ W = \emptyset \to W^{-1} = \emptyset$
34	33	coeq2d	$⊢ W = \emptyset \to (W cyclShift 1) \circ W^{-1} = (W cyclShift 1) \circ \emptyset$
35		co02	$⊢ (W cyclShift 1) \circ \emptyset = \emptyset$
36	34 35	eqtrdi	$⊢ W = \emptyset \to (W cyclShift 1) \circ W^{-1} = \emptyset$
37	30 36	uneq12d	$⊢ W = \emptyset \to ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1}) = ({I ↾}_{D}) \cup \emptyset$
38		un0	$⊢ ({I ↾}_{D}) \cup \emptyset = {I ↾}_{D}$
39	37 38	eqtrdi	$⊢ W = \emptyset \to ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1}) = {I ↾}_{D}$
40	23 39	syl	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 0) \to ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1}) = {I ↾}_{D}$
41	20 40	eqtrd	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 0) \to C (W) = {I ↾}_{D}$
42	19	adantr	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to C (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
43	17	adantr	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to W \in Word D$
44		1zzd	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to 1 \in ℤ$
45		simpr	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to \|W\| = 1$
46		1cshid	$⊢ (W \in Word D \land 1 \in ℤ \land \|W\| = 1) \to W cyclShift 1 = W$
47	43 44 45 46	syl3anc	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to W cyclShift 1 = W$
48	47	coeq1d	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to (W cyclShift 1) \circ W^{-1} = W \circ W^{-1}$
49		wrdf	$⊢ W \in Word D \to W : (0 ..^\|W\|) ⟶ D$
50		ffun	$⊢ W : (0 ..^\|W\|) ⟶ D \to Fun W$
51		funcocnv2	$⊢ Fun W \to W \circ W^{-1} = {I ↾}_{ran W}$
52	43 49 50 51	4syl	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to W \circ W^{-1} = {I ↾}_{ran W}$
53	48 52	eqtrd	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to (W cyclShift 1) \circ W^{-1} = {I ↾}_{ran W}$
54	53	uneq2d	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1}) = ({I ↾}_{(D ∖ ran W)}) \cup ({I ↾}_{ran W})$
55		resundi	$⊢ {I ↾}_{((D ∖ ran W) \cup ran W)} = ({I ↾}_{(D ∖ ran W)}) \cup ({I ↾}_{ran W})$
56		frn	$⊢ W : (0 ..^\|W\|) ⟶ D \to ran W \subseteq D$
57		undifr	$⊢ ran W \subseteq D \leftrightarrow (D ∖ ran W) \cup ran W = D$
58	56 57	sylib	$⊢ W : (0 ..^\|W\|) ⟶ D \to (D ∖ ran W) \cup ran W = D$
59	43 49 58	3syl	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to (D ∖ ran W) \cup ran W = D$
60	59	reseq2d	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to {I ↾}_{((D ∖ ran W) \cup ran W)} = {I ↾}_{D}$
61	55 60	syl5eqr	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to ({I ↾}_{(D ∖ ran W)}) \cup ({I ↾}_{ran W}) = {I ↾}_{D}$
62	42 54 61	3eqtrd	$⊢ ((D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \land \|W\| = 1) \to C (W) = {I ↾}_{D}$
63	3	elin2d	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to W \in {\|.\|}^{-1} [\{0, 1\}]$
64		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
65		ffn	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to \|.\| Fn V$
66		elpreima	$⊢ \|.\| Fn V \to (W \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow (W \in V \land \|W\| \in \{0, 1\}))$
67	64 65 66	mp2b	$⊢ W \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow (W \in V \land \|W\| \in \{0, 1\})$
68	63 67	sylib	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to (W \in V \land \|W\| \in \{0, 1\})$
69	68	simprd	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to \|W\| \in \{0, 1\}$
70		elpri	$⊢ \|W\| \in \{0, 1\} \to (\|W\| = 0 \lor \|W\| = 1)$
71	69 70	syl	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to (\|W\| = 0 \lor \|W\| = 1)$
72	41 62 71	mpjaodan	$⊢ (D \in V \land W \in (dom C \cap {\|.\|}^{-1} [\{0, 1\}])) \to C (W) = {I ↾}_{D}$

Metamath Proof Explorer

Theorem tocyc01

Proof