psgnval

Description: Value of the permutation sign function. (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	psgnval	$⊢ P \in dom N \to N (P) = (ι s \| \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$

Step	Hyp	Ref	Expression
1		psgnval.g	$⊢ G = SymGrp (D)$
2		psgnval.t	$⊢ T = ran pmTrsp (D)$
3		psgnval.n	$⊢ N = pmSgn (D)$
4		eqeq1	$⊢ t = P \to (t = \sum_{G} w \leftrightarrow P = \sum_{G} w)$
5	4	anbi1d	$⊢ t = P \to ((t = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$
6	5	rexbidv	$⊢ t = P \to (\exists w \in Word T (t = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$
7	6	iotabidv	$⊢ t = P \to (ι s \| \exists w \in Word T (t = \sum_{G} w \land s = {(- 1)}^{\|w\|})) = (ι s \| \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$
8		eqid	$⊢ {Base}_{G} = {Base}_{G}$
9		eqid	$⊢ \{x \in {Base}_{G} \| dom (x ∖ I) \in Fin\} = \{x \in {Base}_{G} \| dom (x ∖ I) \in Fin\}$
10	1 8 9 3	psgnfn	$⊢ N Fn \{x \in {Base}_{G} \| dom (x ∖ I) \in Fin\}$
11	10	fndmi	$⊢ dom N = \{x \in {Base}_{G} \| dom (x ∖ I) \in Fin\}$
12	1 8 11 2 3	psgnfval	$⊢ N = (t \in dom N ⟼ (ι s \| \exists w \in Word T (t = \sum_{G} w \land s = {(- 1)}^{\|w\|})))$
13		iotaex	$⊢ (ι s \| \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|})) \in V$
14	7 12 13	fvmpt	$⊢ P \in dom N \to N (P) = (ι s \| \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$

Metamath Proof Explorer