Theorem psgnvalfi

Description: Value of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019)

	Ref	Expression
Hypotheses	psgnfvalfi.g	|- G = ( SymGrp ` D )
	psgnfvalfi.b	|- B = ( Base ` G )
	psgnfvalfi.t	|- T = ran ( pmTrsp ` D )
	psgnfvalfi.n	|- N = ( pmSgn ` D )
Assertion	psgnvalfi	|- ( ( D e. Fin /\ P e. B ) -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnfvalfi.g	|- G = ( SymGrp ` D )
2		psgnfvalfi.b	|- B = ( Base ` G )
3		psgnfvalfi.t	|- T = ran ( pmTrsp ` D )
4		psgnfvalfi.n	|- N = ( pmSgn ` D )
5		simpr	|- ( ( D e. Fin /\ P e. B ) -> P e. B )
6	1 2	sygbasnfpfi	|- ( ( D e. Fin /\ P e. B ) -> dom ( P \ _I ) e. Fin )
7	1 4 2	psgneldm	|- ( P e. dom N <-> ( P e. B /\ dom ( P \ _I ) e. Fin ) )
8	5 6 7	sylanbrc	|- ( ( D e. Fin /\ P e. B ) -> P e. dom N )
9	1 3 4	psgnval	|- ( P e. dom N -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
10	8 9	syl	|- ( ( D e. Fin /\ P e. B ) -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )