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 )