Theorem psgnsn

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

	Ref	Expression
Hypotheses	psgnsn.0	|- D = { A }
	psgnsn.g	|- G = ( SymGrp ` D )
	psgnsn.b	|- B = ( Base ` G )
	psgnsn.n	|- N = ( pmSgn ` D )
Assertion	psgnsn	|- ( ( A e. V /\ X e. B ) -> ( N ` X ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		psgnsn.0	|- D = { A }
2		psgnsn.g	|- G = ( SymGrp ` D )
3		psgnsn.b	|- B = ( Base ` G )
4		psgnsn.n	|- N = ( pmSgn ` D )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6	5	gsum0	|- ( G gsum (/) ) = ( 0g ` G )
7	2 3 1	symg1bas	|- ( A e. V -> B = { { <. A , A >. } } )
8	7	eleq2d	|- ( A e. V -> ( X e. B <-> X e. { { <. A , A >. } } ) )
9	8	biimpa	|- ( ( A e. V /\ X e. B ) -> X e. { { <. A , A >. } } )
10		elsni	|- ( X e. { { <. A , A >. } } -> X = { <. A , A >. } )
11	1	reseq2i	|- ( _I |` D ) = ( _I |` { A } )
12		snex	|- { A } e. _V
13	12	snid	|- { A } e. { { A } }
14	1 13	eqeltri	|- D e. { { A } }
15	2	symgid	|- ( D e. { { A } } -> ( _I |` D ) = ( 0g ` G ) )
16	14 15	mp1i	|- ( A e. V -> ( _I |` D ) = ( 0g ` G ) )
17		restidsing	|- ( _I |` { A } ) = ( { A } X. { A } )
18		xpsng	|- ( ( A e. V /\ A e. V ) -> ( { A } X. { A } ) = { <. A , A >. } )
19	18	anidms	|- ( A e. V -> ( { A } X. { A } ) = { <. A , A >. } )
20	17 19	syl5eq	|- ( A e. V -> ( _I |` { A } ) = { <. A , A >. } )
21	11 16 20	3eqtr3a	|- ( A e. V -> ( 0g ` G ) = { <. A , A >. } )
22	21	adantr	|- ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = { <. A , A >. } )
23		id	|- ( { <. A , A >. } = X -> { <. A , A >. } = X )
24	23	eqcoms	|- ( X = { <. A , A >. } -> { <. A , A >. } = X )
25	22 24	sylan9eqr	|- ( ( X = { <. A , A >. } /\ ( A e. V /\ X e. B ) ) -> ( 0g ` G ) = X )
26	25	ex	|- ( X = { <. A , A >. } -> ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X ) )
27	10 26	syl	|- ( X e. { { <. A , A >. } } -> ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X ) )
28	9 27	mpcom	|- ( ( A e. V /\ X e. B ) -> ( 0g ` G ) = X )
29	6 28	syl5req	|- ( ( A e. V /\ X e. B ) -> X = ( G gsum (/) ) )
30	29	fveq2d	|- ( ( A e. V /\ X e. B ) -> ( N ` X ) = ( N ` ( G gsum (/) ) ) )
31	1 12	eqeltri	|- D e. _V
32		wrd0	|- (/) e. Word (/)
33	31 32	pm3.2i	|- ( D e. _V /\ (/) e. Word (/) )
34	1	fveq2i	|- ( pmTrsp ` D ) = ( pmTrsp ` { A } )
35		pmtrsn	|- ( pmTrsp ` { A } ) = (/)
36	34 35	eqtri	|- ( pmTrsp ` D ) = (/)
37	36	rneqi	|- ran ( pmTrsp ` D ) = ran (/)
38		rn0	|- ran (/) = (/)
39	37 38	eqtr2i	|- (/) = ran ( pmTrsp ` D )
40	2 39 4	psgnvalii	|- ( ( D e. _V /\ (/) e. Word (/) ) -> ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) )
41	33 40	mp1i	|- ( ( A e. V /\ X e. B ) -> ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) )
42		hash0	|- ( # ` (/) ) = 0
43	42	oveq2i	|- ( -u 1 ^ ( # ` (/) ) ) = ( -u 1 ^ 0 )
44		neg1cn	|- -u 1 e. CC
45		exp0	|- ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
46	44 45	ax-mp	|- ( -u 1 ^ 0 ) = 1
47	43 46	eqtri	|- ( -u 1 ^ ( # ` (/) ) ) = 1
48	47	a1i	|- ( ( A e. V /\ X e. B ) -> ( -u 1 ^ ( # ` (/) ) ) = 1 )
49	30 41 48	3eqtrd	|- ( ( A e. V /\ X e. B ) -> ( N ` X ) = 1 )