Metamath Proof Explorer

Theorem efgred

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the terminal point. (Contributed by Mario Carneiro, 28-Sep-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
Assertion efgred ⊢A∈dom⁡S∧B∈dom⁡S∧S⁡A=S⁡B→A⁡0=B⁡0

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 fviss ⊢I⁡WordI×2𝑜⊆WordI×2𝑜
8 1 7 eqsstri ⊢W⊆WordI×2𝑜
9 1 2 3 4 5 6 efgsf ⊢S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W
10 9 fdmi ⊢dom⁡S=t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1
11 10 feq2i ⊢S:dom⁡S⟶W↔S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W
12 9 11 mpbir ⊢S:dom⁡S⟶W
13 12 ffvelcdmi ⊢A∈dom⁡S→S⁡A∈W
14 13 adantr ⊢A∈dom⁡S∧B∈dom⁡S→S⁡A∈W
15 8 14 sselid ⊢A∈dom⁡S∧B∈dom⁡S→S⁡A∈WordI×2𝑜
16 lencl ⊢S⁡A∈WordI×2𝑜→S⁡A∈ℕ0
17 15 16 syl ⊢A∈dom⁡S∧B∈dom⁡S→S⁡A∈ℕ0
18 peano2nn0 ⊢S⁡A∈ℕ0→S⁡A+1∈ℕ0
19 17 18 syl ⊢A∈dom⁡S∧B∈dom⁡S→S⁡A+1∈ℕ0
20 breq2 ⊢c=0→S⁡a<c↔S⁡a<0
21 20 imbi1d ⊢c=0→S⁡a<c→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡a<0→S⁡a=S⁡b→a⁡0=b⁡0
22 21 2ralbidv ⊢c=0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<c→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<0→S⁡a=S⁡b→a⁡0=b⁡0
23 breq2 ⊢c=i→S⁡a<c↔S⁡a<i
24 23 imbi1d ⊢c=i→S⁡a<c→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0
25 24 2ralbidv ⊢c=i→∀a∈dom⁡S∀b∈dom⁡SS⁡a<c→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0
26 breq2 ⊢c=i+1→S⁡a<c↔S⁡a<i+1
27 26 imbi1d ⊢c=i+1→S⁡a<c→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡a<i+1→S⁡a=S⁡b→a⁡0=b⁡0
28 27 2ralbidv ⊢c=i+1→∀a∈dom⁡S∀b∈dom⁡SS⁡a<c→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<i+1→S⁡a=S⁡b→a⁡0=b⁡0
29 breq2 ⊢c=S⁡A+1→S⁡a<c↔S⁡a<S⁡A+1
30 29 imbi1d ⊢c=S⁡A+1→S⁡a<c→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡a<S⁡A+1→S⁡a=S⁡b→a⁡0=b⁡0
31 30 2ralbidv ⊢c=S⁡A+1→∀a∈dom⁡S∀b∈dom⁡SS⁡a<c→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<S⁡A+1→S⁡a=S⁡b→a⁡0=b⁡0
32 12 ffvelcdmi ⊢a∈dom⁡S→S⁡a∈W
33 8 32 sselid ⊢a∈dom⁡S→S⁡a∈WordI×2𝑜
34 lencl ⊢S⁡a∈WordI×2𝑜→S⁡a∈ℕ0
35 33 34 syl ⊢a∈dom⁡S→S⁡a∈ℕ0
36 nn0nlt0 ⊢S⁡a∈ℕ0→¬S⁡a<0
37 35 36 syl ⊢a∈dom⁡S→¬S⁡a<0
38 37 pm2.21d ⊢a∈dom⁡S→S⁡a<0→S⁡a=S⁡b→a⁡0=b⁡0
39 38 adantr ⊢a∈dom⁡S∧b∈dom⁡S→S⁡a<0→S⁡a=S⁡b→a⁡0=b⁡0
40 39 rgen2 ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<0→S⁡a=S⁡b→a⁡0=b⁡0
41 simpl1 ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0
42 simpl3l ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0→S⁡c=i
43 breq2 ⊢S⁡c=i→S⁡a<S⁡c↔S⁡a<i
44 43 imbi1d ⊢S⁡c=i→S⁡a<S⁡c→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0
45 44 2ralbidv ⊢S⁡c=i→∀a∈dom⁡S∀b∈dom⁡SS⁡a<S⁡c→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0
46 42 45 syl ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<S⁡c→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0
47 41 46 mpbird ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<S⁡c→S⁡a=S⁡b→a⁡0=b⁡0
48 simpl2l ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0→c∈dom⁡S
49 simpl2r ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0→d∈dom⁡S
50 simpl3r ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0→S⁡c=S⁡d
51 simpr ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0→¬c⁡0=d⁡0
52 1 2 3 4 5 6 47 48 49 50 51 efgredlem ⊢¬∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0
53 iman ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d→c⁡0=d⁡0↔¬∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d∧¬c⁡0=d⁡0
54 52 53 mpbir ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S∧S⁡c=i∧S⁡c=S⁡d→c⁡0=d⁡0
55 54 3expia ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S→S⁡c=i∧S⁡c=S⁡d→c⁡0=d⁡0
56 55 expd ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧c∈dom⁡S∧d∈dom⁡S→S⁡c=i→S⁡c=S⁡d→c⁡0=d⁡0
57 56 ralrimivva ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0→∀c∈dom⁡S∀d∈dom⁡SS⁡c=i→S⁡c=S⁡d→c⁡0=d⁡0
58 2fveq3 ⊢c=a→S⁡c=S⁡a
59 58 eqeq1d ⊢c=a→S⁡c=i↔S⁡a=i
60 fveqeq2 ⊢c=a→S⁡c=S⁡d↔S⁡a=S⁡d
61 fveq1 ⊢c=a→c⁡0=a⁡0
62 61 eqeq1d ⊢c=a→c⁡0=d⁡0↔a⁡0=d⁡0
63 60 62 imbi12d ⊢c=a→S⁡c=S⁡d→c⁡0=d⁡0↔S⁡a=S⁡d→a⁡0=d⁡0
64 59 63 imbi12d ⊢c=a→S⁡c=i→S⁡c=S⁡d→c⁡0=d⁡0↔S⁡a=i→S⁡a=S⁡d→a⁡0=d⁡0
65 fveq2 ⊢d=b→S⁡d=S⁡b
66 65 eqeq2d ⊢d=b→S⁡a=S⁡d↔S⁡a=S⁡b
67 fveq1 ⊢d=b→d⁡0=b⁡0
68 67 eqeq2d ⊢d=b→a⁡0=d⁡0↔a⁡0=b⁡0
69 66 68 imbi12d ⊢d=b→S⁡a=S⁡d→a⁡0=d⁡0↔S⁡a=S⁡b→a⁡0=b⁡0
70 69 imbi2d ⊢d=b→S⁡a=i→S⁡a=S⁡d→a⁡0=d⁡0↔S⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
71 64 70 cbvral2vw ⊢∀c∈dom⁡S∀d∈dom⁡SS⁡c=i→S⁡c=S⁡d→c⁡0=d⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
72 57 71 sylib ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0→∀a∈dom⁡S∀b∈dom⁡SS⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
73 72 ancli ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧∀a∈dom⁡S∀b∈dom⁡SS⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
74 35 adantr ⊢a∈dom⁡S∧b∈dom⁡S→S⁡a∈ℕ0
75 nn0leltp1 ⊢S⁡a∈ℕ0∧i∈ℕ0→S⁡a≤i↔S⁡a<i+1
76 nn0re ⊢S⁡a∈ℕ0→S⁡a∈ℝ
77 nn0re ⊢i∈ℕ0→i∈ℝ
78 leloe ⊢S⁡a∈ℝ∧i∈ℝ→S⁡a≤i↔S⁡a<i∨S⁡a=i
79 76 77 78 syl2an ⊢S⁡a∈ℕ0∧i∈ℕ0→S⁡a≤i↔S⁡a<i∨S⁡a=i
80 75 79 bitr3d ⊢S⁡a∈ℕ0∧i∈ℕ0→S⁡a<i+1↔S⁡a<i∨S⁡a=i
81 80 ancoms ⊢i∈ℕ0∧S⁡a∈ℕ0→S⁡a<i+1↔S⁡a<i∨S⁡a=i
82 74 81 sylan2 ⊢i∈ℕ0∧a∈dom⁡S∧b∈dom⁡S→S⁡a<i+1↔S⁡a<i∨S⁡a=i
83 82 imbi1d ⊢i∈ℕ0∧a∈dom⁡S∧b∈dom⁡S→S⁡a<i+1→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡a<i∨S⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
84 jaob ⊢S⁡a<i∨S⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧S⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
85 83 84 bitrdi ⊢i∈ℕ0∧a∈dom⁡S∧b∈dom⁡S→S⁡a<i+1→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧S⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
86 85 2ralbidva ⊢i∈ℕ0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<i+1→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧S⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
87 r19.26-2 ⊢∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧S⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧∀a∈dom⁡S∀b∈dom⁡SS⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
88 86 87 bitrdi ⊢i∈ℕ0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<i+1→S⁡a=S⁡b→a⁡0=b⁡0↔∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0∧∀a∈dom⁡S∀b∈dom⁡SS⁡a=i→S⁡a=S⁡b→a⁡0=b⁡0
89 73 88 imbitrrid ⊢i∈ℕ0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<i→S⁡a=S⁡b→a⁡0=b⁡0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<i+1→S⁡a=S⁡b→a⁡0=b⁡0
90 22 25 28 31 40 89 nn0ind ⊢S⁡A+1∈ℕ0→∀a∈dom⁡S∀b∈dom⁡SS⁡a<S⁡A+1→S⁡a=S⁡b→a⁡0=b⁡0
91 19 90 syl ⊢A∈dom⁡S∧B∈dom⁡S→∀a∈dom⁡S∀b∈dom⁡SS⁡a<S⁡A+1→S⁡a=S⁡b→a⁡0=b⁡0
92 17 nn0red ⊢A∈dom⁡S∧B∈dom⁡S→S⁡A∈ℝ
93 92 ltp1d ⊢A∈dom⁡S∧B∈dom⁡S→S⁡A<S⁡A+1
94 2fveq3 ⊢a=A→S⁡a=S⁡A
95 94 breq1d ⊢a=A→S⁡a<S⁡A+1↔S⁡A<S⁡A+1
96 fveqeq2 ⊢a=A→S⁡a=S⁡b↔S⁡A=S⁡b
97 fveq1 ⊢a=A→a⁡0=A⁡0
98 97 eqeq1d ⊢a=A→a⁡0=b⁡0↔A⁡0=b⁡0
99 96 98 imbi12d ⊢a=A→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡A=S⁡b→A⁡0=b⁡0
100 95 99 imbi12d ⊢a=A→S⁡a<S⁡A+1→S⁡a=S⁡b→a⁡0=b⁡0↔S⁡A<S⁡A+1→S⁡A=S⁡b→A⁡0=b⁡0
101 fveq2 ⊢b=B→S⁡b=S⁡B
102 101 eqeq2d ⊢b=B→S⁡A=S⁡b↔S⁡A=S⁡B
103 fveq1 ⊢b=B→b⁡0=B⁡0
104 103 eqeq2d ⊢b=B→A⁡0=b⁡0↔A⁡0=B⁡0
105 102 104 imbi12d ⊢b=B→S⁡A=S⁡b→A⁡0=b⁡0↔S⁡A=S⁡B→A⁡0=B⁡0
106 105 imbi2d ⊢b=B→S⁡A<S⁡A+1→S⁡A=S⁡b→A⁡0=b⁡0↔S⁡A<S⁡A+1→S⁡A=S⁡B→A⁡0=B⁡0
107 100 106 rspc2v ⊢A∈dom⁡S∧B∈dom⁡S→∀a∈dom⁡S∀b∈dom⁡SS⁡a<S⁡A+1→S⁡a=S⁡b→a⁡0=b⁡0→S⁡A<S⁡A+1→S⁡A=S⁡B→A⁡0=B⁡0
108 91 93 107 mp2d ⊢A∈dom⁡S∧B∈dom⁡S→S⁡A=S⁡B→A⁡0=B⁡0
109 108 3impia ⊢A∈dom⁡S∧B∈dom⁡S∧S⁡A=S⁡B→A⁡0=B⁡0