This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid 
 |-  ( 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 )