cycpmco2lem2

	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	cycpmco2lem2	$⊢ φ \to U (E) = I$

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		ovexd	$⊢ φ \to W^{-1} (J) + 1 \in V$
10	7 9	eqeltrid	$⊢ φ \to E \in V$
11	5	eldifad	$⊢ φ \to I \in D$
12	11	s1cld	$⊢ φ \to ⟨“ I ”⟩ \in Word D$
13		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\|⟩)$
14	4 10 10 12 13	syl13anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
15	8 14	eqtrid	$⊢ φ \to U = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
16	15	fveq1d	$⊢ φ \to U (E) = (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (E)$
17		ssrab2	$⊢ \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \subseteq Word D$
18		eqid	$⊢ {Base}_{S} = {Base}_{S}$
19	1 2 18	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
20	3 19	syl	$⊢ φ \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
21	20	fdmd	$⊢ φ \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
22	4 21	eleqtrd	$⊢ φ \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
23	17 22	sselid	$⊢ φ \to W \in Word D$
24		pfxcl	$⊢ W \in Word D \to W prefix E \in Word D$
25	23 24	syl	$⊢ φ \to W prefix E \in Word D$
26		ccatcl	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D) \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
27	25 12 26	syl2anc	$⊢ φ \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
28		swrdcl	$⊢ W \in Word D \to W substr ⟨E, \|W\|⟩ \in Word D$
29	23 28	syl	$⊢ φ \to W substr ⟨E, \|W\|⟩ \in Word D$
30		fz0ssnn0	$⊢ (0 \dots \|W\|) \subseteq ℕ_{0}$
31		id	$⊢ w = W \to w = W$
32		dmeq	$⊢ w = W \to dom w = dom W$
33		eqidd	$⊢ w = W \to D = D$
34	31 32 33	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
35	34	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)$
36	22 35	sylib	$⊢ φ \to (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
37	36	simprd	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
38		f1cnv	$⊢ W : dom W \underset{1-1}{⟶} D \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
39		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
40	37 38 39	3syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
41	40 6	ffvelcdmd	$⊢ φ \to W^{-1} (J) \in dom W$
42		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
43	23 42	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
44	41 43	eleqtrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W\|)$
45		fzofzp1	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
46	44 45	syl	$⊢ φ \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
47	7 46	eqeltrid	$⊢ φ \to E \in (0 \dots \|W\|)$
48	30 47	sselid	$⊢ φ \to E \in ℕ_{0}$
49		fzonn0p1	$⊢ E \in ℕ_{0} \to E \in (0 ..^E + 1)$
50	48 49	syl	$⊢ φ \to E \in (0 ..^E + 1)$
51		ccatws1len	$⊢ W prefix E \in Word D \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
52	23 24 51	3syl	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
53		pfxlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|)) \to \|W prefix E\| = E$
54	23 47 53	syl2anc	$⊢ φ \to \|W prefix E\| = E$
55	54	oveq1d	$⊢ φ \to \|W prefix E\| + 1 = E + 1$
56	52 55	eqtrd	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = E + 1$
57	56	oveq2d	$⊢ φ \to (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|) = (0 ..^E + 1)$
58	50 57	eleqtrrd	$⊢ φ \to E \in (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|)$
59		ccatval1	$⊢ ((W prefix E) ++ ⟨“ I ”⟩ \in Word D \land W substr ⟨E, \|W\|⟩ \in Word D \land E \in (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|)) \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (E) = ((W prefix E) ++ ⟨“ I ”⟩) (E)$
60	27 29 58 59	syl3anc	$⊢ φ \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (E) = ((W prefix E) ++ ⟨“ I ”⟩) (E)$
61	48	nn0zd	$⊢ φ \to E \in ℤ$
62		elfzomin	$⊢ E \in ℤ \to E \in (E ..^E + 1)$
63	61 62	syl	$⊢ φ \to E \in (E ..^E + 1)$
64		s1len	$⊢ \|⟨“ I ”⟩\| = 1$
65	64	a1i	$⊢ φ \to \|⟨“ I ”⟩\| = 1$
66	54 65	oveq12d	$⊢ φ \to \|W prefix E\| + \|⟨“ I ”⟩\| = E + 1$
67	54 66	oveq12d	$⊢ φ \to (\|W prefix E\| ..^\|W prefix E\| + \|⟨“ I ”⟩\|) = (E ..^E + 1)$
68	63 67	eleqtrrd	$⊢ φ \to E \in (\|W prefix E\| ..^\|W prefix E\| + \|⟨“ I ”⟩\|)$
69		ccatval2	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D \land E \in (\|W prefix E\| ..^\|W prefix E\| + \|⟨“ I ”⟩\|)) \to ((W prefix E) ++ ⟨“ I ”⟩) (E) = ⟨“ I ”⟩ (E - \|W prefix E\|)$
70	25 12 68 69	syl3anc	$⊢ φ \to ((W prefix E) ++ ⟨“ I ”⟩) (E) = ⟨“ I ”⟩ (E - \|W prefix E\|)$
71	16 60 70	3eqtrd	$⊢ φ \to U (E) = ⟨“ I ”⟩ (E - \|W prefix E\|)$
72	54	oveq2d	$⊢ φ \to E - \|W prefix E\| = E - E$
73	48	nn0cnd	$⊢ φ \to E \in ℂ$
74	73	subidd	$⊢ φ \to E - E = 0$
75	72 74	eqtrd	$⊢ φ \to E - \|W prefix E\| = 0$
76	75	fveq2d	$⊢ φ \to ⟨“ I ”⟩ (E - \|W prefix E\|) = ⟨“ I ”⟩ (0)$
77		s1fv	$⊢ I \in (D ∖ ran W) \to ⟨“ I ”⟩ (0) = I$
78	5 77	syl	$⊢ φ \to ⟨“ I ”⟩ (0) = I$
79	71 76 78	3eqtrd	$⊢ φ \to U (E) = I$

Metamath Proof Explorer

Theorem cycpmco2lem2

Proof