Metamath Proof Explorer

Theorem psgninv

Description: The sign of a permutation equals the sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses psgninv.s 
|- S = ( SymGrp ` D )
psgninv.n 
|- N = ( pmSgn ` D )
psgninv.p 
|- P = ( Base ` S )
Assertion psgninv 
|- ( ( D e. Fin /\ F e. P ) -> ( N ` `' F ) = ( N ` F ) )

Proof

Step Hyp Ref Expression
1 psgninv.s 
 |-  S = ( SymGrp ` D )
2 psgninv.n 
 |-  N = ( pmSgn ` D )
3 psgninv.p 
 |-  P = ( Base ` S )
4 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
5 1 2 4 psgnghm2 
 |-  ( D e. Fin -> N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
6 eqid 
 |-  ( invg ` S ) = ( invg ` S )
7 eqid 
 |-  ( invg ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) = ( invg ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
8 3 6 7 ghminv 
 |-  ( ( N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ F e. P ) -> ( N ` ( ( invg ` S ) ` F ) ) = ( ( invg ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ` ( N ` F ) ) )
9 5 8 sylan 
 |-  ( ( D e. Fin /\ F e. P ) -> ( N ` ( ( invg ` S ) ` F ) ) = ( ( invg ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ` ( N ` F ) ) )
10 1 3 6 symginv 
 |-  ( F e. P -> ( ( invg ` S ) ` F ) = `' F )
11 10 adantl 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( invg ` S ) ` F ) = `' F )
12 11 fveq2d 
 |-  ( ( D e. Fin /\ F e. P ) -> ( N ` ( ( invg ` S ) ` F ) ) = ( N ` `' F ) )
13 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
14 13 cnmsgnsubg 
 |-  { 1 , -u 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
15 4 cnmsgnbas 
 |-  { 1 , -u 1 } = ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
16 3 15 ghmf 
 |-  ( N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> N : P --> { 1 , -u 1 } )
17 5 16 syl 
 |-  ( D e. Fin -> N : P --> { 1 , -u 1 } )
18 17 ffvelrnda 
 |-  ( ( D e. Fin /\ F e. P ) -> ( N ` F ) e. { 1 , -u 1 } )
19 cnex 
 |-  CC e. _V
20 19 difexi 
 |-  ( CC \ { 0 } ) e. _V
21 ax-1cn 
 |-  1 e. CC
22 ax-1ne0 
 |-  1 =/= 0
23 eldifsn 
 |-  ( 1 e. ( CC \ { 0 } ) <-> ( 1 e. CC /\ 1 =/= 0 ) )
24 21 22 23 mpbir2an 
 |-  1 e. ( CC \ { 0 } )
25 neg1cn 
 |-  -u 1 e. CC
26 neg1ne0 
 |-  -u 1 =/= 0
27 eldifsn 
 |-  ( -u 1 e. ( CC \ { 0 } ) <-> ( -u 1 e. CC /\ -u 1 =/= 0 ) )
28 25 26 27 mpbir2an 
 |-  -u 1 e. ( CC \ { 0 } )
29 prssi 
 |-  ( ( 1 e. ( CC \ { 0 } ) /\ -u 1 e. ( CC \ { 0 } ) ) -> { 1 , -u 1 } C_ ( CC \ { 0 } ) )
30 24 28 29 mp2an 
 |-  { 1 , -u 1 } C_ ( CC \ { 0 } )
31 ressabs 
 |-  ( ( ( CC \ { 0 } ) e. _V /\ { 1 , -u 1 } C_ ( CC \ { 0 } ) ) -> ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
32 20 30 31 mp2an 
 |-  ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
33 32 eqcomi 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s { 1 , -u 1 } )
34 cnfldbas 
 |-  CC = ( Base ` CCfld )
35 cnfld0 
 |-  0 = ( 0g ` CCfld )
36 cndrng 
 |-  CCfld e. DivRing
37 34 35 36 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
38 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
39 37 13 38 invrfval 
 |-  ( invr ` CCfld ) = ( invg ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
40 33 39 7 subginv 
 |-  ( ( { 1 , -u 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) /\ ( N ` F ) e. { 1 , -u 1 } ) -> ( ( invr ` CCfld ) ` ( N ` F ) ) = ( ( invg ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ` ( N ` F ) ) )
41 14 18 40 sylancr 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( invr ` CCfld ) ` ( N ` F ) ) = ( ( invg ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ` ( N ` F ) ) )
42 30 18 sselid 
 |-  ( ( D e. Fin /\ F e. P ) -> ( N ` F ) e. ( CC \ { 0 } ) )
43 eldifsn 
 |-  ( ( N ` F ) e. ( CC \ { 0 } ) <-> ( ( N ` F ) e. CC /\ ( N ` F ) =/= 0 ) )
44 42 43 sylib 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( N ` F ) e. CC /\ ( N ` F ) =/= 0 ) )
45 cnfldinv 
 |-  ( ( ( N ` F ) e. CC /\ ( N ` F ) =/= 0 ) -> ( ( invr ` CCfld ) ` ( N ` F ) ) = ( 1 / ( N ` F ) ) )
46 44 45 syl 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( invr ` CCfld ) ` ( N ` F ) ) = ( 1 / ( N ` F ) ) )
47 41 46 eqtr3d 
 |-  ( ( D e. Fin /\ F e. P ) -> ( ( invg ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ` ( N ` F ) ) = ( 1 / ( N ` F ) ) )
48 9 12 47 3eqtr3d 
 |-  ( ( D e. Fin /\ F e. P ) -> ( N ` `' F ) = ( 1 / ( N ` F ) ) )
49 fvex 
 |-  ( N ` F ) e. _V
50 49 elpr 
 |-  ( ( N ` F ) e. { 1 , -u 1 } <-> ( ( N ` F ) = 1 \/ ( N ` F ) = -u 1 ) )
51 1div1e1 
 |-  ( 1 / 1 ) = 1
52 oveq2 
 |-  ( ( N ` F ) = 1 -> ( 1 / ( N ` F ) ) = ( 1 / 1 ) )
53 id 
 |-  ( ( N ` F ) = 1 -> ( N ` F ) = 1 )
54 51 52 53 3eqtr4a 
 |-  ( ( N ` F ) = 1 -> ( 1 / ( N ` F ) ) = ( N ` F ) )
55 divneg2 
 |-  ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
56 21 21 22 55 mp3an 
 |-  -u ( 1 / 1 ) = ( 1 / -u 1 )
57 51 negeqi 
 |-  -u ( 1 / 1 ) = -u 1
58 56 57 eqtr3i 
 |-  ( 1 / -u 1 ) = -u 1
59 oveq2 
 |-  ( ( N ` F ) = -u 1 -> ( 1 / ( N ` F ) ) = ( 1 / -u 1 ) )
60 id 
 |-  ( ( N ` F ) = -u 1 -> ( N ` F ) = -u 1 )
61 58 59 60 3eqtr4a 
 |-  ( ( N ` F ) = -u 1 -> ( 1 / ( N ` F ) ) = ( N ` F ) )
62 54 61 jaoi 
 |-  ( ( ( N ` F ) = 1 \/ ( N ` F ) = -u 1 ) -> ( 1 / ( N ` F ) ) = ( N ` F ) )
63 50 62 sylbi 
 |-  ( ( N ` F ) e. { 1 , -u 1 } -> ( 1 / ( N ` F ) ) = ( N ` F ) )
64 18 63 syl 
 |-  ( ( D e. Fin /\ F e. P ) -> ( 1 / ( N ` F ) ) = ( N ` F ) )
65 48 64 eqtrd 
 |-  ( ( D e. Fin /\ F e. P ) -> ( N ` `' F ) = ( N ` F ) )