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

Metamath Proof Explorer

Theorem psgnprfval2

Description: The permutation sign of the transposition for a pair. (Contributed by AV, 10-Dec-2018)

Ref Expression
Hypotheses psgnprfval.0 ⊢ 𝐷 = { 1 , 2 }
psgnprfval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnprfval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
psgnprfval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnprfval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgnprfval2 ( 𝑁 ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) = - 1

Proof

Step Hyp Ref Expression
1 psgnprfval.0 ⊢ 𝐷 = { 1 , 2 }
2 psgnprfval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
3 psgnprfval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 psgnprfval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
5 psgnprfval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
6 prex ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V
7 6 snid ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
8 1 fveq2i ⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ { 1 , 2 } )
9 8 rneqi ⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ { 1 , 2 } )
10 pmtrprfvalrn ⊢ ran ( pmTrsp ‘ { 1 , 2 } ) = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
11 9 10 eqtri ⊢ ran ( pmTrsp ‘ 𝐷 ) = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
12 7 11 eleqtrri ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ran ( pmTrsp ‘ 𝐷 )
13 12 4 eleqtrri ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑇
14 2 4 5 psgnpmtr ⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑇 → ( 𝑁 ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) = - 1 )
15 13 14 ax-mp ⊢ ( 𝑁 ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) = - 1