Metamath Proof Explorer

Theorem efgsf

Description: Value of the auxiliary function S defining a sequence of extensions starting at some irreducible word. (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 efgsf ⊢ S : t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟶ W

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 id ⊢ m = t → m = t
8 fveq2 ⊢ m = t → m = t
9 8 oveq1d ⊢ m = t → m − 1 = t − 1
10 7 9 fveq12d ⊢ m = t → m ⁡ m − 1 = t ⁡ t − 1
11 10 eleq1d ⊢ m = t → m ⁡ m − 1 ∈ W ↔ t ⁡ t − 1 ∈ W
12 11 ralrab2 ⊢ ∀ m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 m ⁡ m − 1 ∈ W ↔ ∀ t ∈ Word W ∖ ∅ t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 → t ⁡ t − 1 ∈ W
13 eldifi ⊢ t ∈ Word W ∖ ∅ → t ∈ Word W
14 wrdf ⊢ t ∈ Word W → t : 0 ..^ t ⟶ W
15 13 14 syl ⊢ t ∈ Word W ∖ ∅ → t : 0 ..^ t ⟶ W
16 eldifsn ⊢ t ∈ Word W ∖ ∅ ↔ t ∈ Word W ∧ t ≠ ∅
17 lennncl ⊢ t ∈ Word W ∧ t ≠ ∅ → t ∈ ℕ
18 16 17 sylbi ⊢ t ∈ Word W ∖ ∅ → t ∈ ℕ
19 fzo0end ⊢ t ∈ ℕ → t − 1 ∈ 0 ..^ t
20 18 19 syl ⊢ t ∈ Word W ∖ ∅ → t − 1 ∈ 0 ..^ t
21 15 20 ffvelrnd ⊢ t ∈ Word W ∖ ∅ → t ⁡ t − 1 ∈ W
22 21 a1d ⊢ t ∈ Word W ∖ ∅ → t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 → t ⁡ t − 1 ∈ W
23 12 22 mprgbir ⊢ ∀ m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 m ⁡ m − 1 ∈ W
24 6 fmpt ⊢ ∀ m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 m ⁡ m − 1 ∈ W ↔ S : t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟶ W
25 23 24 mpbi ⊢ S : t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟶ W