Theorem psgnvali

Description: A finitary permutation has at least one representation for its parity. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypotheses	psgnval.g	|- G = ( SymGrp ` D )
	psgnval.t	|- T = ran ( pmTrsp ` D )
	psgnval.n	|- N = ( pmSgn ` D )
Assertion	psgnvali	|- ( P e. dom N -> E. w e. Word T ( P = ( G gsum w ) /\ ( N ` P ) = ( -u 1 ^ ( # ` w ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnval.g	|- G = ( SymGrp ` D )
2		psgnval.t	|- T = ran ( pmTrsp ` D )
3		psgnval.n	|- N = ( pmSgn ` D )
4	1 2 3	psgnval	|- ( P e. dom N -> ( N ` P ) = ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
5	1 2 3	psgneu	|- ( P e. dom N -> E! s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
6		iotacl	|- ( E! s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) -> ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) e. { s | E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) } )
7	5 6	syl	|- ( P e. dom N -> ( iota s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) e. { s | E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) } )
8	4 7	eqeltrd	|- ( P e. dom N -> ( N ` P ) e. { s | E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) } )
9		fvex	|- ( N ` P ) e. _V
10		eqeq1	|- ( s = ( N ` P ) -> ( s = ( -u 1 ^ ( # ` w ) ) <-> ( N ` P ) = ( -u 1 ^ ( # ` w ) ) ) )
11	10	anbi2d	|- ( s = ( N ` P ) -> ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> ( P = ( G gsum w ) /\ ( N ` P ) = ( -u 1 ^ ( # ` w ) ) ) ) )
12	11	rexbidv	|- ( s = ( N ` P ) -> ( E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. w e. Word T ( P = ( G gsum w ) /\ ( N ` P ) = ( -u 1 ^ ( # ` w ) ) ) ) )
13	9 12	elab	|- ( ( N ` P ) e. { s | E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) } <-> E. w e. Word T ( P = ( G gsum w ) /\ ( N ` P ) = ( -u 1 ^ ( # ` w ) ) ) )
14	8 13	sylib	|- ( P e. dom N -> E. w e. Word T ( P = ( G gsum w ) /\ ( N ` P ) = ( -u 1 ^ ( # ` w ) ) ) )