Step | Hyp | Ref
| Expression |
1 | | s1len 14558 |
. . . . . 6
β’
(β―ββ¨βπΎββ©) = 1 |
2 | 1 | oveq2i 7422 |
. . . . 5
β’
(0..^(β―ββ¨βπΎββ©)) = (0..^1) |
3 | | fzo01 13716 |
. . . . 5
β’ (0..^1) =
{0} |
4 | 2, 3 | eqtri 2760 |
. . . 4
β’
(0..^(β―ββ¨βπΎββ©)) = {0} |
5 | 4 | a1i 11 |
. . 3
β’ (πΎ β β β
(0..^(β―ββ¨βπΎββ©)) = {0}) |
6 | | simpr 485 |
. . . . . 6
β’ ((πΎ β β β§ π β
(0..^(β―ββ¨βπΎββ©))) β π β
(0..^(β―ββ¨βπΎββ©))) |
7 | 6, 4 | eleqtrdi 2843 |
. . . . 5
β’ ((πΎ β β β§ π β
(0..^(β―ββ¨βπΎββ©))) β π β {0}) |
8 | | velsn 4644 |
. . . . 5
β’ (π β {0} β π = 0) |
9 | 7, 8 | sylib 217 |
. . . 4
β’ ((πΎ β β β§ π β
(0..^(β―ββ¨βπΎββ©))) β π = 0) |
10 | | oveq2 7419 |
. . . . . . . . 9
β’ (π = 0 β (0...π) = (0...0)) |
11 | | 0z 12571 |
. . . . . . . . . 10
β’ 0 β
β€ |
12 | | fzsn 13545 |
. . . . . . . . . 10
β’ (0 β
β€ β (0...0) = {0}) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
β’ (0...0) =
{0} |
14 | 10, 13 | eqtrdi 2788 |
. . . . . . . 8
β’ (π = 0 β (0...π) = {0}) |
15 | 14 | mpteq1d 5243 |
. . . . . . 7
β’ (π = 0 β (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ))) = (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ)))) |
16 | 15 | oveq2d 7427 |
. . . . . 6
β’ (π = 0 β (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))) = (π Ξ£g (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ))))) |
17 | 16 | adantl 482 |
. . . . 5
β’ ((πΎ β β β§ π = 0) β (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))) = (π Ξ£g (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ))))) |
18 | | signsv.p |
. . . . . . . . 9
⒠⨣ =
(π β {-1, 0, 1}, π β {-1, 0, 1} β¦
if(π = 0, π, π)) |
19 | | signsv.w |
. . . . . . . . 9
β’ π = {β¨(Baseβndx), {-1,
0, 1}β©, β¨(+gβndx), ⨣
β©} |
20 | 18, 19 | signswmnd 33637 |
. . . . . . . 8
β’ π β Mnd |
21 | 20 | a1i 11 |
. . . . . . 7
β’ (πΎ β β β π β Mnd) |
22 | | 0re 11218 |
. . . . . . . 8
β’ 0 β
β |
23 | 22 | a1i 11 |
. . . . . . 7
β’ (πΎ β β β 0 β
β) |
24 | | s1fv 14562 |
. . . . . . . . . 10
β’ (πΎ β β β
(β¨βπΎββ©β0) = πΎ) |
25 | | id 22 |
. . . . . . . . . 10
β’ (πΎ β β β πΎ β
β) |
26 | 24, 25 | eqeltrd 2833 |
. . . . . . . . 9
β’ (πΎ β β β
(β¨βπΎββ©β0) β
β) |
27 | 26 | rexrd 11266 |
. . . . . . . 8
β’ (πΎ β β β
(β¨βπΎββ©β0) β
β*) |
28 | | sgncl 33606 |
. . . . . . . 8
β’
((β¨βπΎββ©β0) β
β* β (sgnβ(β¨βπΎββ©β0)) β {-1, 0,
1}) |
29 | 27, 28 | syl 17 |
. . . . . . 7
β’ (πΎ β β β
(sgnβ(β¨βπΎββ©β0)) β {-1, 0,
1}) |
30 | 18, 19 | signswbase 33634 |
. . . . . . . 8
β’ {-1, 0,
1} = (Baseβπ) |
31 | | 2fveq3 6896 |
. . . . . . . 8
β’ (π = 0 β
(sgnβ(β¨βπΎββ©βπ)) = (sgnβ(β¨βπΎββ©β0))) |
32 | 30, 31 | gsumsn 19824 |
. . . . . . 7
β’ ((π β Mnd β§ 0 β
β β§ (sgnβ(β¨βπΎββ©β0)) β {-1, 0, 1})
β (π
Ξ£g (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ)))) = (sgnβ(β¨βπΎββ©β0))) |
33 | 21, 23, 29, 32 | syl3anc 1371 |
. . . . . 6
β’ (πΎ β β β (π Ξ£g
(π β {0} β¦
(sgnβ(β¨βπΎββ©βπ)))) = (sgnβ(β¨βπΎββ©β0))) |
34 | 33 | adantr 481 |
. . . . 5
β’ ((πΎ β β β§ π = 0) β (π Ξ£g (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ)))) = (sgnβ(β¨βπΎββ©β0))) |
35 | 24 | fveq2d 6895 |
. . . . . 6
β’ (πΎ β β β
(sgnβ(β¨βπΎββ©β0)) = (sgnβπΎ)) |
36 | 35 | adantr 481 |
. . . . 5
β’ ((πΎ β β β§ π = 0) β
(sgnβ(β¨βπΎββ©β0)) = (sgnβπΎ)) |
37 | 17, 34, 36 | 3eqtrd 2776 |
. . . 4
β’ ((πΎ β β β§ π = 0) β (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))) = (sgnβπΎ)) |
38 | 9, 37 | syldan 591 |
. . 3
β’ ((πΎ β β β§ π β
(0..^(β―ββ¨βπΎββ©))) β (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))) = (sgnβπΎ)) |
39 | 5, 38 | mpteq12dva 5237 |
. 2
β’ (πΎ β β β (π β
(0..^(β―ββ¨βπΎββ©)) β¦ (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ))))) = (π β {0} β¦ (sgnβπΎ))) |
40 | | s1cl 14554 |
. . 3
β’ (πΎ β β β
β¨βπΎββ©
β Word β) |
41 | | signsv.t |
. . . 4
β’ π = (π β Word β β¦ (π β
(0..^(β―βπ))
β¦ (π
Ξ£g (π β (0...π) β¦ (sgnβ(πβπ)))))) |
42 | | signsv.v |
. . . 4
β’ π = (π β Word β β¦ Ξ£π β
(1..^(β―βπ))if(((πβπ)βπ) β ((πβπ)β(π β 1)), 1, 0)) |
43 | 18, 19, 41, 42 | signstfv 33643 |
. . 3
β’
(β¨βπΎββ© β Word β β
(πββ¨βπΎββ©) = (π β
(0..^(β―ββ¨βπΎββ©)) β¦ (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))))) |
44 | 40, 43 | syl 17 |
. 2
β’ (πΎ β β β (πββ¨βπΎββ©) = (π β
(0..^(β―ββ¨βπΎββ©)) β¦ (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))))) |
45 | | sgnclre 33607 |
. . . 4
β’ (πΎ β β β
(sgnβπΎ) β
β) |
46 | | s1val 14550 |
. . . 4
β’
((sgnβπΎ)
β β β β¨β(sgnβπΎ)ββ© = {β¨0, (sgnβπΎ)β©}) |
47 | 45, 46 | syl 17 |
. . 3
β’ (πΎ β β β
β¨β(sgnβπΎ)ββ© = {β¨0, (sgnβπΎ)β©}) |
48 | | fmptsn 7167 |
. . . 4
β’ ((0
β β β§ (sgnβπΎ) β β) β {β¨0,
(sgnβπΎ)β©} =
(π β {0} β¦
(sgnβπΎ))) |
49 | 22, 45, 48 | sylancr 587 |
. . 3
β’ (πΎ β β β {β¨0,
(sgnβπΎ)β©} =
(π β {0} β¦
(sgnβπΎ))) |
50 | 47, 49 | eqtrd 2772 |
. 2
β’ (πΎ β β β
β¨β(sgnβπΎ)ββ© = (π β {0} β¦ (sgnβπΎ))) |
51 | 39, 44, 50 | 3eqtr4d 2782 |
1
β’ (πΎ β β β (πββ¨βπΎββ©) =
β¨β(sgnβπΎ)ββ©) |