Theorem psgnfieu

Description: A permutation of a finite set has exactly one parity. (Contributed by AV, 13-Jan-2019)

	Ref	Expression
Hypotheses	psgnfitr.g	|- G = ( SymGrp ` N )
	psgnfitr.p	|- B = ( Base ` G )
	psgnfitr.t	|- T = ran ( pmTrsp ` N )
Assertion	psgnfieu	|- ( ( N e. Fin /\ Q e. B ) -> E! s E. w e. Word T ( Q = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )

Proof

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