cycpmco2lem7

	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 ”⟩⟩$
	cycpmco2lem7.1	$⊢ φ \to K \in ran W$
	cycpmco2lem7.2	$⊢ φ \to K \neq J$
	cycpmco2lem7.3	$⊢ φ \to U^{-1} (K) \in (0 ..^E)$
Assertion	cycpmco2lem7	$⊢ φ \to M (U) (K) = M (W) (K)$

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		cycpmco2lem7.1	$⊢ φ \to K \in ran W$
10		cycpmco2lem7.2	$⊢ φ \to K \neq J$
11		cycpmco2lem7.3	$⊢ φ \to U^{-1} (K) \in (0 ..^E)$
12		ssrab2	$⊢ \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \subseteq Word D$
13		eqid	$⊢ {Base}_{S} = {Base}_{S}$
14	1 2 13	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
15	3 14	syl	$⊢ φ \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
16	15	fdmd	$⊢ φ \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
17	4 16	eleqtrd	$⊢ φ \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
18	12 17	sselid	$⊢ φ \to W \in Word D$
19	5	eldifad	$⊢ φ \to I \in D$
20	19	s1cld	$⊢ φ \to ⟨“ I ”⟩ \in Word D$
21		splcl	$⊢ (W \in Word D \land ⟨“ I ”⟩ \in Word D) \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
22	18 20 21	syl2anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
23	8 22	eqeltrid	$⊢ φ \to U \in Word D$
24	1 2 3 4 5 6 7 8	cycpmco2f1	$⊢ φ \to U : dom U \underset{1-1}{⟶} D$
25		id	$⊢ w = W \to w = W$
26		dmeq	$⊢ w = W \to dom w = dom W$
27		eqidd	$⊢ w = W \to D = D$
28	25 26 27	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
29	28	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)$
30	17 29	sylib	$⊢ φ \to (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
31	30	simprd	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
32		f1cnv	$⊢ W : dom W \underset{1-1}{⟶} D \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
33		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
34	31 32 33	3syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
35	34 6	ffvelrnd	$⊢ φ \to W^{-1} (J) \in dom W$
36		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
37	18 36	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
38	35 37	eleqtrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W\|)$
39		fzofzp1	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
40	38 39	syl	$⊢ φ \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
41	7 40	eqeltrid	$⊢ φ \to E \in (0 \dots \|W\|)$
42		elfzuz3	$⊢ E \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq E}$
43		fzoss2	$⊢ \|W\| \in ℤ_{\geq E} \to (0 ..^E) \subseteq (0 ..^\|W\|)$
44	41 42 43	3syl	$⊢ φ \to (0 ..^E) \subseteq (0 ..^\|W\|)$
45	1 2 3 4 5 6 7 8	cycpmco2lem3	$⊢ φ \to \|U\| - 1 = \|W\|$
46	45	oveq2d	$⊢ φ \to (0 ..^\|U\| - 1) = (0 ..^\|W\|)$
47	44 46	sseqtrrd	$⊢ φ \to (0 ..^E) \subseteq (0 ..^\|U\| - 1)$
48	47 11	sseldd	$⊢ φ \to U^{-1} (K) \in (0 ..^\|U\| - 1)$
49	1 3 23 24 48	cycpmfv1	$⊢ φ \to M (U) (U (U^{-1} (K))) = U (U^{-1} (K) + 1)$
50		f1f1orn	$⊢ U : dom U \underset{1-1}{⟶} D \to U : dom U \underset{1-1 onto}{⟶} ran U$
51	24 50	syl	$⊢ φ \to U : dom U \underset{1-1 onto}{⟶} ran U$
52		ssun1	$⊢ ran W \subseteq ran W \cup \{I\}$
53	1 2 3 4 5 6 7 8	cycpmco2rn	$⊢ φ \to ran U = ran W \cup \{I\}$
54	52 53	sseqtrrid	$⊢ φ \to ran W \subseteq ran U$
55	54	sselda	$⊢ (φ \land K \in ran W) \to K \in ran U$
56		f1ocnvfv2	$⊢ (U : dom U \underset{1-1 onto}{⟶} ran U \land K \in ran U) \to U (U^{-1} (K)) = K$
57	51 55 56	syl2an2r	$⊢ (φ \land K \in ran W) \to U (U^{-1} (K)) = K$
58	57	fveq2d	$⊢ (φ \land K \in ran W) \to M (U) (U (U^{-1} (K))) = M (U) (K)$
59	9 58	mpdan	$⊢ φ \to M (U) (U (U^{-1} (K))) = M (U) (K)$
60		f1f1orn	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W \underset{1-1 onto}{⟶} ran W$
61	31 60	syl	$⊢ φ \to W : dom W \underset{1-1 onto}{⟶} ran W$
62	44 37	sseqtrrd	$⊢ φ \to (0 ..^E) \subseteq dom W$
63	62 11	sseldd	$⊢ φ \to U^{-1} (K) \in dom W$
64		f1ocnvfv1	$⊢ (W : dom W \underset{1-1 onto}{⟶} ran W \land U^{-1} (K) \in dom W) \to W^{-1} (W (U^{-1} (K))) = U^{-1} (K)$
65	61 63 64	syl2anc	$⊢ φ \to W^{-1} (W (U^{-1} (K))) = U^{-1} (K)$
66	8	fveq1i	$⊢ U (U^{-1} (K)) = (W splice ⟨E, E, ⟨“ I ”⟩⟩) (U^{-1} (K))$
67		fz0ssnn0	$⊢ (0 \dots \|W\|) \subseteq ℕ_{0}$
68	67 41	sselid	$⊢ φ \to E \in ℕ_{0}$
69		nn0fz0	$⊢ E \in ℕ_{0} \leftrightarrow E \in (0 \dots E)$
70	68 69	sylib	$⊢ φ \to E \in (0 \dots E)$
71	18 70 41 20 11	splfv1	$⊢ φ \to (W splice ⟨E, E, ⟨“ I ”⟩⟩) (U^{-1} (K)) = W (U^{-1} (K))$
72	66 71	eqtrid	$⊢ φ \to U (U^{-1} (K)) = W (U^{-1} (K))$
73	9 57	mpdan	$⊢ φ \to U (U^{-1} (K)) = K$
74	72 73	eqtr3d	$⊢ φ \to W (U^{-1} (K)) = K$
75	74	fveq2d	$⊢ φ \to W^{-1} (W (U^{-1} (K))) = W^{-1} (K)$
76	65 75	eqtr3d	$⊢ φ \to U^{-1} (K) = W^{-1} (K)$
77	76	oveq1d	$⊢ φ \to U^{-1} (K) + 1 = W^{-1} (K) + 1$
78	77	fveq2d	$⊢ φ \to U (U^{-1} (K) + 1) = U (W^{-1} (K) + 1)$
79	49 59 78	3eqtr3d	$⊢ φ \to M (U) (K) = U (W^{-1} (K) + 1)$
80	8	a1i	$⊢ φ \to U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
81	80	fveq1d	$⊢ φ \to U (W^{-1} (K) + 1) = (W splice ⟨E, E, ⟨“ I ”⟩⟩) (W^{-1} (K) + 1)$
82	41	elfzelzd	$⊢ φ \to E \in ℤ$
83		simpr	$⊢ (φ \land U^{-1} (K) \in (0 ..^E - 1)) \to U^{-1} (K) \in (0 ..^E - 1)$
84	7	a1i	$⊢ φ \to E = W^{-1} (J) + 1$
85	84	oveq1d	$⊢ φ \to E - 1 = W^{-1} (J) + 1 - 1$
86		elfzonn0	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) \in ℕ_{0}$
87	38 86	syl	$⊢ φ \to W^{-1} (J) \in ℕ_{0}$
88	87	nn0cnd	$⊢ φ \to W^{-1} (J) \in ℂ$
89		1cnd	$⊢ φ \to 1 \in ℂ$
90	88 89	pncand	$⊢ φ \to W^{-1} (J) + 1 - 1 = W^{-1} (J)$
91	85 90	eqtr2d	$⊢ φ \to W^{-1} (J) = E - 1$
92	91	adantr	$⊢ (φ \land U^{-1} (K) = E - 1) \to W^{-1} (J) = E - 1$
93		simpr	$⊢ (φ \land U^{-1} (K) = E - 1) \to U^{-1} (K) = E - 1$
94	76	adantr	$⊢ (φ \land U^{-1} (K) = E - 1) \to U^{-1} (K) = W^{-1} (K)$
95	92 93 94	3eqtr2rd	$⊢ (φ \land U^{-1} (K) = E - 1) \to W^{-1} (K) = W^{-1} (J)$
96	95	fveq2d	$⊢ (φ \land U^{-1} (K) = E - 1) \to W (W^{-1} (K)) = W (W^{-1} (J))$
97		f1ocnvfv2	$⊢ (W : dom W \underset{1-1 onto}{⟶} ran W \land K \in ran W) \to W (W^{-1} (K)) = K$
98	61 9 97	syl2anc	$⊢ φ \to W (W^{-1} (K)) = K$
99	98	adantr	$⊢ (φ \land U^{-1} (K) = E - 1) \to W (W^{-1} (K)) = K$
100		f1ocnvfv2	$⊢ (W : dom W \underset{1-1 onto}{⟶} ran W \land J \in ran W) \to W (W^{-1} (J)) = J$
101	61 6 100	syl2anc	$⊢ φ \to W (W^{-1} (J)) = J$
102	101	adantr	$⊢ (φ \land U^{-1} (K) = E - 1) \to W (W^{-1} (J)) = J$
103	96 99 102	3eqtr3d	$⊢ (φ \land U^{-1} (K) = E - 1) \to K = J$
104	10	adantr	$⊢ (φ \land U^{-1} (K) = E - 1) \to K \neq J$
105	103 104	pm2.21ddne	$⊢ (φ \land U^{-1} (K) = E - 1) \to U^{-1} (K) \in (0 ..^E - 1)$
106		0zd	$⊢ φ \to 0 \in ℤ$
107		nn0p1nn	$⊢ W^{-1} (J) \in ℕ_{0} \to W^{-1} (J) + 1 \in ℕ$
108	87 107	syl	$⊢ φ \to W^{-1} (J) + 1 \in ℕ$
109	7 108	eqeltrid	$⊢ φ \to E \in ℕ$
110		0p1e1	$⊢ 0 + 1 = 1$
111	110	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
112		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
113	111 112	eqtr4i	$⊢ ℤ_{\geq (0 + 1)} = ℕ$
114	109 113	eleqtrrdi	$⊢ φ \to E \in ℤ_{\geq (0 + 1)}$
115		fzosplitsnm1	$⊢ (0 \in ℤ \land E \in ℤ_{\geq (0 + 1)}) \to (0 ..^E) = (0 ..^E - 1) \cup \{E - 1\}$
116	106 114 115	syl2anc	$⊢ φ \to (0 ..^E) = (0 ..^E - 1) \cup \{E - 1\}$
117	11 116	eleqtrd	$⊢ φ \to U^{-1} (K) \in ((0 ..^E - 1) \cup \{E - 1\})$
118		fvex	$⊢ U^{-1} (K) \in V$
119		elunsn	$⊢ U^{-1} (K) \in V \to (U^{-1} (K) \in ((0 ..^E - 1) \cup \{E - 1\}) \leftrightarrow (U^{-1} (K) \in (0 ..^E - 1) \lor U^{-1} (K) = E - 1))$
120	118 119	ax-mp	$⊢ U^{-1} (K) \in ((0 ..^E - 1) \cup \{E - 1\}) \leftrightarrow (U^{-1} (K) \in (0 ..^E - 1) \lor U^{-1} (K) = E - 1)$
121	117 120	sylib	$⊢ φ \to (U^{-1} (K) \in (0 ..^E - 1) \lor U^{-1} (K) = E - 1)$
122	83 105 121	mpjaodan	$⊢ φ \to U^{-1} (K) \in (0 ..^E - 1)$
123		elfzom1elp1fzo	$⊢ (E \in ℤ \land U^{-1} (K) \in (0 ..^E - 1)) \to U^{-1} (K) + 1 \in (0 ..^E)$
124	82 122 123	syl2anc	$⊢ φ \to U^{-1} (K) + 1 \in (0 ..^E)$
125	77 124	eqeltrrd	$⊢ φ \to W^{-1} (K) + 1 \in (0 ..^E)$
126	18 70 41 20 125	splfv1	$⊢ φ \to (W splice ⟨E, E, ⟨“ I ”⟩⟩) (W^{-1} (K) + 1) = W (W^{-1} (K) + 1)$
127	81 126	eqtrd	$⊢ φ \to U (W^{-1} (K) + 1) = W (W^{-1} (K) + 1)$
128		1zzd	$⊢ φ \to 1 \in ℤ$
129	82 128	zsubcld	$⊢ φ \to E - 1 \in ℤ$
130		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
131		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
132	131	biimpi	$⊢ \|W\| \in ℕ_{0} \to \|W\| \in (0 \dots \|W\|)$
133	18 130 132	3syl	$⊢ φ \to \|W\| \in (0 \dots \|W\|)$
134	133	elfzelzd	$⊢ φ \to \|W\| \in ℤ$
135	134 128	zsubcld	$⊢ φ \to \|W\| - 1 \in ℤ$
136	109	nnred	$⊢ φ \to E \in ℝ$
137	134	zred	$⊢ φ \to \|W\| \in ℝ$
138		1red	$⊢ φ \to 1 \in ℝ$
139		elfzle2	$⊢ E \in (0 \dots \|W\|) \to E \leq \|W\|$
140	41 139	syl	$⊢ φ \to E \leq \|W\|$
141	136 137 138 140	lesub1dd	$⊢ φ \to E - 1 \leq \|W\| - 1$
142		eluz	$⊢ (E - 1 \in ℤ \land \|W\| - 1 \in ℤ) \to (\|W\| - 1 \in ℤ_{\geq (E - 1)} \leftrightarrow E - 1 \leq \|W\| - 1)$
143	142	biimpar	$⊢ ((E - 1 \in ℤ \land \|W\| - 1 \in ℤ) \land E - 1 \leq \|W\| - 1) \to \|W\| - 1 \in ℤ_{\geq (E - 1)}$
144	129 135 141 143	syl21anc	$⊢ φ \to \|W\| - 1 \in ℤ_{\geq (E - 1)}$
145		fzoss2	$⊢ \|W\| - 1 \in ℤ_{\geq (E - 1)} \to (0 ..^E - 1) \subseteq (0 ..^\|W\| - 1)$
146	144 145	syl	$⊢ φ \to (0 ..^E - 1) \subseteq (0 ..^\|W\| - 1)$
147	146 122	sseldd	$⊢ φ \to U^{-1} (K) \in (0 ..^\|W\| - 1)$
148	76 147	eqeltrrd	$⊢ φ \to W^{-1} (K) \in (0 ..^\|W\| - 1)$
149	1 3 18 31 148	cycpmfv1	$⊢ φ \to M (W) (W (W^{-1} (K))) = W (W^{-1} (K) + 1)$
150	98	fveq2d	$⊢ φ \to M (W) (W (W^{-1} (K))) = M (W) (K)$
151	127 149 150	3eqtr2rd	$⊢ φ \to M (W) (K) = U (W^{-1} (K) + 1)$
152	79 151	eqtr4d	$⊢ φ \to M (U) (K) = M (W) (K)$

Metamath Proof Explorer

Theorem cycpmco2lem7

Proof