Metamath Proof Explorer

Theorem efgredlema

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)

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
Assertion efgredlema ⊢ φ → A − 1 ∈ ℕ ∧ B − 1 ∈ ℕ

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 1 2 3 4 5 6 efgsval ⊢ B ∈ dom ⁡ S → S ⁡ B = B ⁡ B − 1
13 9 12 syl ⊢ φ → S ⁡ B = B ⁡ B − 1
14 1 2 3 4 5 6 efgsval ⊢ A ∈ dom ⁡ S → S ⁡ A = A ⁡ A − 1
15 8 14 syl ⊢ φ → S ⁡ A = A ⁡ A − 1
16 10 15 eqtr3d ⊢ φ → S ⁡ B = A ⁡ A − 1
17 13 16 eqtr3d ⊢ φ → B ⁡ B − 1 = A ⁡ A − 1
18 oveq1 ⊢ A = 1 → A − 1 = 1 − 1
19 1m1e0 ⊢ 1 − 1 = 0
20 18 19 eqtrdi ⊢ A = 1 → A − 1 = 0
21 20 fveq2d ⊢ A = 1 → A ⁡ A − 1 = A ⁡ 0
22 17 21 sylan9eq ⊢ φ ∧ A = 1 → B ⁡ B − 1 = A ⁡ 0
23 10 eleq1d ⊢ φ → S ⁡ A ∈ D ↔ S ⁡ B ∈ D
24 1 2 3 4 5 6 efgs1b ⊢ A ∈ dom ⁡ S → S ⁡ A ∈ D ↔ A = 1
25 8 24 syl ⊢ φ → S ⁡ A ∈ D ↔ A = 1
26 1 2 3 4 5 6 efgs1b ⊢ B ∈ dom ⁡ S → S ⁡ B ∈ D ↔ B = 1
27 9 26 syl ⊢ φ → S ⁡ B ∈ D ↔ B = 1
28 23 25 27 3bitr3d ⊢ φ → A = 1 ↔ B = 1
29 28 biimpa ⊢ φ ∧ A = 1 → B = 1
30 oveq1 ⊢ B = 1 → B − 1 = 1 − 1
31 30 19 eqtrdi ⊢ B = 1 → B − 1 = 0
32 31 fveq2d ⊢ B = 1 → B ⁡ B − 1 = B ⁡ 0
33 29 32 syl ⊢ φ ∧ A = 1 → B ⁡ B − 1 = B ⁡ 0
34 22 33 eqtr3d ⊢ φ ∧ A = 1 → A ⁡ 0 = B ⁡ 0
35 11 34 mtand ⊢ φ → ¬ A = 1
36 1 2 3 4 5 6 efgsdm ⊢ A ∈ dom ⁡ S ↔ A ∈ Word W ∖ ∅ ∧ A ⁡ 0 ∈ D ∧ ∀ u ∈ 1 ..^ A A ⁡ u ∈ ran ⁡ T ⁡ A ⁡ u − 1
37 36 simp1bi ⊢ A ∈ dom ⁡ S → A ∈ Word W ∖ ∅
38 eldifsn ⊢ A ∈ Word W ∖ ∅ ↔ A ∈ Word W ∧ A ≠ ∅
39 lennncl ⊢ A ∈ Word W ∧ A ≠ ∅ → A ∈ ℕ
40 38 39 sylbi ⊢ A ∈ Word W ∖ ∅ → A ∈ ℕ
41 8 37 40 3syl ⊢ φ → A ∈ ℕ
42 elnn1uz2 ⊢ A ∈ ℕ ↔ A = 1 ∨ A ∈ ℤ ≥ 2
43 41 42 sylib ⊢ φ → A = 1 ∨ A ∈ ℤ ≥ 2
44 43 ord ⊢ φ → ¬ A = 1 → A ∈ ℤ ≥ 2
45 35 44 mpd ⊢ φ → A ∈ ℤ ≥ 2
46 uz2m1nn ⊢ A ∈ ℤ ≥ 2 → A − 1 ∈ ℕ
47 45 46 syl ⊢ φ → A − 1 ∈ ℕ
48 35 28 mtbid ⊢ φ → ¬ B = 1
49 1 2 3 4 5 6 efgsdm ⊢ B ∈ dom ⁡ S ↔ B ∈ Word W ∖ ∅ ∧ B ⁡ 0 ∈ D ∧ ∀ u ∈ 1 ..^ B B ⁡ u ∈ ran ⁡ T ⁡ B ⁡ u − 1
50 49 simp1bi ⊢ B ∈ dom ⁡ S → B ∈ Word W ∖ ∅
51 eldifsn ⊢ B ∈ Word W ∖ ∅ ↔ B ∈ Word W ∧ B ≠ ∅
52 lennncl ⊢ B ∈ Word W ∧ B ≠ ∅ → B ∈ ℕ
53 51 52 sylbi ⊢ B ∈ Word W ∖ ∅ → B ∈ ℕ
54 9 50 53 3syl ⊢ φ → B ∈ ℕ
55 elnn1uz2 ⊢ B ∈ ℕ ↔ B = 1 ∨ B ∈ ℤ ≥ 2
56 54 55 sylib ⊢ φ → B = 1 ∨ B ∈ ℤ ≥ 2
57 56 ord ⊢ φ → ¬ B = 1 → B ∈ ℤ ≥ 2
58 48 57 mpd ⊢ φ → B ∈ ℤ ≥ 2
59 uz2m1nn ⊢ B ∈ ℤ ≥ 2 → B − 1 ∈ ℕ
60 58 59 syl ⊢ φ → B − 1 ∈ ℕ
61 47 60 jca ⊢ φ → A − 1 ∈ ℕ ∧ B − 1 ∈ ℕ