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⁡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 efgsval2 ⊢A∈WordW∧B∈W∧A++⟨“B”⟩∈dom⁡S→S⁡A++⟨“B”⟩=B

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