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

Metamath Proof Explorer

Theorem psgnprfval1

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

Ref Expression
Hypotheses psgnprfval.0 ⊢ 𝐷 = { 1 , 2 }
psgnprfval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnprfval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
psgnprfval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnprfval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgnprfval1 ( 𝑁 ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) = 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 } ∈ V
7 1 6 eqeltri ⊢ 𝐷 ∈ V
8 2 symgid ⊢ ( 𝐷 ∈ V → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
9 7 8 ax-mp ⊢ ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 )
10 9 gsum0 ⊢ ( 𝐺 Σg ∅ ) = ( I ↾ 𝐷 )
11 reseq2 ⊢ ( 𝐷 = { 1 , 2 } → ( I ↾ 𝐷 ) = ( I ↾ { 1 , 2 } ) )
12 1ex ⊢ 1 ∈ V
13 2nn ⊢ 2 ∈ ℕ
14 residpr ⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → ( I ↾ { 1 , 2 } ) = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } )
15 12 13 14 mp2an ⊢ ( I ↾ { 1 , 2 } ) = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ }
16 11 15 eqtrdi ⊢ ( 𝐷 = { 1 , 2 } → ( I ↾ 𝐷 ) = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } )
17 1 16 ax-mp ⊢ ( I ↾ 𝐷 ) = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ }
18 10 17 eqtr2i ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = ( 𝐺 Σg ∅ )
19 18 fveq2i ⊢ ( 𝑁 ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) = ( 𝑁 ‘ ( 𝐺 Σg ∅ ) )
20 wrd0 ⊢ ∅ ∈ Word 𝑇
21 2 4 5 psgnvalii ⊢ ( ( 𝐷 ∈ V ∧ ∅ ∈ Word 𝑇 ) → ( 𝑁 ‘ ( 𝐺 Σg ∅ ) ) = ( - 1 ↑ ( ♯ ‘ ∅ ) ) )
22 7 20 21 mp2an ⊢ ( 𝑁 ‘ ( 𝐺 Σg ∅ ) ) = ( - 1 ↑ ( ♯ ‘ ∅ ) )
23 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
24 23 oveq2i ⊢ ( - 1 ↑ ( ♯ ‘ ∅ ) ) = ( - 1 ↑ 0 )
25 neg1cn ⊢ - 1 ∈ ℂ
26 exp0 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
27 25 26 ax-mp ⊢ ( - 1 ↑ 0 ) = 1
28 24 27 eqtri ⊢ ( - 1 ↑ ( ♯ ‘ ∅ ) ) = 1
29 19 22 28 3eqtri ⊢ ( 𝑁 ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) = 1