Metamath Proof Explorer


Theorem efgs1b

Description: Every extension sequence ending in an irreducible word is trivial. (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
Assertion efgs1b A dom S S A D A = 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 eldifn S A W x W ran T x ¬ S A x W ran T x
8 7 5 eleq2s S A D ¬ S A x W ran T x
9 1 2 3 4 5 6 efgsdm A dom S A Word W A 0 D a 1 ..^ A A a ran T A a 1
10 9 simp1bi A dom S A Word W
11 eldifsn A Word W A Word W A
12 lennncl A Word W A A
13 11 12 sylbi A Word W A
14 10 13 syl A dom S A
15 elnn1uz2 A A = 1 A 2
16 14 15 sylib A dom S A = 1 A 2
17 16 ord A dom S ¬ A = 1 A 2
18 10 eldifad A dom S A Word W
19 18 adantr A dom S A 2 A Word W
20 wrdf A Word W A : 0 ..^ A W
21 19 20 syl A dom S A 2 A : 0 ..^ A W
22 1z 1
23 simpr A dom S A 2 A 2
24 df-2 2 = 1 + 1
25 24 fveq2i 2 = 1 + 1
26 23 25 eleqtrdi A dom S A 2 A 1 + 1
27 eluzp1m1 1 A 1 + 1 A 1 1
28 22 26 27 sylancr A dom S A 2 A 1 1
29 nnuz = 1
30 28 29 eleqtrrdi A dom S A 2 A 1
31 lbfzo0 0 0 ..^ A 1 A 1
32 30 31 sylibr A dom S A 2 0 0 ..^ A 1
33 fzoend 0 0 ..^ A 1 A - 1 - 1 0 ..^ A 1
34 elfzofz A - 1 - 1 0 ..^ A 1 A - 1 - 1 0 A 1
35 32 33 34 3syl A dom S A 2 A - 1 - 1 0 A 1
36 eluzelz A 2 A
37 36 adantl A dom S A 2 A
38 fzoval A 0 ..^ A = 0 A 1
39 37 38 syl A dom S A 2 0 ..^ A = 0 A 1
40 35 39 eleqtrrd A dom S A 2 A - 1 - 1 0 ..^ A
41 21 40 ffvelrnd A dom S A 2 A A - 1 - 1 W
42 uz2m1nn A 2 A 1
43 1 2 3 4 5 6 efgsdmi A dom S A 1 S A ran T A A - 1 - 1
44 42 43 sylan2 A dom S A 2 S A ran T A A - 1 - 1
45 fveq2 a = A A - 1 - 1 T a = T A A - 1 - 1
46 45 rneqd a = A A - 1 - 1 ran T a = ran T A A - 1 - 1
47 46 eliuni A A - 1 - 1 W S A ran T A A - 1 - 1 S A a W ran T a
48 41 44 47 syl2anc A dom S A 2 S A a W ran T a
49 fveq2 a = x T a = T x
50 49 rneqd a = x ran T a = ran T x
51 50 cbviunv a W ran T a = x W ran T x
52 48 51 eleqtrdi A dom S A 2 S A x W ran T x
53 52 ex A dom S A 2 S A x W ran T x
54 17 53 syld A dom S ¬ A = 1 S A x W ran T x
55 54 con1d A dom S ¬ S A x W ran T x A = 1
56 8 55 syl5 A dom S S A D A = 1
57 9 simp2bi A dom S A 0 D
58 oveq1 A = 1 A 1 = 1 1
59 1m1e0 1 1 = 0
60 58 59 eqtrdi A = 1 A 1 = 0
61 60 fveq2d A = 1 A A 1 = A 0
62 61 eleq1d A = 1 A A 1 D A 0 D
63 57 62 syl5ibrcom A dom S A = 1 A A 1 D
64 1 2 3 4 5 6 efgsval A dom S S A = A A 1
65 64 eleq1d A dom S S A D A A 1 D
66 63 65 sylibrd A dom S A = 1 S A D
67 56 66 impbid A dom S S A D A = 1