Metamath Proof Explorer

Theorem efgredlemb

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015)

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
Assertion efgredlemb ⊢ ¬ φ

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 fveq2 ⊢ S ⁡ A = S ⁡ B → S ⁡ A = S ⁡ B
22 21 breq2d ⊢ S ⁡ A = S ⁡ B → S ⁡ a < S ⁡ A ↔ S ⁡ a < S ⁡ B
23 22 imbi1d ⊢ S ⁡ A = S ⁡ B → S ⁡ a < S ⁡ A → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < S ⁡ B → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
24 23 2ralbidv ⊢ S ⁡ A = S ⁡ B → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ B → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
25 10 24 syl ⊢ φ → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ B → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
26 7 25 mpbid ⊢ φ → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ B → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
27 10 eqcomd ⊢ φ → S ⁡ B = S ⁡ A
28 eqcom ⊢ A ⁡ 0 = B ⁡ 0 ↔ B ⁡ 0 = A ⁡ 0
29 11 28 sylnib ⊢ φ → ¬ B ⁡ 0 = A ⁡ 0
30 eqcom ⊢ A ⁡ K = B ⁡ L ↔ B ⁡ L = A ⁡ K
31 20 30 sylnib ⊢ φ → ¬ B ⁡ L = A ⁡ K
32 1 2 3 4 5 6 26 9 8 27 29 13 12 15 14 17 16 19 18 31 efgredlemc ⊢ φ → Q ∈ ℤ ≥ P → B ⁡ 0 = A ⁡ 0
33 32 28 imbitrrdi ⊢ φ → Q ∈ ℤ ≥ P → A ⁡ 0 = B ⁡ 0
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 efgredlemc ⊢ φ → P ∈ ℤ ≥ Q → A ⁡ 0 = B ⁡ 0
35 14 elfzelzd ⊢ φ → P ∈ ℤ
36 15 elfzelzd ⊢ φ → Q ∈ ℤ
37 uztric ⊢ P ∈ ℤ ∧ Q ∈ ℤ → Q ∈ ℤ ≥ P ∨ P ∈ ℤ ≥ Q
38 35 36 37 syl2anc ⊢ φ → Q ∈ ℤ ≥ P ∨ P ∈ ℤ ≥ Q
39 33 34 38 mpjaod ⊢ φ → A ⁡ 0 = B ⁡ 0
40 39 11 pm2.65i ⊢ ¬ φ