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 ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
Assertion efgs1 ( 𝐴 ∈ 𝐷 → ⟨“ 𝐴 ”⟩ ∈ dom 𝑆 )

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4 efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5 efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6 efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7 eldifi ⊢ ( 𝐴 ∈ ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → 𝐴 ∈ 𝑊 )
8 7 5 eleq2s ⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ∈ 𝑊 )
9 8 s1cld ⊢ ( 𝐴 ∈ 𝐷 → ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 )
10 s1nz ⊢ ⟨“ 𝐴 ”⟩ ≠ ∅
11 eldifsn ⊢ ( ⟨“ 𝐴 ”⟩ ∈ ( Word 𝑊 ∖ { ∅ } ) ↔ ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ≠ ∅ ) )
12 9 10 11 sylanblrc ⊢ ( 𝐴 ∈ 𝐷 → ⟨“ 𝐴 ”⟩ ∈ ( Word 𝑊 ∖ { ∅ } ) )
13 s1fv ⊢ ( 𝐴 ∈ 𝐷 → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) = 𝐴 )
14 id ⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ∈ 𝐷 )
15 13 14 eqeltrd ⊢ ( 𝐴 ∈ 𝐷 → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) ∈ 𝐷 )
16 s1len ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1
17 16 a1i ⊢ ( 𝐴 ∈ 𝐷 → ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1 )
18 17 oveq2d ⊢ ( 𝐴 ∈ 𝐷 → ( 1 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) = ( 1 ..^ 1 ) )
19 fzo0 ⊢ ( 1 ..^ 1 ) = ∅
20 18 19 eqtrdi ⊢ ( 𝐴 ∈ 𝐷 → ( 1 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) = ∅ )
21 rzal ⊢ ( ( 1 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) = ∅ → ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) ( ⟨“ 𝐴 ”⟩ ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ⟨“ 𝐴 ”⟩ ‘ ( 𝑖 − 1 ) ) ) )
22 20 21 syl ⊢ ( 𝐴 ∈ 𝐷 → ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) ( ⟨“ 𝐴 ”⟩ ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ⟨“ 𝐴 ”⟩ ‘ ( 𝑖 − 1 ) ) ) )
23 1 2 3 4 5 6 efgsdm ⊢ ( ⟨“ 𝐴 ”⟩ ∈ dom 𝑆 ↔ ( ⟨“ 𝐴 ”⟩ ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( ⟨“ 𝐴 ”⟩ ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) ( ⟨“ 𝐴 ”⟩ ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ⟨“ 𝐴 ”⟩ ‘ ( 𝑖 − 1 ) ) ) ) )
24 12 15 22 23 syl3anbrc ⊢ ( 𝐴 ∈ 𝐷 → ⟨“ 𝐴 ”⟩ ∈ dom 𝑆 )