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 ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
psgninv.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
psgninv.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
Assertion psgninv ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝑁 ‘ ◡ 𝐹 ) = ( 𝑁 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 psgninv.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 psgninv.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
3 psgninv.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
4 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
5 1 2 4 psgnghm2 ⊢ ( 𝐷 ∈ Fin → 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
6 eqid ⊢ ( invg ‘ 𝑆 ) = ( invg ‘ 𝑆 )
7 eqid ⊢ ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) = ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
8 3 6 7 ghminv ⊢ ( ( 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ∧ 𝐹 ∈ 𝑃 ) → ( 𝑁 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝐹 ) ) = ( ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ‘ ( 𝑁 ‘ 𝐹 ) ) )
9 5 8 sylan ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝑁 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝐹 ) ) = ( ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ‘ ( 𝑁 ‘ 𝐹 ) ) )
10 1 3 6 symginv ⊢ ( 𝐹 ∈ 𝑃 → ( ( invg ‘ 𝑆 ) ‘ 𝐹 ) = ◡ 𝐹 )
11 10 adantl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( invg ‘ 𝑆 ) ‘ 𝐹 ) = ◡ 𝐹 )
12 11 fveq2d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝑁 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝐹 ) ) = ( 𝑁 ‘ ◡ 𝐹 ) )
13 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
14 13 cnmsgnsubg ⊢ { 1 , - 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
15 4 cnmsgnbas ⊢ { 1 , - 1 } = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
16 3 15 ghmf ⊢ ( 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → 𝑁 : 𝑃 ⟶ { 1 , - 1 } )
17 5 16 syl ⊢ ( 𝐷 ∈ Fin → 𝑁 : 𝑃 ⟶ { 1 , - 1 } )
18 17 ffvelrnda ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝑁 ‘ 𝐹 ) ∈ { 1 , - 1 } )
19 cnex ⊢ ℂ ∈ V
20 19 difexi ⊢ ( ℂ ∖ { 0 } ) ∈ V
21 ax-1cn ⊢ 1 ∈ ℂ
22 ax-1ne0 ⊢ 1 ≠ 0
23 eldifsn ⊢ ( 1 ∈ ( ℂ ∖ { 0 } ) ↔ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) )
24 21 22 23 mpbir2an ⊢ 1 ∈ ( ℂ ∖ { 0 } )
25 neg1cn ⊢ - 1 ∈ ℂ
26 neg1ne0 ⊢ - 1 ≠ 0
27 eldifsn ⊢ ( - 1 ∈ ( ℂ ∖ { 0 } ) ↔ ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) )
28 25 26 27 mpbir2an ⊢ - 1 ∈ ( ℂ ∖ { 0 } )
29 prssi ⊢ ( ( 1 ∈ ( ℂ ∖ { 0 } ) ∧ - 1 ∈ ( ℂ ∖ { 0 } ) ) → { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } ) )
30 24 28 29 mp2an ⊢ { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } )
31 ressabs ⊢ ( ( ( ℂ ∖ { 0 } ) ∈ V ∧ { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } ) ) → ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
32 20 30 31 mp2an ⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
33 32 eqcomi ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s { 1 , - 1 } )
34 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
35 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
36 cndrng ⊢ ℂfld ∈ DivRing
37 34 35 36 drngui ⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
38 eqid ⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
39 37 13 38 invrfval ⊢ ( invr ‘ ℂfld ) = ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
40 33 39 7 subginv ⊢ ( ( { 1 , - 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ { 1 , - 1 } ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑁 ‘ 𝐹 ) ) = ( ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ‘ ( 𝑁 ‘ 𝐹 ) ) )
41 14 18 40 sylancr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑁 ‘ 𝐹 ) ) = ( ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ‘ ( 𝑁 ‘ 𝐹 ) ) )
42 30 18 sseldi ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝑁 ‘ 𝐹 ) ∈ ( ℂ ∖ { 0 } ) )
43 eldifsn ⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑁 ‘ 𝐹 ) ∈ ℂ ∧ ( 𝑁 ‘ 𝐹 ) ≠ 0 ) )
44 42 43 sylib ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( 𝑁 ‘ 𝐹 ) ∈ ℂ ∧ ( 𝑁 ‘ 𝐹 ) ≠ 0 ) )
45 cnfldinv ⊢ ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℂ ∧ ( 𝑁 ‘ 𝐹 ) ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑁 ‘ 𝐹 ) ) = ( 1 / ( 𝑁 ‘ 𝐹 ) ) )
46 44 45 syl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑁 ‘ 𝐹 ) ) = ( 1 / ( 𝑁 ‘ 𝐹 ) ) )
47 41 46 eqtr3d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ‘ ( 𝑁 ‘ 𝐹 ) ) = ( 1 / ( 𝑁 ‘ 𝐹 ) ) )
48 9 12 47 3eqtr3d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝑁 ‘ ◡ 𝐹 ) = ( 1 / ( 𝑁 ‘ 𝐹 ) ) )
49 fvex ⊢ ( 𝑁 ‘ 𝐹 ) ∈ V
50 49 elpr ⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ { 1 , - 1 } ↔ ( ( 𝑁 ‘ 𝐹 ) = 1 ∨ ( 𝑁 ‘ 𝐹 ) = - 1 ) )
51 1div1e1 ⊢ ( 1 / 1 ) = 1
52 oveq2 ⊢ ( ( 𝑁 ‘ 𝐹 ) = 1 → ( 1 / ( 𝑁 ‘ 𝐹 ) ) = ( 1 / 1 ) )
53 id ⊢ ( ( 𝑁 ‘ 𝐹 ) = 1 → ( 𝑁 ‘ 𝐹 ) = 1 )
54 51 52 53 3eqtr4a ⊢ ( ( 𝑁 ‘ 𝐹 ) = 1 → ( 1 / ( 𝑁 ‘ 𝐹 ) ) = ( 𝑁 ‘ 𝐹 ) )
55 divneg2 ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 1 / 1 ) = ( 1 / - 1 ) )
56 21 21 22 55 mp3an ⊢ - ( 1 / 1 ) = ( 1 / - 1 )
57 51 negeqi ⊢ - ( 1 / 1 ) = - 1
58 56 57 eqtr3i ⊢ ( 1 / - 1 ) = - 1
59 oveq2 ⊢ ( ( 𝑁 ‘ 𝐹 ) = - 1 → ( 1 / ( 𝑁 ‘ 𝐹 ) ) = ( 1 / - 1 ) )
60 id ⊢ ( ( 𝑁 ‘ 𝐹 ) = - 1 → ( 𝑁 ‘ 𝐹 ) = - 1 )
61 58 59 60 3eqtr4a ⊢ ( ( 𝑁 ‘ 𝐹 ) = - 1 → ( 1 / ( 𝑁 ‘ 𝐹 ) ) = ( 𝑁 ‘ 𝐹 ) )
62 54 61 jaoi ⊢ ( ( ( 𝑁 ‘ 𝐹 ) = 1 ∨ ( 𝑁 ‘ 𝐹 ) = - 1 ) → ( 1 / ( 𝑁 ‘ 𝐹 ) ) = ( 𝑁 ‘ 𝐹 ) )
63 50 62 sylbi ⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ { 1 , - 1 } → ( 1 / ( 𝑁 ‘ 𝐹 ) ) = ( 𝑁 ‘ 𝐹 ) )
64 18 63 syl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 1 / ( 𝑁 ‘ 𝐹 ) ) = ( 𝑁 ‘ 𝐹 ) )
65 48 64 eqtrd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝑁 ‘ ◡ 𝐹 ) = ( 𝑁 ‘ 𝐹 ) )