Step | Hyp | Ref
| Expression |
1 | | s1len 14556 |
. . . . . 6
β’
(β―ββ¨βπΎββ©) = 1 |
2 | 1 | oveq2i 7420 |
. . . . 5
β’
(0..^(β―ββ¨βπΎββ©)) = (0..^1) |
3 | | fzo01 13714 |
. . . . 5
β’ (0..^1) =
{0} |
4 | 2, 3 | eqtri 2761 |
. . . 4
β’
(0..^(β―ββ¨βπΎββ©)) = {0} |
5 | 4 | a1i 11 |
. . 3
β’ (πΎ β β β
(0..^(β―ββ¨βπΎββ©)) = {0}) |
6 | | simpr 486 |
. . . . . 6
β’ ((πΎ β β β§ π β
(0..^(β―ββ¨βπΎββ©))) β π β
(0..^(β―ββ¨βπΎββ©))) |
7 | 6, 4 | eleqtrdi 2844 |
. . . . 5
β’ ((πΎ β β β§ π β
(0..^(β―ββ¨βπΎββ©))) β π β {0}) |
8 | | velsn 4645 |
. . . . 5
β’ (π β {0} β π = 0) |
9 | 7, 8 | sylib 217 |
. . . 4
β’ ((πΎ β β β§ π β
(0..^(β―ββ¨βπΎββ©))) β π = 0) |
10 | | oveq2 7417 |
. . . . . . . . 9
β’ (π = 0 β (0...π) = (0...0)) |
11 | | 0z 12569 |
. . . . . . . . . 10
β’ 0 β
β€ |
12 | | fzsn 13543 |
. . . . . . . . . 10
β’ (0 β
β€ β (0...0) = {0}) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
β’ (0...0) =
{0} |
14 | 10, 13 | eqtrdi 2789 |
. . . . . . . 8
β’ (π = 0 β (0...π) = {0}) |
15 | 14 | mpteq1d 5244 |
. . . . . . 7
β’ (π = 0 β (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ))) = (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ)))) |
16 | 15 | oveq2d 7425 |
. . . . . 6
β’ (π = 0 β (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))) = (π Ξ£g (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ))))) |
17 | 16 | adantl 483 |
. . . . 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 33568 |
. . . . . . . 8
β’ π β Mnd |
21 | 20 | a1i 11 |
. . . . . . 7
β’ (πΎ β β β π β Mnd) |
22 | | 0re 11216 |
. . . . . . . 8
β’ 0 β
β |
23 | 22 | a1i 11 |
. . . . . . 7
β’ (πΎ β β β 0 β
β) |
24 | | s1fv 14560 |
. . . . . . . . . 10
β’ (πΎ β β β
(β¨βπΎββ©β0) = πΎ) |
25 | | id 22 |
. . . . . . . . . 10
β’ (πΎ β β β πΎ β
β) |
26 | 24, 25 | eqeltrd 2834 |
. . . . . . . . 9
β’ (πΎ β β β
(β¨βπΎββ©β0) β
β) |
27 | 26 | rexrd 11264 |
. . . . . . . 8
β’ (πΎ β β β
(β¨βπΎββ©β0) β
β*) |
28 | | sgncl 33537 |
. . . . . . . 8
β’
((β¨βπΎββ©β0) β
β* β (sgnβ(β¨βπΎββ©β0)) β {-1, 0,
1}) |
29 | 27, 28 | syl 17 |
. . . . . . 7
β’ (πΎ β β β
(sgnβ(β¨βπΎββ©β0)) β {-1, 0,
1}) |
30 | 18, 19 | signswbase 33565 |
. . . . . . . 8
β’ {-1, 0,
1} = (Baseβπ) |
31 | | 2fveq3 6897 |
. . . . . . . 8
β’ (π = 0 β
(sgnβ(β¨βπΎββ©βπ)) = (sgnβ(β¨βπΎββ©β0))) |
32 | 30, 31 | gsumsn 19822 |
. . . . . . 7
β’ ((π β Mnd β§ 0 β
β β§ (sgnβ(β¨βπΎββ©β0)) β {-1, 0, 1})
β (π
Ξ£g (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ)))) = (sgnβ(β¨βπΎββ©β0))) |
33 | 21, 23, 29, 32 | syl3anc 1372 |
. . . . . 6
β’ (πΎ β β β (π Ξ£g
(π β {0} β¦
(sgnβ(β¨βπΎββ©βπ)))) = (sgnβ(β¨βπΎββ©β0))) |
34 | 33 | adantr 482 |
. . . . 5
β’ ((πΎ β β β§ π = 0) β (π Ξ£g (π β {0} β¦
(sgnβ(β¨βπΎββ©βπ)))) = (sgnβ(β¨βπΎββ©β0))) |
35 | 24 | fveq2d 6896 |
. . . . . 6
β’ (πΎ β β β
(sgnβ(β¨βπΎββ©β0)) = (sgnβπΎ)) |
36 | 35 | adantr 482 |
. . . . 5
β’ ((πΎ β β β§ π = 0) β
(sgnβ(β¨βπΎββ©β0)) = (sgnβπΎ)) |
37 | 17, 34, 36 | 3eqtrd 2777 |
. . . 4
β’ ((πΎ β β β§ π = 0) β (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))) = (sgnβπΎ)) |
38 | 9, 37 | syldan 592 |
. . 3
β’ ((πΎ β β β§ π β
(0..^(β―ββ¨βπΎββ©))) β (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))) = (sgnβπΎ)) |
39 | 5, 38 | mpteq12dva 5238 |
. 2
β’ (πΎ β β β (π β
(0..^(β―ββ¨βπΎββ©)) β¦ (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ))))) = (π β {0} β¦ (sgnβπΎ))) |
40 | | s1cl 14552 |
. . 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 33574 |
. . 3
β’
(β¨βπΎββ© β Word β β
(πββ¨βπΎββ©) = (π β
(0..^(β―ββ¨βπΎββ©)) β¦ (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))))) |
44 | 40, 43 | syl 17 |
. 2
β’ (πΎ β β β (πββ¨βπΎββ©) = (π β
(0..^(β―ββ¨βπΎββ©)) β¦ (π Ξ£g (π β (0...π) β¦ (sgnβ(β¨βπΎββ©βπ)))))) |
45 | | sgnclre 33538 |
. . . 4
β’ (πΎ β β β
(sgnβπΎ) β
β) |
46 | | s1val 14548 |
. . . 4
β’
((sgnβπΎ)
β β β β¨β(sgnβπΎ)ββ© = {β¨0, (sgnβπΎ)β©}) |
47 | 45, 46 | syl 17 |
. . 3
β’ (πΎ β β β
β¨β(sgnβπΎ)ββ© = {β¨0, (sgnβπΎ)β©}) |
48 | | fmptsn 7165 |
. . . 4
β’ ((0
β β β§ (sgnβπΎ) β β) β {β¨0,
(sgnβπΎ)β©} =
(π β {0} β¦
(sgnβπΎ))) |
49 | 22, 45, 48 | sylancr 588 |
. . 3
β’ (πΎ β β β {β¨0,
(sgnβπΎ)β©} =
(π β {0} β¦
(sgnβπΎ))) |
50 | 47, 49 | eqtrd 2773 |
. 2
β’ (πΎ β β β
β¨β(sgnβπΎ)ββ© = (π β {0} β¦ (sgnβπΎ))) |
51 | 39, 44, 50 | 3eqtr4d 2783 |
1
β’ (πΎ β β β (πββ¨βπΎββ©) =
β¨β(sgnβπΎ)ββ©) |