cycpmco2f1

Description: The word U used in cycpmco2 is injective, so it can represent a cycle and form a cyclic permutation ( MU ) . (Contributed by Thierry Arnoux, 4-Jan-2024)

	Ref	Expression
Hypotheses	cycpmco2.c	$⊢ M = toCyc (D)$
	cycpmco2.s	$⊢ S = SymGrp (D)$
	cycpmco2.d	$⊢ φ \to D \in V$
	cycpmco2.w	$⊢ φ \to W \in dom M$
	cycpmco2.i	$⊢ φ \to I \in (D ∖ ran W)$
	cycpmco2.j	$⊢ φ \to J \in ran W$
	cycpmco2.e	$⊢ E = W^{-1} (J) + 1$
	cycpmco2.1	$⊢ U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
Assertion	cycpmco2f1	$⊢ φ \to U : dom U \underset{1-1}{⟶} D$

Proof

Step	Hyp	Ref	Expression
1		cycpmco2.c	$⊢ M = toCyc (D)$
2		cycpmco2.s	$⊢ S = SymGrp (D)$
3		cycpmco2.d	$⊢ φ \to D \in V$
4		cycpmco2.w	$⊢ φ \to W \in dom M$
5		cycpmco2.i	$⊢ φ \to I \in (D ∖ ran W)$
6		cycpmco2.j	$⊢ φ \to J \in ran W$
7		cycpmco2.e	$⊢ E = W^{-1} (J) + 1$
8		cycpmco2.1	$⊢ U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
9		ssrab2	$⊢ \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \subseteq Word D$
10		eqid	$⊢ {Base}_{S} = {Base}_{S}$
11	1 2 10	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
12	3 11	syl	$⊢ φ \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
13	12	fdmd	$⊢ φ \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
14	4 13	eleqtrd	$⊢ φ \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
15	9 14	sselid	$⊢ φ \to W \in Word D$
16		pfxcl	$⊢ W \in Word D \to W prefix E \in Word D$
17	15 16	syl	$⊢ φ \to W prefix E \in Word D$
18	5	eldifad	$⊢ φ \to I \in D$
19	18	s1cld	$⊢ φ \to ⟨“ I ”⟩ \in Word D$
20		ccatcl	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D) \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
21	17 19 20	syl2anc	$⊢ φ \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
22		swrdcl	$⊢ W \in Word D \to W substr ⟨E, \|W\|⟩ \in Word D$
23	15 22	syl	$⊢ φ \to W substr ⟨E, \|W\|⟩ \in Word D$
24		id	$⊢ w = W \to w = W$
25		dmeq	$⊢ w = W \to dom w = dom W$
26		eqidd	$⊢ w = W \to D = D$
27	24 25 26	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
28	27	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)$
29	14 28	sylib	$⊢ φ \to (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
30	29	simprd	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
31		f1cnv	$⊢ W : dom W \underset{1-1}{⟶} D \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
32		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
33	30 31 32	3syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
34	33 6	ffvelrnd	$⊢ φ \to W^{-1} (J) \in dom W$
35		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
36	15 35	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
37	34 36	eleqtrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W\|)$
38		fzofzp1	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
39	37 38	syl	$⊢ φ \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
40	7 39	eqeltrid	$⊢ φ \to E \in (0 \dots \|W\|)$
41	15 30 40	pfxf1	$⊢ φ \to (W prefix E) : dom (W prefix E) \underset{1-1}{⟶} D$
42	18	s1f1	$⊢ φ \to ⟨“ I ”⟩ : dom ⟨“ I ”⟩ \underset{1-1}{⟶} D$
43		s1rn	$⊢ I \in D \to ran ⟨“ I ”⟩ = \{I\}$
44	18 43	syl	$⊢ φ \to ran ⟨“ I ”⟩ = \{I\}$
45	44	ineq2d	$⊢ φ \to ran (W prefix E) \cap ran ⟨“ I ”⟩ = ran (W prefix E) \cap \{I\}$
46		pfxrn2	$⊢ (W \in Word D \land E \in (0 \dots \|W\|)) \to ran (W prefix E) \subseteq ran W$
47	15 40 46	syl2anc	$⊢ φ \to ran (W prefix E) \subseteq ran W$
48	47	ssrind	$⊢ φ \to ran (W prefix E) \cap \{I\} \subseteq ran W \cap \{I\}$
49	5	eldifbd	$⊢ φ \to \neg I \in ran W$
50		disjsn	$⊢ ran W \cap \{I\} = \emptyset \leftrightarrow \neg I \in ran W$
51	49 50	sylibr	$⊢ φ \to ran W \cap \{I\} = \emptyset$
52	48 51	sseqtrd	$⊢ φ \to ran (W prefix E) \cap \{I\} \subseteq \emptyset$
53		ss0	$⊢ ran (W prefix E) \cap \{I\} \subseteq \emptyset \to ran (W prefix E) \cap \{I\} = \emptyset$
54	52 53	syl	$⊢ φ \to ran (W prefix E) \cap \{I\} = \emptyset$
55	45 54	eqtrd	$⊢ φ \to ran (W prefix E) \cap ran ⟨“ I ”⟩ = \emptyset$
56	3 17 19 41 42 55	ccatf1	$⊢ φ \to ((W prefix E) ++ ⟨“ I ”⟩) : dom ((W prefix E) ++ ⟨“ I ”⟩) \underset{1-1}{⟶} D$
57		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
58		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
59	58	biimpi	$⊢ \|W\| \in ℕ_{0} \to \|W\| \in (0 \dots \|W\|)$
60	15 57 59	3syl	$⊢ φ \to \|W\| \in (0 \dots \|W\|)$
61	15 40 60 30	swrdf1	$⊢ φ \to (W substr ⟨E, \|W\|⟩) : dom (W substr ⟨E, \|W\|⟩) \underset{1-1}{⟶} D$
62		ccatrn	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D) \to ran ((W prefix E) ++ ⟨“ I ”⟩) = ran (W prefix E) \cup ran ⟨“ I ”⟩$
63	17 19 62	syl2anc	$⊢ φ \to ran ((W prefix E) ++ ⟨“ I ”⟩) = ran (W prefix E) \cup ran ⟨“ I ”⟩$
64	63	ineq1d	$⊢ φ \to ran ((W prefix E) ++ ⟨“ I ”⟩) \cap ran (W substr ⟨E, \|W\|⟩) = (ran (W prefix E) \cup ran ⟨“ I ”⟩) \cap ran (W substr ⟨E, \|W\|⟩)$
65		indir	$⊢ (ran (W prefix E) \cup ran ⟨“ I ”⟩) \cap ran (W substr ⟨E, \|W\|⟩) = (ran (W prefix E) \cap ran (W substr ⟨E, \|W\|⟩)) \cup (ran ⟨“ I ”⟩ \cap ran (W substr ⟨E, \|W\|⟩))$
66	64 65	eqtrdi	$⊢ φ \to ran ((W prefix E) ++ ⟨“ I ”⟩) \cap ran (W substr ⟨E, \|W\|⟩) = (ran (W prefix E) \cap ran (W substr ⟨E, \|W\|⟩)) \cup (ran ⟨“ I ”⟩ \cap ran (W substr ⟨E, \|W\|⟩))$
67		fz0ssnn0	$⊢ (0 \dots \|W\|) \subseteq ℕ_{0}$
68	67 40	sselid	$⊢ φ \to E \in ℕ_{0}$
69		pfxval	$⊢ (W \in Word D \land E \in ℕ_{0}) \to W prefix E = W substr ⟨0, E⟩$
70	15 68 69	syl2anc	$⊢ φ \to W prefix E = W substr ⟨0, E⟩$
71	70	rneqd	$⊢ φ \to ran (W prefix E) = ran (W substr ⟨0, E⟩)$
72	71	ineq1d	$⊢ φ \to ran (W prefix E) \cap ran (W substr ⟨E, \|W\|⟩) = ran (W substr ⟨0, E⟩) \cap ran (W substr ⟨E, \|W\|⟩)$
73		0elfz	$⊢ E \in ℕ_{0} \to 0 \in (0 \dots E)$
74	68 73	syl	$⊢ φ \to 0 \in (0 \dots E)$
75		elfzuz3	$⊢ E \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq E}$
76		eluzfz1	$⊢ \|W\| \in ℤ_{\geq E} \to E \in (E \dots \|W\|)$
77	40 75 76	3syl	$⊢ φ \to E \in (E \dots \|W\|)$
78		eluzfz2	$⊢ \|W\| \in ℤ_{\geq E} \to \|W\| \in (E \dots \|W\|)$
79	40 75 78	3syl	$⊢ φ \to \|W\| \in (E \dots \|W\|)$
80	15 74 40 30 77 79	swrdrndisj	$⊢ φ \to ran (W substr ⟨0, E⟩) \cap ran (W substr ⟨E, \|W\|⟩) = \emptyset$
81	72 80	eqtrd	$⊢ φ \to ran (W prefix E) \cap ran (W substr ⟨E, \|W\|⟩) = \emptyset$
82		incom	$⊢ ran ⟨“ I ”⟩ \cap ran (W substr ⟨E, \|W\|⟩) = ran (W substr ⟨E, \|W\|⟩) \cap ran ⟨“ I ”⟩$
83	44	ineq2d	$⊢ φ \to ran (W substr ⟨E, \|W\|⟩) \cap ran ⟨“ I ”⟩ = ran (W substr ⟨E, \|W\|⟩) \cap \{I\}$
84		swrdrn2	$⊢ (W \in Word D \land E \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to ran (W substr ⟨E, \|W\|⟩) \subseteq ran W$
85	15 40 60 84	syl3anc	$⊢ φ \to ran (W substr ⟨E, \|W\|⟩) \subseteq ran W$
86	85	ssrind	$⊢ φ \to ran (W substr ⟨E, \|W\|⟩) \cap \{I\} \subseteq ran W \cap \{I\}$
87	86 51	sseqtrd	$⊢ φ \to ran (W substr ⟨E, \|W\|⟩) \cap \{I\} \subseteq \emptyset$
88		ss0	$⊢ ran (W substr ⟨E, \|W\|⟩) \cap \{I\} \subseteq \emptyset \to ran (W substr ⟨E, \|W\|⟩) \cap \{I\} = \emptyset$
89	87 88	syl	$⊢ φ \to ran (W substr ⟨E, \|W\|⟩) \cap \{I\} = \emptyset$
90	83 89	eqtrd	$⊢ φ \to ran (W substr ⟨E, \|W\|⟩) \cap ran ⟨“ I ”⟩ = \emptyset$
91	82 90	syl5eq	$⊢ φ \to ran ⟨“ I ”⟩ \cap ran (W substr ⟨E, \|W\|⟩) = \emptyset$
92	81 91	uneq12d	$⊢ φ \to (ran (W prefix E) \cap ran (W substr ⟨E, \|W\|⟩)) \cup (ran ⟨“ I ”⟩ \cap ran (W substr ⟨E, \|W\|⟩)) = \emptyset \cup \emptyset$
93		unidm	$⊢ \emptyset \cup \emptyset = \emptyset$
94	93	a1i	$⊢ φ \to \emptyset \cup \emptyset = \emptyset$
95	66 92 94	3eqtrd	$⊢ φ \to ran ((W prefix E) ++ ⟨“ I ”⟩) \cap ran (W substr ⟨E, \|W\|⟩) = \emptyset$
96	3 21 23 56 61 95	ccatf1	$⊢ φ \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) : dom (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) \underset{1-1}{⟶} D$
97		ovexd	$⊢ φ \to W^{-1} (J) + 1 \in V$
98	7 97	eqeltrid	$⊢ φ \to E \in V$
99		splval	$⊢ (W \in dom M \land (E \in V \land E \in V \land ⟨“ I ”⟩ \in Word D)) \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
100	4 98 98 19 99	syl13anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
101	8 100	syl5eq	$⊢ φ \to U = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
102	101	dmeqd	$⊢ φ \to dom U = dom (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩))$
103		eqidd	$⊢ φ \to D = D$
104	101 102 103	f1eq123d	$⊢ φ \to (U : dom U \underset{1-1}{⟶} D \leftrightarrow (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) : dom (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) \underset{1-1}{⟶} D)$
105	96 104	mpbird	$⊢ φ \to U : dom U \underset{1-1}{⟶} D$

Metamath Proof Explorer

Theorem cycpmco2f1

Proof