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⁡WordI×2𝑜
efgval.r ⊢∼˙=~FG⁡I
efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
efgredlem.1 ⊢φ→∀a∈dom⁡S∀b∈dom⁡SS⁡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⁡WordI×2𝑜
2 efgval.r ⊢∼˙=~FG⁡I
3 efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
4 efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
5 efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
6 efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
7 efgredlem.1 ⊢φ→∀a∈dom⁡S∀b∈dom⁡SS⁡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∈WordW∖∅∧A⁡0∈D∧∀u∈1..^AA⁡u∈ran⁡T⁡A⁡u−1
37 36 simp1bi ⊢A∈dom⁡S→A∈WordW∖∅
38 eldifsn ⊢A∈WordW∖∅↔A∈WordW∧A≠∅
39 lennncl ⊢A∈WordW∧A≠∅→A∈ℕ
40 38 39 sylbi ⊢A∈WordW∖∅→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∈WordW∖∅∧B⁡0∈D∧∀u∈1..^BB⁡u∈ran⁡T⁡B⁡u−1
50 49 simp1bi ⊢B∈dom⁡S→B∈WordW∖∅
51 eldifsn ⊢B∈WordW∖∅↔B∈WordW∧B≠∅
52 lennncl ⊢B∈WordW∧B≠∅→B∈ℕ
53 51 52 sylbi ⊢B∈WordW∖∅→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∈ℕ