Theorem psgnfvalfi

Description: Function definition 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	psgnfvalfi	|- ( D e. Fin -> N = ( x e. B |-> ( iota s E. w e. Word T ( x = ( 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		eqid	|- { p e. B | dom ( p \ _I ) e. Fin } = { p e. B | dom ( p \ _I ) e. Fin }
6	1 2 5 3 4	psgnfval	|- N = ( x e. { p e. B | dom ( p \ _I ) e. Fin } |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
7	1 2	sygbasnfpfi	|- ( ( D e. Fin /\ p e. B ) -> dom ( p \ _I ) e. Fin )
8	7	ralrimiva	|- ( D e. Fin -> A. p e. B dom ( p \ _I ) e. Fin )
9		rabid2	|- ( B = { p e. B | dom ( p \ _I ) e. Fin } <-> A. p e. B dom ( p \ _I ) e. Fin )
10	8 9	sylibr	|- ( D e. Fin -> B = { p e. B | dom ( p \ _I ) e. Fin } )
11	10	eqcomd	|- ( D e. Fin -> { p e. B | dom ( p \ _I ) e. Fin } = B )
12	11	mpteq1d	|- ( D e. Fin -> ( x e. { p e. B | dom ( p \ _I ) e. Fin } |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) = ( x e. B |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )
13	6 12	syl5eq	|- ( D e. Fin -> N = ( x e. B |-> ( iota s E. w e. Word T ( x = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) )