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

Metamath Proof Explorer

Theorem psgnsn

Description: The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019)

Ref Expression
Hypotheses psgnsn.0 ⊢ 𝐷 = { 𝐴 }
psgnsn.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnsn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
psgnsn.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgnsn ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) = 1 )

Proof

Step Hyp Ref Expression
1 psgnsn.0 ⊢ 𝐷 = { 𝐴 }
2 psgnsn.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
3 psgnsn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 psgnsn.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 5 gsum0 ⊢ ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 )
7 2 3 1 symg1bas ⊢ ( 𝐴 ∈ 𝑉 → 𝐵 = { { ⟨ 𝐴 , 𝐴 ⟩ } } )
8 7 eleq2d ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ { { ⟨ 𝐴 , 𝐴 ⟩ } } ) )
9 8 biimpa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ { { ⟨ 𝐴 , 𝐴 ⟩ } } )
10 elsni ⊢ ( 𝑋 ∈ { { ⟨ 𝐴 , 𝐴 ⟩ } } → 𝑋 = { ⟨ 𝐴 , 𝐴 ⟩ } )
11 1 reseq2i ⊢ ( I ↾ 𝐷 ) = ( I ↾ { 𝐴 } )
12 snex ⊢ { 𝐴 } ∈ V
13 12 snid ⊢ { 𝐴 } ∈ { { 𝐴 } }
14 1 13 eqeltri ⊢ 𝐷 ∈ { { 𝐴 } }
15 2 symgid ⊢ ( 𝐷 ∈ { { 𝐴 } } → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
16 14 15 mp1i ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
17 restidsing ⊢ ( I ↾ { 𝐴 } ) = ( { 𝐴 } × { 𝐴 } )
18 xpsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( { 𝐴 } × { 𝐴 } ) = { ⟨ 𝐴 , 𝐴 ⟩ } )
19 18 anidms ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } × { 𝐴 } ) = { ⟨ 𝐴 , 𝐴 ⟩ } )
20 17 19 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ { 𝐴 } ) = { ⟨ 𝐴 , 𝐴 ⟩ } )
21 11 16 20 3eqtr3a ⊢ ( 𝐴 ∈ 𝑉 → ( 0g ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐴 ⟩ } )
22 21 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐴 ⟩ } )
23 id ⊢ ( { ⟨ 𝐴 , 𝐴 ⟩ } = 𝑋 → { ⟨ 𝐴 , 𝐴 ⟩ } = 𝑋 )
24 23 eqcoms ⊢ ( 𝑋 = { ⟨ 𝐴 , 𝐴 ⟩ } → { ⟨ 𝐴 , 𝐴 ⟩ } = 𝑋 )
25 22 24 sylan9eqr ⊢ ( ( 𝑋 = { ⟨ 𝐴 , 𝐴 ⟩ } ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ) → ( 0g ‘ 𝐺 ) = 𝑋 )
26 25 ex ⊢ ( 𝑋 = { ⟨ 𝐴 , 𝐴 ⟩ } → ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ 𝐺 ) = 𝑋 ) )
27 10 26 syl ⊢ ( 𝑋 ∈ { { ⟨ 𝐴 , 𝐴 ⟩ } } → ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ 𝐺 ) = 𝑋 ) )
28 9 27 mpcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ 𝐺 ) = 𝑋 )
29 6 28 eqtr2id ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( 𝐺 Σg ∅ ) )
30 29 fveq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝑁 ‘ ( 𝐺 Σg ∅ ) ) )
31 1 12 eqeltri ⊢ 𝐷 ∈ V
32 wrd0 ⊢ ∅ ∈ Word ∅
33 31 32 pm3.2i ⊢ ( 𝐷 ∈ V ∧ ∅ ∈ Word ∅ )
34 1 fveq2i ⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ { 𝐴 } )
35 pmtrsn ⊢ ( pmTrsp ‘ { 𝐴 } ) = ∅
36 34 35 eqtri ⊢ ( pmTrsp ‘ 𝐷 ) = ∅
37 36 rneqi ⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ∅
38 rn0 ⊢ ran ∅ = ∅
39 37 38 eqtr2i ⊢ ∅ = ran ( pmTrsp ‘ 𝐷 )
40 2 39 4 psgnvalii ⊢ ( ( 𝐷 ∈ V ∧ ∅ ∈ Word ∅ ) → ( 𝑁 ‘ ( 𝐺 Σg ∅ ) ) = ( - 1 ↑ ( ♯ ‘ ∅ ) ) )
41 33 40 mp1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝐺 Σg ∅ ) ) = ( - 1 ↑ ( ♯ ‘ ∅ ) ) )
42 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
43 42 oveq2i ⊢ ( - 1 ↑ ( ♯ ‘ ∅ ) ) = ( - 1 ↑ 0 )
44 neg1cn ⊢ - 1 ∈ ℂ
45 exp0 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
46 44 45 ax-mp ⊢ ( - 1 ↑ 0 ) = 1
47 43 46 eqtri ⊢ ( - 1 ↑ ( ♯ ‘ ∅ ) ) = 1
48 47 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( - 1 ↑ ( ♯ ‘ ∅ ) ) = 1 )
49 30 41 48 3eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) = 1 )