This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )