Metamath Proof Explorer

Theorem efgs1

Description: A singleton of an irreducible word is an extension sequence. (Contributed by Mario Carneiro, 27-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 efgs1 ⊢A∈D→⟨“A”⟩∈dom⁡S

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 eldifi ⊢A∈W∖⋃x∈Wran⁡T⁡x→A∈W
8 7 5 eleq2s ⊢A∈D→A∈W
9 8 s1cld ⊢A∈D→⟨“A”⟩∈WordW
10 s1nz ⊢⟨“A”⟩≠∅
11 eldifsn ⊢⟨“A”⟩∈WordW∖∅↔⟨“A”⟩∈WordW∧⟨“A”⟩≠∅
12 9 10 11 sylanblrc ⊢A∈D→⟨“A”⟩∈WordW∖∅
13 s1fv ⊢A∈D→⟨“A”⟩⁡0=A
14 id ⊢A∈D→A∈D
15 13 14 eqeltrd ⊢A∈D→⟨“A”⟩⁡0∈D
16 s1len ⊢⟨“A”⟩=1
17 16 a1i ⊢A∈D→⟨“A”⟩=1
18 17 oveq2d ⊢A∈D→1..^⟨“A”⟩=1..^1
19 fzo0 ⊢1..^1=∅
20 18 19 eqtrdi ⊢A∈D→1..^⟨“A”⟩=∅
21 rzal ⊢1..^⟨“A”⟩=∅→∀i∈1..^⟨“A”⟩⟨“A”⟩⁡i∈ran⁡T⁡⟨“A”⟩⁡i−1
22 20 21 syl ⊢A∈D→∀i∈1..^⟨“A”⟩⟨“A”⟩⁡i∈ran⁡T⁡⟨“A”⟩⁡i−1
23 1 2 3 4 5 6 efgsdm ⊢⟨“A”⟩∈dom⁡S↔⟨“A”⟩∈WordW∖∅∧⟨“A”⟩⁡0∈D∧∀i∈1..^⟨“A”⟩⟨“A”⟩⁡i∈ran⁡T⁡⟨“A”⟩⁡i−1
24 12 15 22 23 syl3anbrc ⊢A∈D→⟨“A”⟩∈dom⁡S