cycpmco2lem3

	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	cycpmco2lem3	$⊢ φ \to \|U\| - 1 = \|W\|$

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		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
17	15 16	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
18	17	nn0cnd	$⊢ φ \to \|W\| \in ℂ$
19		1cnd	$⊢ φ \to 1 \in ℂ$
20		ovexd	$⊢ φ \to W^{-1} (J) + 1 \in V$
21	7 20	eqeltrid	$⊢ φ \to E \in V$
22	5	eldifad	$⊢ φ \to I \in D$
23	22	s1cld	$⊢ φ \to ⟨“ I ”⟩ \in Word D$
24		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\|⟩)$
25	4 21 21 23 24	syl13anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
26	8 25	eqtrid	$⊢ φ \to U = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
27	26	fveq2d	$⊢ φ \to \|U\| = \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\|$
28		pfxcl	$⊢ W \in Word D \to W prefix E \in Word D$
29	15 28	syl	$⊢ φ \to W prefix E \in Word D$
30		ccatcl	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D) \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
31	29 23 30	syl2anc	$⊢ φ \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
32		swrdcl	$⊢ W \in Word D \to W substr ⟨E, \|W\|⟩ \in Word D$
33	15 32	syl	$⊢ φ \to W substr ⟨E, \|W\|⟩ \in Word D$
34		ccatlen	$⊢ ((W prefix E) ++ ⟨“ I ”⟩ \in Word D \land W substr ⟨E, \|W\|⟩ \in Word D) \to \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\| = \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|$
35	31 33 34	syl2anc	$⊢ φ \to \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\| = \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|$
36		ccatws1len	$⊢ W prefix E \in Word D \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
37	29 36	syl	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
38		id	$⊢ w = W \to w = W$
39		dmeq	$⊢ w = W \to dom w = dom W$
40		eqidd	$⊢ w = W \to D = D$
41	38 39 40	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
42	41	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)$
43	14 42	sylib	$⊢ φ \to (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
44		f1cnv	$⊢ W : dom W \underset{1-1}{⟶} D \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
45	43 44	simpl2im	$⊢ φ \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
46		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
47	45 46	syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
48	47 6	ffvelcdmd	$⊢ φ \to W^{-1} (J) \in dom W$
49		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
50	15 49	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
51	48 50	eleqtrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W\|)$
52		fzofzp1	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
53	51 52	syl	$⊢ φ \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
54	7 53	eqeltrid	$⊢ φ \to E \in (0 \dots \|W\|)$
55		pfxlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|)) \to \|W prefix E\| = E$
56	15 54 55	syl2anc	$⊢ φ \to \|W prefix E\| = E$
57	56	oveq1d	$⊢ φ \to \|W prefix E\| + 1 = E + 1$
58	37 57	eqtrd	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = E + 1$
59		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
60	17 59	sylib	$⊢ φ \to \|W\| \in (0 \dots \|W\|)$
61		swrdlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
62	15 54 60 61	syl3anc	$⊢ φ \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
63	58 62	oveq12d	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\| = E + 1 + (\|W\| - E)$
64	27 35 63	3eqtrd	$⊢ φ \to \|U\| = E + 1 + (\|W\| - E)$
65		fz0ssnn0	$⊢ (0 \dots \|W\|) \subseteq ℕ_{0}$
66	65 54	sselid	$⊢ φ \to E \in ℕ_{0}$
67	66	nn0zd	$⊢ φ \to E \in ℤ$
68	67	peano2zd	$⊢ φ \to E + 1 \in ℤ$
69	68	zcnd	$⊢ φ \to E + 1 \in ℂ$
70	66	nn0cnd	$⊢ φ \to E \in ℂ$
71	69 18 70	addsubassd	$⊢ φ \to (E + 1) + \|W\| - E = E + 1 + (\|W\| - E)$
72	70 19 18	addassd	$⊢ φ \to E + 1 + \|W\| = E + 1 + \|W\|$
73	72	oveq1d	$⊢ φ \to (E + 1) + \|W\| - E = E + (1 + \|W\|) - E$
74	64 71 73	3eqtr2d	$⊢ φ \to \|U\| = E + (1 + \|W\|) - E$
75	19 18	addcld	$⊢ φ \to 1 + \|W\| \in ℂ$
76	70 75	pncan2d	$⊢ φ \to E + (1 + \|W\|) - E = 1 + \|W\|$
77	19 18	addcomd	$⊢ φ \to 1 + \|W\| = \|W\| + 1$
78	74 76 77	3eqtrd	$⊢ φ \to \|U\| = \|W\| + 1$
79	18 19 78	mvrraddd	$⊢ φ \to \|U\| - 1 = \|W\|$

Metamath Proof Explorer

Theorem cycpmco2lem3

Proof