Metamath Proof Explorer

Theorem psgn0fv0

Description: The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019)

Ref Expression
Assertion psgn0fv0 
|- ( ( pmSgn ` (/) ) ` (/) ) = 1

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 wrd0 
 |-  (/) e. Word ran ( pmTrsp ` (/) )
3 eqid 
 |-  ( 0g ` ( SymGrp ` (/) ) ) = ( 0g ` ( SymGrp ` (/) ) )
4 3 gsum0 
 |-  ( ( SymGrp ` (/) ) gsum (/) ) = ( 0g ` ( SymGrp ` (/) ) )
5 eqid 
 |-  ( SymGrp ` (/) ) = ( SymGrp ` (/) )
6 5 symgid 
 |-  ( (/) e. _V -> ( _I |` (/) ) = ( 0g ` ( SymGrp ` (/) ) ) )
7 1 6 ax-mp 
 |-  ( _I |` (/) ) = ( 0g ` ( SymGrp ` (/) ) )
8 res0 
 |-  ( _I |` (/) ) = (/)
9 7 8 eqtr3i 
 |-  ( 0g ` ( SymGrp ` (/) ) ) = (/)
10 9 a1i 
 |-  ( ( (/) e. _V /\ (/) e. Word ran ( pmTrsp ` (/) ) ) -> ( 0g ` ( SymGrp ` (/) ) ) = (/) )
11 4 10 syl5req 
 |-  ( ( (/) e. _V /\ (/) e. Word ran ( pmTrsp ` (/) ) ) -> (/) = ( ( SymGrp ` (/) ) gsum (/) ) )
12 11 fveq2d 
 |-  ( ( (/) e. _V /\ (/) e. Word ran ( pmTrsp ` (/) ) ) -> ( ( pmSgn ` (/) ) ` (/) ) = ( ( pmSgn ` (/) ) ` ( ( SymGrp ` (/) ) gsum (/) ) ) )
13 eqid 
 |-  ran ( pmTrsp ` (/) ) = ran ( pmTrsp ` (/) )
14 eqid 
 |-  ( pmSgn ` (/) ) = ( pmSgn ` (/) )
15 5 13 14 psgnvalii 
 |-  ( ( (/) e. _V /\ (/) e. Word ran ( pmTrsp ` (/) ) ) -> ( ( pmSgn ` (/) ) ` ( ( SymGrp ` (/) ) gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) )
16 hash0 
 |-  ( # ` (/) ) = 0
17 16 oveq2i 
 |-  ( -u 1 ^ ( # ` (/) ) ) = ( -u 1 ^ 0 )
18 neg1cn 
 |-  -u 1 e. CC
19 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
20 18 19 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
21 17 20 eqtri 
 |-  ( -u 1 ^ ( # ` (/) ) ) = 1
22 21 a1i 
 |-  ( ( (/) e. _V /\ (/) e. Word ran ( pmTrsp ` (/) ) ) -> ( -u 1 ^ ( # ` (/) ) ) = 1 )
23 12 15 22 3eqtrd 
 |-  ( ( (/) e. _V /\ (/) e. Word ran ( pmTrsp ` (/) ) ) -> ( ( pmSgn ` (/) ) ` (/) ) = 1 )
24 1 2 23 mp2an 
 |-  ( ( pmSgn ` (/) ) ` (/) ) = 1