Metamath Proof Explorer

Theorem efgsval2

Description: Value of the auxiliary function S defining a sequence of extensions. (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 efgsval2 ⊢ A ∈ Word W ∧ B ∈ W ∧ A ++ ⟨“ B ”⟩ ∈ dom ⁡ S → S ⁡ A ++ ⟨“ B ”⟩ = B

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 1 2 3 4 5 6 efgsval ⊢ A ++ ⟨“ B ”⟩ ∈ dom ⁡ S → S ⁡ A ++ ⟨“ B ”⟩ = A ++ ⟨“ B ”⟩ ⁡ A ++ ⟨“ B ”⟩ − 1
8 s1cl ⊢ B ∈ W → ⟨“ B ”⟩ ∈ Word W
9 ccatlen ⊢ A ∈ Word W ∧ ⟨“ B ”⟩ ∈ Word W → A ++ ⟨“ B ”⟩ = A + ⟨“ B ”⟩
10 8 9 sylan2 ⊢ A ∈ Word W ∧ B ∈ W → A ++ ⟨“ B ”⟩ = A + ⟨“ B ”⟩
11 s1len ⊢ ⟨“ B ”⟩ = 1
12 11 oveq2i ⊢ A + ⟨“ B ”⟩ = A + 1
13 10 12 eqtrdi ⊢ A ∈ Word W ∧ B ∈ W → A ++ ⟨“ B ”⟩ = A + 1
14 13 oveq1d ⊢ A ∈ Word W ∧ B ∈ W → A ++ ⟨“ B ”⟩ − 1 = A + 1 - 1
15 lencl ⊢ A ∈ Word W → A ∈ ℕ 0
16 15 nn0cnd ⊢ A ∈ Word W → A ∈ ℂ
17 ax-1cn ⊢ 1 ∈ ℂ
18 pncan ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → A + 1 - 1 = A
19 16 17 18 sylancl ⊢ A ∈ Word W → A + 1 - 1 = A
20 16 addid2d ⊢ A ∈ Word W → 0 + A = A
21 19 20 eqtr4d ⊢ A ∈ Word W → A + 1 - 1 = 0 + A
22 21 adantr ⊢ A ∈ Word W ∧ B ∈ W → A + 1 - 1 = 0 + A
23 14 22 eqtrd ⊢ A ∈ Word W ∧ B ∈ W → A ++ ⟨“ B ”⟩ − 1 = 0 + A
24 23 fveq2d ⊢ A ∈ Word W ∧ B ∈ W → A ++ ⟨“ B ”⟩ ⁡ A ++ ⟨“ B ”⟩ − 1 = A ++ ⟨“ B ”⟩ ⁡ 0 + A
25 simpl ⊢ A ∈ Word W ∧ B ∈ W → A ∈ Word W
26 8 adantl ⊢ A ∈ Word W ∧ B ∈ W → ⟨“ B ”⟩ ∈ Word W
27 1nn ⊢ 1 ∈ ℕ
28 11 27 eqeltri ⊢ ⟨“ B ”⟩ ∈ ℕ
29 lbfzo0 ⊢ 0 ∈ 0 ..^ ⟨“ B ”⟩ ↔ ⟨“ B ”⟩ ∈ ℕ
30 28 29 mpbir ⊢ 0 ∈ 0 ..^ ⟨“ B ”⟩
31 30 a1i ⊢ A ∈ Word W ∧ B ∈ W → 0 ∈ 0 ..^ ⟨“ B ”⟩
32 ccatval3 ⊢ A ∈ Word W ∧ ⟨“ B ”⟩ ∈ Word W ∧ 0 ∈ 0 ..^ ⟨“ B ”⟩ → A ++ ⟨“ B ”⟩ ⁡ 0 + A = ⟨“ B ”⟩ ⁡ 0
33 25 26 31 32 syl3anc ⊢ A ∈ Word W ∧ B ∈ W → A ++ ⟨“ B ”⟩ ⁡ 0 + A = ⟨“ B ”⟩ ⁡ 0
34 s1fv ⊢ B ∈ W → ⟨“ B ”⟩ ⁡ 0 = B
35 34 adantl ⊢ A ∈ Word W ∧ B ∈ W → ⟨“ B ”⟩ ⁡ 0 = B
36 24 33 35 3eqtrd ⊢ A ∈ Word W ∧ B ∈ W → A ++ ⟨“ B ”⟩ ⁡ A ++ ⟨“ B ”⟩ − 1 = B
37 7 36 sylan9eqr ⊢ A ∈ Word W ∧ B ∈ W ∧ A ++ ⟨“ B ”⟩ ∈ dom ⁡ S → S ⁡ A ++ ⟨“ B ”⟩ = B
38 37 3impa ⊢ A ∈ Word W ∧ B ∈ W ∧ A ++ ⟨“ B ”⟩ ∈ dom ⁡ S → S ⁡ A ++ ⟨“ B ”⟩ = B