efgredlemd

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

	Ref	Expression
Hypotheses	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
	efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
	efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
	efgredlem.1	$⊢ φ \to \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))$
	efgredlem.2	$⊢ φ \to A \in dom S$
	efgredlem.3	$⊢ φ \to B \in dom S$
	efgredlem.4	$⊢ φ \to S (A) = S (B)$
	efgredlem.5	$⊢ φ \to \neg A (0) = B (0)$
	efgredlemb.k	$⊢ K = \|A\| - 1 - 1$
	efgredlemb.l	$⊢ L = \|B\| - 1 - 1$
	efgredlemb.p	$⊢ φ \to P \in (0 \dots \|A (K)\|)$
	efgredlemb.q	$⊢ φ \to Q \in (0 \dots \|B (L)\|)$
	efgredlemb.u	$⊢ φ \to U \in (I \times 2_{𝑜})$
	efgredlemb.v	$⊢ φ \to V \in (I \times 2_{𝑜})$
	efgredlemb.6	$⊢ φ \to S (A) = P T (A (K)) U$
	efgredlemb.7	$⊢ φ \to S (B) = Q T (B (L)) V$
	efgredlemb.8	$⊢ φ \to \neg A (K) = B (L)$
	efgredlemd.9	$⊢ φ \to P \in ℤ_{\geq (Q + 2)}$
	efgredlemd.c	$⊢ φ \to C \in dom S$
	efgredlemd.sc	$⊢ φ \to S (C) = (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
Assertion	efgredlemd	$⊢ φ \to A (0) = B (0)$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
4		efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
5		efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
6		efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
7		efgredlem.1	$⊢ φ \to \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))$
8		efgredlem.2	$⊢ φ \to A \in dom S$
9		efgredlem.3	$⊢ φ \to B \in dom S$
10		efgredlem.4	$⊢ φ \to S (A) = S (B)$
11		efgredlem.5	$⊢ φ \to \neg A (0) = B (0)$
12		efgredlemb.k	$⊢ K = \|A\| - 1 - 1$
13		efgredlemb.l	$⊢ L = \|B\| - 1 - 1$
14		efgredlemb.p	$⊢ φ \to P \in (0 \dots \|A (K)\|)$
15		efgredlemb.q	$⊢ φ \to Q \in (0 \dots \|B (L)\|)$
16		efgredlemb.u	$⊢ φ \to U \in (I \times 2_{𝑜})$
17		efgredlemb.v	$⊢ φ \to V \in (I \times 2_{𝑜})$
18		efgredlemb.6	$⊢ φ \to S (A) = P T (A (K)) U$
19		efgredlemb.7	$⊢ φ \to S (B) = Q T (B (L)) V$
20		efgredlemb.8	$⊢ φ \to \neg A (K) = B (L)$
21		efgredlemd.9	$⊢ φ \to P \in ℤ_{\geq (Q + 2)}$
22		efgredlemd.c	$⊢ φ \to C \in dom S$
23		efgredlemd.sc	$⊢ φ \to S (C) = (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
24	1 2 3 4 5 6	efgsdm	$⊢ C \in dom S \leftrightarrow (C \in (Word W ∖ \{\emptyset\}) \land C (0) \in D \land \forall i \in (1 ..^\|C\|) C (i) \in ran T (C (i - 1)))$
25	24	simp1bi	$⊢ C \in dom S \to C \in (Word W ∖ \{\emptyset\})$
26	22 25	syl	$⊢ φ \to C \in (Word W ∖ \{\emptyset\})$
27	26	eldifad	$⊢ φ \to C \in Word W$
28	1 2 3 4 5 6	efgsdm	$⊢ A \in dom S \leftrightarrow (A \in (Word W ∖ \{\emptyset\}) \land A (0) \in D \land \forall i \in (1 ..^\|A\|) A (i) \in ran T (A (i - 1)))$
29	28	simp1bi	$⊢ A \in dom S \to A \in (Word W ∖ \{\emptyset\})$
30	8 29	syl	$⊢ φ \to A \in (Word W ∖ \{\emptyset\})$
31	30	eldifad	$⊢ φ \to A \in Word W$
32		wrdf	$⊢ A \in Word W \to A : (0 ..^\|A\|) ⟶ W$
33	31 32	syl	$⊢ φ \to A : (0 ..^\|A\|) ⟶ W$
34		fzossfz	$⊢ (0 ..^\|A\| - 1) \subseteq (0 \dots \|A\| - 1)$
35		lencl	$⊢ A \in Word W \to \|A\| \in ℕ_{0}$
36	31 35	syl	$⊢ φ \to \|A\| \in ℕ_{0}$
37	36	nn0zd	$⊢ φ \to \|A\| \in ℤ$
38		fzoval	$⊢ \|A\| \in ℤ \to (0 ..^\|A\|) = (0 \dots \|A\| - 1)$
39	37 38	syl	$⊢ φ \to (0 ..^\|A\|) = (0 \dots \|A\| - 1)$
40	34 39	sseqtrrid	$⊢ φ \to (0 ..^\|A\| - 1) \subseteq (0 ..^\|A\|)$
41	1 2 3 4 5 6 7 8 9 10 11	efgredlema	$⊢ φ \to (\|A\| - 1 \in ℕ \land \|B\| - 1 \in ℕ)$
42	41	simpld	$⊢ φ \to \|A\| - 1 \in ℕ$
43		fzo0end	$⊢ \|A\| - 1 \in ℕ \to \|A\| - 1 - 1 \in (0 ..^\|A\| - 1)$
44	42 43	syl	$⊢ φ \to \|A\| - 1 - 1 \in (0 ..^\|A\| - 1)$
45	12 44	eqeltrid	$⊢ φ \to K \in (0 ..^\|A\| - 1)$
46	40 45	sseldd	$⊢ φ \to K \in (0 ..^\|A\|)$
47	33 46	ffvelrnd	$⊢ φ \to A (K) \in W$
48	47	s1cld	$⊢ φ \to ⟨“ A (K) ”⟩ \in Word W$
49		eldifsn	$⊢ C \in (Word W ∖ \{\emptyset\}) \leftrightarrow (C \in Word W \land C \neq \emptyset)$
50		lennncl	$⊢ (C \in Word W \land C \neq \emptyset) \to \|C\| \in ℕ$
51	49 50	sylbi	$⊢ C \in (Word W ∖ \{\emptyset\}) \to \|C\| \in ℕ$
52	26 51	syl	$⊢ φ \to \|C\| \in ℕ$
53		lbfzo0	$⊢ 0 \in (0 ..^\|C\|) \leftrightarrow \|C\| \in ℕ$
54	52 53	sylibr	$⊢ φ \to 0 \in (0 ..^\|C\|)$
55		ccatval1	$⊢ (C \in Word W \land ⟨“ A (K) ”⟩ \in Word W \land 0 \in (0 ..^\|C\|)) \to (C ++ ⟨“ A (K) ”⟩) (0) = C (0)$
56	27 48 54 55	syl3anc	$⊢ φ \to (C ++ ⟨“ A (K) ”⟩) (0) = C (0)$
57	1 2 3 4 5 6	efgsdm	$⊢ B \in dom S \leftrightarrow (B \in (Word W ∖ \{\emptyset\}) \land B (0) \in D \land \forall i \in (1 ..^\|B\|) B (i) \in ran T (B (i - 1)))$
58	57	simp1bi	$⊢ B \in dom S \to B \in (Word W ∖ \{\emptyset\})$
59	9 58	syl	$⊢ φ \to B \in (Word W ∖ \{\emptyset\})$
60	59	eldifad	$⊢ φ \to B \in Word W$
61		wrdf	$⊢ B \in Word W \to B : (0 ..^\|B\|) ⟶ W$
62	60 61	syl	$⊢ φ \to B : (0 ..^\|B\|) ⟶ W$
63		fzossfz	$⊢ (0 ..^\|B\| - 1) \subseteq (0 \dots \|B\| - 1)$
64		lencl	$⊢ B \in Word W \to \|B\| \in ℕ_{0}$
65	60 64	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
66	65	nn0zd	$⊢ φ \to \|B\| \in ℤ$
67		fzoval	$⊢ \|B\| \in ℤ \to (0 ..^\|B\|) = (0 \dots \|B\| - 1)$
68	66 67	syl	$⊢ φ \to (0 ..^\|B\|) = (0 \dots \|B\| - 1)$
69	63 68	sseqtrrid	$⊢ φ \to (0 ..^\|B\| - 1) \subseteq (0 ..^\|B\|)$
70	41	simprd	$⊢ φ \to \|B\| - 1 \in ℕ$
71		fzo0end	$⊢ \|B\| - 1 \in ℕ \to \|B\| - 1 - 1 \in (0 ..^\|B\| - 1)$
72	70 71	syl	$⊢ φ \to \|B\| - 1 - 1 \in (0 ..^\|B\| - 1)$
73	13 72	eqeltrid	$⊢ φ \to L \in (0 ..^\|B\| - 1)$
74	69 73	sseldd	$⊢ φ \to L \in (0 ..^\|B\|)$
75	62 74	ffvelrnd	$⊢ φ \to B (L) \in W$
76	75	s1cld	$⊢ φ \to ⟨“ B (L) ”⟩ \in Word W$
77		ccatval1	$⊢ (C \in Word W \land ⟨“ B (L) ”⟩ \in Word W \land 0 \in (0 ..^\|C\|)) \to (C ++ ⟨“ B (L) ”⟩) (0) = C (0)$
78	27 76 54 77	syl3anc	$⊢ φ \to (C ++ ⟨“ B (L) ”⟩) (0) = C (0)$
79	56 78	eqtr4d	$⊢ φ \to (C ++ ⟨“ A (K) ”⟩) (0) = (C ++ ⟨“ B (L) ”⟩) (0)$
80		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
81	1 80	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
82	81 47	sselid	$⊢ φ \to A (K) \in Word (I \times 2_{𝑜})$
83		lencl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to \|A (K)\| \in ℕ_{0}$
84	82 83	syl	$⊢ φ \to \|A (K)\| \in ℕ_{0}$
85	84	nn0red	$⊢ φ \to \|A (K)\| \in ℝ$
86		2rp	$⊢ 2 \in ℝ^{+}$
87		ltaddrp	$⊢ (\|A (K)\| \in ℝ \land 2 \in ℝ^{+}) \to \|A (K)\| < \|A (K)\| + 2$
88	85 86 87	sylancl	$⊢ φ \to \|A (K)\| < \|A (K)\| + 2$
89	36	nn0red	$⊢ φ \to \|A\| \in ℝ$
90	89	lem1d	$⊢ φ \to \|A\| - 1 \leq \|A\|$
91		fznn	$⊢ \|A\| \in ℤ \to (\|A\| - 1 \in (1 \dots \|A\|) \leftrightarrow (\|A\| - 1 \in ℕ \land \|A\| - 1 \leq \|A\|))$
92	37 91	syl	$⊢ φ \to (\|A\| - 1 \in (1 \dots \|A\|) \leftrightarrow (\|A\| - 1 \in ℕ \land \|A\| - 1 \leq \|A\|))$
93	42 90 92	mpbir2and	$⊢ φ \to \|A\| - 1 \in (1 \dots \|A\|)$
94	1 2 3 4 5 6	efgsres	$⊢ (A \in dom S \land \|A\| - 1 \in (1 \dots \|A\|)) \to {A ↾}_{(0 ..^\|A\| - 1)} \in dom S$
95	8 93 94	syl2anc	$⊢ φ \to {A ↾}_{(0 ..^\|A\| - 1)} \in dom S$
96	1 2 3 4 5 6	efgsval	$⊢ {A ↾}_{(0 ..^\|A\| - 1)} \in dom S \to S ({A ↾}_{(0 ..^\|A\| - 1)}) = ({A ↾}_{(0 ..^\|A\| - 1)}) (\|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1)$
97	95 96	syl	$⊢ φ \to S ({A ↾}_{(0 ..^\|A\| - 1)}) = ({A ↾}_{(0 ..^\|A\| - 1)}) (\|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1)$
98		fz1ssfz0	$⊢ (1 \dots \|A\|) \subseteq (0 \dots \|A\|)$
99	98 93	sselid	$⊢ φ \to \|A\| - 1 \in (0 \dots \|A\|)$
100		pfxres	$⊢ (A \in Word W \land \|A\| - 1 \in (0 \dots \|A\|)) \to A prefix (\|A\| - 1) = {A ↾}_{(0 ..^\|A\| - 1)}$
101	31 99 100	syl2anc	$⊢ φ \to A prefix (\|A\| - 1) = {A ↾}_{(0 ..^\|A\| - 1)}$
102	101	fveq2d	$⊢ φ \to \|A prefix (\|A\| - 1)\| = \|{A ↾}_{(0 ..^\|A\| - 1)}\|$
103		pfxlen	$⊢ (A \in Word W \land \|A\| - 1 \in (0 \dots \|A\|)) \to \|A prefix (\|A\| - 1)\| = \|A\| - 1$
104	31 99 103	syl2anc	$⊢ φ \to \|A prefix (\|A\| - 1)\| = \|A\| - 1$
105	102 104	eqtr3d	$⊢ φ \to \|{A ↾}_{(0 ..^\|A\| - 1)}\| = \|A\| - 1$
106	105	oveq1d	$⊢ φ \to \|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1 = \|A\| - 1 - 1$
107	106 12	eqtr4di	$⊢ φ \to \|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1 = K$
108	107	fveq2d	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (\|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1) = ({A ↾}_{(0 ..^\|A\| - 1)}) (K)$
109	45	fvresd	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (K) = A (K)$
110	97 108 109	3eqtrd	$⊢ φ \to S ({A ↾}_{(0 ..^\|A\| - 1)}) = A (K)$
111	110	fveq2d	$⊢ φ \to \|S ({A ↾}_{(0 ..^\|A\| - 1)})\| = \|A (K)\|$
112	1 2 3 4 5 6	efgsdmi	$⊢ (A \in dom S \land \|A\| - 1 \in ℕ) \to S (A) \in ran T (A (\|A\| - 1 - 1))$
113	8 42 112	syl2anc	$⊢ φ \to S (A) \in ran T (A (\|A\| - 1 - 1))$
114	12	fveq2i	$⊢ A (K) = A (\|A\| - 1 - 1)$
115	114	fveq2i	$⊢ T (A (K)) = T (A (\|A\| - 1 - 1))$
116	115	rneqi	$⊢ ran T (A (K)) = ran T (A (\|A\| - 1 - 1))$
117	113 116	eleqtrrdi	$⊢ φ \to S (A) \in ran T (A (K))$
118	1 2 3 4	efgtlen	$⊢ (A (K) \in W \land S (A) \in ran T (A (K))) \to \|S (A)\| = \|A (K)\| + 2$
119	47 117 118	syl2anc	$⊢ φ \to \|S (A)\| = \|A (K)\| + 2$
120	88 111 119	3brtr4d	$⊢ φ \to \|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\|$
121	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	efgredleme	$⊢ φ \to (A (K) \in ran T (S (C)) \land B (L) \in ran T (S (C)))$
122	121	simpld	$⊢ φ \to A (K) \in ran T (S (C))$
123	1 2 3 4 5 6	efgsp1	$⊢ (C \in dom S \land A (K) \in ran T (S (C))) \to C ++ ⟨“ A (K) ”⟩ \in dom S$
124	22 122 123	syl2anc	$⊢ φ \to C ++ ⟨“ A (K) ”⟩ \in dom S$
125	1 2 3 4 5 6	efgsval2	$⊢ (C \in Word W \land A (K) \in W \land C ++ ⟨“ A (K) ”⟩ \in dom S) \to S (C ++ ⟨“ A (K) ”⟩) = A (K)$
126	27 47 124 125	syl3anc	$⊢ φ \to S (C ++ ⟨“ A (K) ”⟩) = A (K)$
127	110 126	eqtr4d	$⊢ φ \to S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (C ++ ⟨“ A (K) ”⟩)$
128		2fveq3	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to \|S (a)\| = \|S ({A ↾}_{(0 ..^\|A\| - 1)})\|$
129	128	breq1d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to (\|S (a)\| < \|S (A)\| \leftrightarrow \|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\|)$
130		fveqeq2	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to (S (a) = S (b) \leftrightarrow S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b))$
131		fveq1	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to a (0) = ({A ↾}_{(0 ..^\|A\| - 1)}) (0)$
132	131	eqeq1d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to (a (0) = b (0) \leftrightarrow ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0))$
133	130 132	imbi12d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to ((S (a) = S (b) \to a (0) = b (0)) \leftrightarrow (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0)))$
134	129 133	imbi12d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to ((\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0))) \leftrightarrow (\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0))))$
135		fveq2	$⊢ b = C ++ ⟨“ A (K) ”⟩ \to S (b) = S (C ++ ⟨“ A (K) ”⟩)$
136	135	eqeq2d	$⊢ b = C ++ ⟨“ A (K) ”⟩ \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \leftrightarrow S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (C ++ ⟨“ A (K) ”⟩))$
137		fveq1	$⊢ b = C ++ ⟨“ A (K) ”⟩ \to b (0) = (C ++ ⟨“ A (K) ”⟩) (0)$
138	137	eqeq2d	$⊢ b = C ++ ⟨“ A (K) ”⟩ \to (({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0) \leftrightarrow ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = (C ++ ⟨“ A (K) ”⟩) (0))$
139	136 138	imbi12d	$⊢ b = C ++ ⟨“ A (K) ”⟩ \to ((S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0)) \leftrightarrow (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (C ++ ⟨“ A (K) ”⟩) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = (C ++ ⟨“ A (K) ”⟩) (0)))$
140	139	imbi2d	$⊢ b = C ++ ⟨“ A (K) ”⟩ \to ((\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0))) \leftrightarrow (\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (C ++ ⟨“ A (K) ”⟩) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = (C ++ ⟨“ A (K) ”⟩) (0))))$
141	134 140	rspc2va	$⊢ (({A ↾}_{(0 ..^\|A\| - 1)} \in dom S \land C ++ ⟨“ A (K) ”⟩ \in dom S) \land \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))) \to (\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (C ++ ⟨“ A (K) ”⟩) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = (C ++ ⟨“ A (K) ”⟩) (0)))$
142	95 124 7 141	syl21anc	$⊢ φ \to (\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (C ++ ⟨“ A (K) ”⟩) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = (C ++ ⟨“ A (K) ”⟩) (0)))$
143	120 127 142	mp2d	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = (C ++ ⟨“ A (K) ”⟩) (0)$
144	81 75	sselid	$⊢ φ \to B (L) \in Word (I \times 2_{𝑜})$
145		lencl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to \|B (L)\| \in ℕ_{0}$
146	144 145	syl	$⊢ φ \to \|B (L)\| \in ℕ_{0}$
147	146	nn0red	$⊢ φ \to \|B (L)\| \in ℝ$
148		ltaddrp	$⊢ (\|B (L)\| \in ℝ \land 2 \in ℝ^{+}) \to \|B (L)\| < \|B (L)\| + 2$
149	147 86 148	sylancl	$⊢ φ \to \|B (L)\| < \|B (L)\| + 2$
150	65	nn0red	$⊢ φ \to \|B\| \in ℝ$
151	150	lem1d	$⊢ φ \to \|B\| - 1 \leq \|B\|$
152		fznn	$⊢ \|B\| \in ℤ \to (\|B\| - 1 \in (1 \dots \|B\|) \leftrightarrow (\|B\| - 1 \in ℕ \land \|B\| - 1 \leq \|B\|))$
153	66 152	syl	$⊢ φ \to (\|B\| - 1 \in (1 \dots \|B\|) \leftrightarrow (\|B\| - 1 \in ℕ \land \|B\| - 1 \leq \|B\|))$
154	70 151 153	mpbir2and	$⊢ φ \to \|B\| - 1 \in (1 \dots \|B\|)$
155	1 2 3 4 5 6	efgsres	$⊢ (B \in dom S \land \|B\| - 1 \in (1 \dots \|B\|)) \to {B ↾}_{(0 ..^\|B\| - 1)} \in dom S$
156	9 154 155	syl2anc	$⊢ φ \to {B ↾}_{(0 ..^\|B\| - 1)} \in dom S$
157	1 2 3 4 5 6	efgsval	$⊢ {B ↾}_{(0 ..^\|B\| - 1)} \in dom S \to S ({B ↾}_{(0 ..^\|B\| - 1)}) = ({B ↾}_{(0 ..^\|B\| - 1)}) (\|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1)$
158	156 157	syl	$⊢ φ \to S ({B ↾}_{(0 ..^\|B\| - 1)}) = ({B ↾}_{(0 ..^\|B\| - 1)}) (\|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1)$
159		fz1ssfz0	$⊢ (1 \dots \|B\|) \subseteq (0 \dots \|B\|)$
160	159 154	sselid	$⊢ φ \to \|B\| - 1 \in (0 \dots \|B\|)$
161		pfxres	$⊢ (B \in Word W \land \|B\| - 1 \in (0 \dots \|B\|)) \to B prefix (\|B\| - 1) = {B ↾}_{(0 ..^\|B\| - 1)}$
162	60 160 161	syl2anc	$⊢ φ \to B prefix (\|B\| - 1) = {B ↾}_{(0 ..^\|B\| - 1)}$
163	162	fveq2d	$⊢ φ \to \|B prefix (\|B\| - 1)\| = \|{B ↾}_{(0 ..^\|B\| - 1)}\|$
164		pfxlen	$⊢ (B \in Word W \land \|B\| - 1 \in (0 \dots \|B\|)) \to \|B prefix (\|B\| - 1)\| = \|B\| - 1$
165	60 160 164	syl2anc	$⊢ φ \to \|B prefix (\|B\| - 1)\| = \|B\| - 1$
166	163 165	eqtr3d	$⊢ φ \to \|{B ↾}_{(0 ..^\|B\| - 1)}\| = \|B\| - 1$
167	166	oveq1d	$⊢ φ \to \|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1 = \|B\| - 1 - 1$
168	167 13	eqtr4di	$⊢ φ \to \|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1 = L$
169	168	fveq2d	$⊢ φ \to ({B ↾}_{(0 ..^\|B\| - 1)}) (\|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1) = ({B ↾}_{(0 ..^\|B\| - 1)}) (L)$
170	73	fvresd	$⊢ φ \to ({B ↾}_{(0 ..^\|B\| - 1)}) (L) = B (L)$
171	158 169 170	3eqtrd	$⊢ φ \to S ({B ↾}_{(0 ..^\|B\| - 1)}) = B (L)$
172	171	fveq2d	$⊢ φ \to \|S ({B ↾}_{(0 ..^\|B\| - 1)})\| = \|B (L)\|$
173	1 2 3 4 5 6	efgsdmi	$⊢ (B \in dom S \land \|B\| - 1 \in ℕ) \to S (B) \in ran T (B (\|B\| - 1 - 1))$
174	9 70 173	syl2anc	$⊢ φ \to S (B) \in ran T (B (\|B\| - 1 - 1))$
175	10 174	eqeltrd	$⊢ φ \to S (A) \in ran T (B (\|B\| - 1 - 1))$
176	13	fveq2i	$⊢ B (L) = B (\|B\| - 1 - 1)$
177	176	fveq2i	$⊢ T (B (L)) = T (B (\|B\| - 1 - 1))$
178	177	rneqi	$⊢ ran T (B (L)) = ran T (B (\|B\| - 1 - 1))$
179	175 178	eleqtrrdi	$⊢ φ \to S (A) \in ran T (B (L))$
180	1 2 3 4	efgtlen	$⊢ (B (L) \in W \land S (A) \in ran T (B (L))) \to \|S (A)\| = \|B (L)\| + 2$
181	75 179 180	syl2anc	$⊢ φ \to \|S (A)\| = \|B (L)\| + 2$
182	149 172 181	3brtr4d	$⊢ φ \to \|S ({B ↾}_{(0 ..^\|B\| - 1)})\| < \|S (A)\|$
183	121	simprd	$⊢ φ \to B (L) \in ran T (S (C))$
184	1 2 3 4 5 6	efgsp1	$⊢ (C \in dom S \land B (L) \in ran T (S (C))) \to C ++ ⟨“ B (L) ”⟩ \in dom S$
185	22 183 184	syl2anc	$⊢ φ \to C ++ ⟨“ B (L) ”⟩ \in dom S$
186	1 2 3 4 5 6	efgsval2	$⊢ (C \in Word W \land B (L) \in W \land C ++ ⟨“ B (L) ”⟩ \in dom S) \to S (C ++ ⟨“ B (L) ”⟩) = B (L)$
187	27 75 185 186	syl3anc	$⊢ φ \to S (C ++ ⟨“ B (L) ”⟩) = B (L)$
188	171 187	eqtr4d	$⊢ φ \to S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (C ++ ⟨“ B (L) ”⟩)$
189		2fveq3	$⊢ a = {B ↾}_{(0 ..^\|B\| - 1)} \to \|S (a)\| = \|S ({B ↾}_{(0 ..^\|B\| - 1)})\|$
190	189	breq1d	$⊢ a = {B ↾}_{(0 ..^\|B\| - 1)} \to (\|S (a)\| < \|S (A)\| \leftrightarrow \|S ({B ↾}_{(0 ..^\|B\| - 1)})\| < \|S (A)\|)$
191		fveqeq2	$⊢ a = {B ↾}_{(0 ..^\|B\| - 1)} \to (S (a) = S (b) \leftrightarrow S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (b))$
192		fveq1	$⊢ a = {B ↾}_{(0 ..^\|B\| - 1)} \to a (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0)$
193	192	eqeq1d	$⊢ a = {B ↾}_{(0 ..^\|B\| - 1)} \to (a (0) = b (0) \leftrightarrow ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = b (0))$
194	191 193	imbi12d	$⊢ a = {B ↾}_{(0 ..^\|B\| - 1)} \to ((S (a) = S (b) \to a (0) = b (0)) \leftrightarrow (S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (b) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = b (0)))$
195	190 194	imbi12d	$⊢ a = {B ↾}_{(0 ..^\|B\| - 1)} \to ((\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0))) \leftrightarrow (\|S ({B ↾}_{(0 ..^\|B\| - 1)})\| < \|S (A)\| \to (S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (b) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = b (0))))$
196		fveq2	$⊢ b = C ++ ⟨“ B (L) ”⟩ \to S (b) = S (C ++ ⟨“ B (L) ”⟩)$
197	196	eqeq2d	$⊢ b = C ++ ⟨“ B (L) ”⟩ \to (S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (b) \leftrightarrow S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (C ++ ⟨“ B (L) ”⟩))$
198		fveq1	$⊢ b = C ++ ⟨“ B (L) ”⟩ \to b (0) = (C ++ ⟨“ B (L) ”⟩) (0)$
199	198	eqeq2d	$⊢ b = C ++ ⟨“ B (L) ”⟩ \to (({B ↾}_{(0 ..^\|B\| - 1)}) (0) = b (0) \leftrightarrow ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = (C ++ ⟨“ B (L) ”⟩) (0))$
200	197 199	imbi12d	$⊢ b = C ++ ⟨“ B (L) ”⟩ \to ((S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (b) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = b (0)) \leftrightarrow (S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (C ++ ⟨“ B (L) ”⟩) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = (C ++ ⟨“ B (L) ”⟩) (0)))$
201	200	imbi2d	$⊢ b = C ++ ⟨“ B (L) ”⟩ \to ((\|S ({B ↾}_{(0 ..^\|B\| - 1)})\| < \|S (A)\| \to (S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (b) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = b (0))) \leftrightarrow (\|S ({B ↾}_{(0 ..^\|B\| - 1)})\| < \|S (A)\| \to (S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (C ++ ⟨“ B (L) ”⟩) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = (C ++ ⟨“ B (L) ”⟩) (0))))$
202	195 201	rspc2va	$⊢ (({B ↾}_{(0 ..^\|B\| - 1)} \in dom S \land C ++ ⟨“ B (L) ”⟩ \in dom S) \land \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))) \to (\|S ({B ↾}_{(0 ..^\|B\| - 1)})\| < \|S (A)\| \to (S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (C ++ ⟨“ B (L) ”⟩) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = (C ++ ⟨“ B (L) ”⟩) (0)))$
203	156 185 7 202	syl21anc	$⊢ φ \to (\|S ({B ↾}_{(0 ..^\|B\| - 1)})\| < \|S (A)\| \to (S ({B ↾}_{(0 ..^\|B\| - 1)}) = S (C ++ ⟨“ B (L) ”⟩) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = (C ++ ⟨“ B (L) ”⟩) (0)))$
204	182 188 203	mp2d	$⊢ φ \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = (C ++ ⟨“ B (L) ”⟩) (0)$
205	79 143 204	3eqtr4d	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0)$
206		lbfzo0	$⊢ 0 \in (0 ..^\|A\| - 1) \leftrightarrow \|A\| - 1 \in ℕ$
207	42 206	sylibr	$⊢ φ \to 0 \in (0 ..^\|A\| - 1)$
208	207	fvresd	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = A (0)$
209		lbfzo0	$⊢ 0 \in (0 ..^\|B\| - 1) \leftrightarrow \|B\| - 1 \in ℕ$
210	70 209	sylibr	$⊢ φ \to 0 \in (0 ..^\|B\| - 1)$
211	210	fvresd	$⊢ φ \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = B (0)$
212	205 208 211	3eqtr3d	$⊢ φ \to A (0) = B (0)$

Metamath Proof Explorer

Theorem efgredlemd

Proof