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 \in Fin \land P \in B) \to N (P) = (ι s \| \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$

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 \in Fin \land P \in B) \to P \in B$
6	1 2	sygbasnfpfi	$⊢ (D \in Fin \land P \in B) \to dom (P ∖ I) \in Fin$
7	1 4 2	psgneldm	$⊢ P \in dom N \leftrightarrow (P \in B \land dom (P ∖ I) \in Fin)$
8	5 6 7	sylanbrc	$⊢ (D \in Fin \land P \in B) \to P \in dom N$
9	1 3 4	psgnval	$⊢ P \in dom N \to N (P) = (ι s \| \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$
10	8 9	syl	$⊢ (D \in Fin \land P \in B) \to N (P) = (ι s \| \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$

Metamath Proof Explorer