Description: The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | psgnsn.0 | |
|
psgnsn.g | |
||
psgnsn.b | |
||
psgnsn.n | |
||
Assertion | psgnsn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psgnsn.0 | |
|
2 | psgnsn.g | |
|
3 | psgnsn.b | |
|
4 | psgnsn.n | |
|
5 | eqid | |
|
6 | 5 | gsum0 | |
7 | 2 3 1 | symg1bas | |
8 | 7 | eleq2d | |
9 | 8 | biimpa | |
10 | elsni | |
|
11 | 1 | reseq2i | |
12 | snex | |
|
13 | 12 | snid | |
14 | 1 13 | eqeltri | |
15 | 2 | symgid | |
16 | 14 15 | mp1i | |
17 | restidsing | |
|
18 | xpsng | |
|
19 | 18 | anidms | |
20 | 17 19 | eqtrid | |
21 | 11 16 20 | 3eqtr3a | |
22 | 21 | adantr | |
23 | id | |
|
24 | 23 | eqcoms | |
25 | 22 24 | sylan9eqr | |
26 | 25 | ex | |
27 | 10 26 | syl | |
28 | 9 27 | mpcom | |
29 | 6 28 | eqtr2id | |
30 | 29 | fveq2d | |
31 | 1 12 | eqeltri | |
32 | wrd0 | |
|
33 | 31 32 | pm3.2i | |
34 | 1 | fveq2i | |
35 | pmtrsn | |
|
36 | 34 35 | eqtri | |
37 | 36 | rneqi | |
38 | rn0 | |
|
39 | 37 38 | eqtr2i | |
40 | 2 39 4 | psgnvalii | |
41 | 33 40 | mp1i | |
42 | hash0 | |
|
43 | 42 | oveq2i | |
44 | neg1cn | |
|
45 | exp0 | |
|
46 | 44 45 | ax-mp | |
47 | 43 46 | eqtri | |
48 | 47 | a1i | |
49 | 30 41 48 | 3eqtrd | |