Metamath Proof Explorer

Theorem 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 × 2 𝑜
efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
efgredlem.1 ⊢ φ → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
efgredlem.2 ⊢ φ → A ∈ dom ⁡ S
efgredlem.3 ⊢ φ → B ∈ dom ⁡ S
efgredlem.4 ⊢ φ → S ⁡ A = S ⁡ B
efgredlem.5 ⊢ φ → ¬ A ⁡ 0 = B ⁡ 0
efgredlemb.k ⊢ K = A - 1 - 1
efgredlemb.l ⊢ L = B - 1 - 1
efgredlemb.p ⊢ φ → P ∈ 0 … A ⁡ K
efgredlemb.q ⊢ φ → Q ∈ 0 … B ⁡ L
efgredlemb.u ⊢ φ → U ∈ I × 2 𝑜
efgredlemb.v ⊢ φ → V ∈ I × 2 𝑜
efgredlemb.6 ⊢ φ → S ⁡ A = P T ⁡ A ⁡ K U
efgredlemb.7 ⊢ φ → S ⁡ B = Q T ⁡ B ⁡ L V
efgredlemb.8 ⊢ φ → ¬ A ⁡ K = B ⁡ L
efgredlemd.9 ⊢ φ → P ∈ ℤ ≥ Q + 2
efgredlemd.c ⊢ φ → C ∈ dom ⁡ S
efgredlemd.sc ⊢ φ → S ⁡ C = B ⁡ L prefix Q ++ A ⁡ K substr Q + 2 A ⁡ K
Assertion efgredlemd ⊢ φ → A ⁡ 0 = B ⁡ 0

Proof

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