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 ⁡ 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 efgs1 ⊢ A ∈ D → ⟨“ A ”⟩ ∈ dom ⁡ S

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 eldifi ⊢ A ∈ W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x → A ∈ W
8 7 5 eleq2s ⊢ A ∈ D → A ∈ W
9 8 s1cld ⊢ A ∈ D → ⟨“ A ”⟩ ∈ Word W
10 s1nz ⊢ ⟨“ A ”⟩ ≠ ∅
11 eldifsn ⊢ ⟨“ A ”⟩ ∈ Word W ∖ ∅ ↔ ⟨“ A ”⟩ ∈ Word W ∧ ⟨“ A ”⟩ ≠ ∅
12 9 10 11 sylanblrc ⊢ A ∈ D → ⟨“ A ”⟩ ∈ Word W ∖ ∅
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 ”⟩ ∈ Word W ∖ ∅ ∧ ⟨“ A ”⟩ ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ ⟨“ A ”⟩ ⟨“ A ”⟩ ⁡ i ∈ ran ⁡ T ⁡ ⟨“ A ”⟩ ⁡ i − 1
24 12 15 22 23 syl3anbrc ⊢ A ∈ D → ⟨“ A ”⟩ ∈ dom ⁡ S