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 = ( SymGrp ` D )
psgnsn.b
|- B = ( Base ` G )
psgnsn.n
|- N = ( pmSgn ` D )
Assertion psgnsn
|- ( ( A e. V /\ X e. B ) -> ( N ` X ) = 1 )

Proof

Step Hyp Ref Expression
1 psgnsn.0
 |-  D = { A }
2 psgnsn.g
 |-  G = ( SymGrp ` D )
3 psgnsn.b
 |-  B = ( Base ` G )
4 psgnsn.n
 |-  N = ( pmSgn ` D )
5 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
6 5 gsum0
 |-  ( G gsum (/) ) = ( 0g ` G )
7 2 3 1 symg1bas
 |-  ( A e. V -> B = { { <. A , A >. } } )
8 7 eleq2d
 |-  ( A e. V -> ( X e. B <-> X e. { { <. A , A >. } } ) )
9 8 biimpa
 |-  ( ( A e. V /\ X e. B ) -> X e. { { <. A , A >. } } )
10 elsni
 |-  ( X e. { { <. A , A >. } } -> X = { <. A , A >. } )
11 1 reseq2i
 |-  ( _I |` D ) = ( _I |` { A } )
12 snex
 |-  { A } e. _V
13 12 snid
 |-  { A } e. { { A } }
14 1 13 eqeltri
 |-  D e. { { A } }
15 2 symgid
 |-  ( D e. { { A } } -> ( _I |` D ) = ( 0g ` G ) )
16 14 15 mp1i
 |-  ( A e. V -> ( _I |` D ) = ( 0g ` G ) )
17 restidsing
 |-  ( _I |` { A } ) = ( { A } X. { A } )
18 xpsng
 |-  ( ( A e. V /\ A e. V ) -> ( { A } X. { A } ) = { <. A , A >. } )
19 18 anidms
 |-  ( A e. V -> ( { A } X. { A } ) = { <. A , A >. } )
20 17 19 syl5eq
 |-  ( A e. V -> ( _I |` { A } ) = { <. A , A >. } )
21 11 16 20 3eqtr3a
 |-  ( A e. V -> ( 0g ` G ) = { <. A , A >. } )
22 21 adantr
 |-  ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = { <. A , A >. } )
23 id
 |-  ( { <. A , A >. } = X -> { <. A , A >. } = X )
24 23 eqcoms
 |-  ( X = { <. A , A >. } -> { <. A , A >. } = X )
25 22 24 sylan9eqr
 |-  ( ( X = { <. A , A >. } /\ ( A e. V /\ X e. B ) ) -> ( 0g ` G ) = X )
26 25 ex
 |-  ( X = { <. A , A >. } -> ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X ) )
27 10 26 syl
 |-  ( X e. { { <. A , A >. } } -> ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X ) )
28 9 27 mpcom
 |-  ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X )
29 6 28 eqtr2id
 |-  ( ( A e. V /\ X e. B ) -> X = ( G gsum (/) ) )
30 29 fveq2d
 |-  ( ( A e. V /\ X e. B ) -> ( N ` X ) = ( N ` ( G gsum (/) ) ) )
31 1 12 eqeltri
 |-  D e. _V
32 wrd0
 |-  (/) e. Word (/)
33 31 32 pm3.2i
 |-  ( D e. _V /\ (/) e. Word (/) )
34 1 fveq2i
 |-  ( pmTrsp ` D ) = ( pmTrsp ` { A } )
35 pmtrsn
 |-  ( pmTrsp ` { A } ) = (/)
36 34 35 eqtri
 |-  ( pmTrsp ` D ) = (/)
37 36 rneqi
 |-  ran ( pmTrsp ` D ) = ran (/)
38 rn0
 |-  ran (/) = (/)
39 37 38 eqtr2i
 |-  (/) = ran ( pmTrsp ` D )
40 2 39 4 psgnvalii
 |-  ( ( D e. _V /\ (/) e. Word (/) ) -> ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) )
41 33 40 mp1i
 |-  ( ( A e. V /\ X e. B ) -> ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) )
42 hash0
 |-  ( # ` (/) ) = 0
43 42 oveq2i
 |-  ( -u 1 ^ ( # ` (/) ) ) = ( -u 1 ^ 0 )
44 neg1cn
 |-  -u 1 e. CC
45 exp0
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
46 44 45 ax-mp
 |-  ( -u 1 ^ 0 ) = 1
47 43 46 eqtri
 |-  ( -u 1 ^ ( # ` (/) ) ) = 1
48 47 a1i
 |-  ( ( A e. V /\ X e. B ) -> ( -u 1 ^ ( # ` (/) ) ) = 1 )
49 30 41 48 3eqtrd
 |-  ( ( A e. V /\ X e. B ) -> ( N ` X ) = 1 )