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⁡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 efgsf ⊢S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W

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 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∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1m⁡m−1∈W↔∀t∈WordW∖∅t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1→t⁡t−1∈W
13 eldifi ⊢t∈WordW∖∅→t∈WordW
14 wrdf ⊢t∈WordW→t:0..^t⟶W
15 13 14 syl ⊢t∈WordW∖∅→t:0..^t⟶W
16 eldifsn ⊢t∈WordW∖∅↔t∈WordW∧t≠∅
17 lennncl ⊢t∈WordW∧t≠∅→t∈ℕ
18 16 17 sylbi ⊢t∈WordW∖∅→t∈ℕ
19 fzo0end ⊢t∈ℕ→t−1∈0..^t
20 18 19 syl ⊢t∈WordW∖∅→t−1∈0..^t
21 15 20 ffvelcdmd ⊢t∈WordW∖∅→t⁡t−1∈W
22 21 a1d ⊢t∈WordW∖∅→t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1→t⁡t−1∈W
23 12 22 mprgbir ⊢∀m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1m⁡m−1∈W
24 6 fmpt ⊢∀m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1m⁡m−1∈W↔S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W
25 23 24 mpbi ⊢S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W