Metamath Proof Explorer


Theorem psgnsn

Description: The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019)

Ref Expression
Hypotheses psgnsn.0 D=A
psgnsn.g G=SymGrpD
psgnsn.b B=BaseG
psgnsn.n N=pmSgnD
Assertion psgnsn AVXBNX=1

Proof

Step Hyp Ref Expression
1 psgnsn.0 D=A
2 psgnsn.g G=SymGrpD
3 psgnsn.b B=BaseG
4 psgnsn.n N=pmSgnD
5 eqid 0G=0G
6 5 gsum0 G=0G
7 2 3 1 symg1bas AVB=AA
8 7 eleq2d AVXBXAA
9 8 biimpa AVXBXAA
10 elsni XAAX=AA
11 1 reseq2i ID=IA
12 snex AV
13 12 snid AA
14 1 13 eqeltri DA
15 2 symgid DAID=0G
16 14 15 mp1i AVID=0G
17 restidsing IA=A×A
18 xpsng AVAVA×A=AA
19 18 anidms AVA×A=AA
20 17 19 eqtrid AVIA=AA
21 11 16 20 3eqtr3a AV0G=AA
22 21 adantr AVXB0G=AA
23 id AA=XAA=X
24 23 eqcoms X=AAAA=X
25 22 24 sylan9eqr X=AAAVXB0G=X
26 25 ex X=AAAVXB0G=X
27 10 26 syl XAAAVXB0G=X
28 9 27 mpcom AVXB0G=X
29 6 28 eqtr2id AVXBX=G
30 29 fveq2d AVXBNX=NG
31 1 12 eqeltri DV
32 wrd0 Word
33 31 32 pm3.2i DVWord
34 1 fveq2i pmTrspD=pmTrspA
35 pmtrsn pmTrspA=
36 34 35 eqtri pmTrspD=
37 36 rneqi ranpmTrspD=ran
38 rn0 ran=
39 37 38 eqtr2i =ranpmTrspD
40 2 39 4 psgnvalii DVWordNG=1
41 33 40 mp1i AVXBNG=1
42 hash0 =0
43 42 oveq2i 1=10
44 neg1cn 1
45 exp0 110=1
46 44 45 ax-mp 10=1
47 43 46 eqtri 1=1
48 47 a1i AVXB1=1
49 30 41 48 3eqtrd AVXBNX=1