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 syl6ibr φ 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 ¬ φ