psgneu

Description: A finitary permutation has exactly one 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	psgneu	$⊢ P \in dom N \to \exists! s \exists w \in Word T (P = \sum_{G} w \land s = {(- 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		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5	1 3 4	psgneldm	$⊢ P \in dom N \leftrightarrow (P \in {Base}_{G} \land dom (P ∖ I) \in Fin)$
6	5	simplbi	$⊢ P \in dom N \to P \in {Base}_{G}$
7	1 4	elbasfv	$⊢ P \in {Base}_{G} \to D \in V$
8	6 7	syl	$⊢ P \in dom N \to D \in V$
9	1 2 3	psgneldm2	$⊢ D \in V \to (P \in dom N \leftrightarrow \exists w \in Word T P = \sum_{G} w)$
10	8 9	syl	$⊢ P \in dom N \to (P \in dom N \leftrightarrow \exists w \in Word T P = \sum_{G} w)$
11	10	ibi	$⊢ P \in dom N \to \exists w \in Word T P = \sum_{G} w$
12		simpr	$⊢ ((P \in dom N \land w \in Word T) \land P = \sum_{G} w) \to P = \sum_{G} w$
13		eqid	$⊢ {(- 1)}^{\|w\|} = {(- 1)}^{\|w\|}$
14		ovex	$⊢ {(- 1)}^{\|w\|} \in V$
15		eqeq1	$⊢ s = {(- 1)}^{\|w\|} \to (s = {(- 1)}^{\|w\|} \leftrightarrow {(- 1)}^{\|w\|} = {(- 1)}^{\|w\|})$
16	15	anbi2d	$⊢ s = {(- 1)}^{\|w\|} \to ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow (P = \sum_{G} w \land {(- 1)}^{\|w\|} = {(- 1)}^{\|w\|}))$
17	14 16	spcev	$⊢ (P = \sum_{G} w \land {(- 1)}^{\|w\|} = {(- 1)}^{\|w\|}) \to \exists s (P = \sum_{G} w \land s = {(- 1)}^{\|w\|})$
18	12 13 17	sylancl	$⊢ ((P \in dom N \land w \in Word T) \land P = \sum_{G} w) \to \exists s (P = \sum_{G} w \land s = {(- 1)}^{\|w\|})$
19	18	ex	$⊢ (P \in dom N \land w \in Word T) \to (P = \sum_{G} w \to \exists s (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$
20	19	reximdva	$⊢ P \in dom N \to (\exists w \in Word T P = \sum_{G} w \to \exists w \in Word T \exists s (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}))$
21	11 20	mpd	$⊢ P \in dom N \to \exists w \in Word T \exists s (P = \sum_{G} w \land s = {(- 1)}^{\|w\|})$
22		rexcom4	$⊢ \exists w \in Word T \exists s (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow \exists s \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|})$
23	21 22	sylib	$⊢ P \in dom N \to \exists s \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|})$
24		reeanv	$⊢ \exists w \in Word T \exists x \in Word T ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|})) \leftrightarrow (\exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land \exists x \in Word T (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))$
25	8	ad2antrr	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to D \in V$
26		simplrl	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to w \in Word T$
27		simplrr	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to x \in Word T$
28		simprll	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to P = \sum_{G} w$
29		simprrl	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to P = \sum_{G} x$
30	28 29	eqtr3d	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to \sum_{G} w = \sum_{G} x$
31	1 2 25 26 27 30	psgnuni	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to {(- 1)}^{\|w\|} = {(- 1)}^{\|x\|}$
32		simprlr	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to s = {(- 1)}^{\|w\|}$
33		simprrr	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to t = {(- 1)}^{\|x\|}$
34	31 32 33	3eqtr4d	$⊢ ((P \in dom N \land (w \in Word T \land x \in Word T)) \land ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))) \to s = t$
35	34	ex	$⊢ (P \in dom N \land (w \in Word T \land x \in Word T)) \to (((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|})) \to s = t)$
36	35	rexlimdvva	$⊢ P \in dom N \to (\exists w \in Word T \exists x \in Word T ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land (P = \sum_{G} x \land t = {(- 1)}^{\|x\|})) \to s = t)$
37	24 36	biimtrrid	$⊢ P \in dom N \to ((\exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land \exists x \in Word T (P = \sum_{G} x \land t = {(- 1)}^{\|x\|})) \to s = t)$
38	37	alrimivv	$⊢ P \in dom N \to \forall s \forall t ((\exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land \exists x \in Word T (P = \sum_{G} x \land t = {(- 1)}^{\|x\|})) \to s = t)$
39		eqeq1	$⊢ s = t \to (s = {(- 1)}^{\|w\|} \leftrightarrow t = {(- 1)}^{\|w\|})$
40	39	anbi2d	$⊢ s = t \to ((P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow (P = \sum_{G} w \land t = {(- 1)}^{\|w\|}))$
41	40	rexbidv	$⊢ s = t \to (\exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow \exists w \in Word T (P = \sum_{G} w \land t = {(- 1)}^{\|w\|}))$
42		oveq2	$⊢ w = x \to \sum_{G} w = \sum_{G} x$
43	42	eqeq2d	$⊢ w = x \to (P = \sum_{G} w \leftrightarrow P = \sum_{G} x)$
44		fveq2	$⊢ w = x \to \|w\| = \|x\|$
45	44	oveq2d	$⊢ w = x \to {(- 1)}^{\|w\|} = {(- 1)}^{\|x\|}$
46	45	eqeq2d	$⊢ w = x \to (t = {(- 1)}^{\|w\|} \leftrightarrow t = {(- 1)}^{\|x\|})$
47	43 46	anbi12d	$⊢ w = x \to ((P = \sum_{G} w \land t = {(- 1)}^{\|w\|}) \leftrightarrow (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))$
48	47	cbvrexvw	$⊢ \exists w \in Word T (P = \sum_{G} w \land t = {(- 1)}^{\|w\|}) \leftrightarrow \exists x \in Word T (P = \sum_{G} x \land t = {(- 1)}^{\|x\|})$
49	41 48	bitrdi	$⊢ s = t \to (\exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow \exists x \in Word T (P = \sum_{G} x \land t = {(- 1)}^{\|x\|}))$
50	49	eu4	$⊢ \exists! s \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow (\exists s \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land \forall s \forall t ((\exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|}) \land \exists x \in Word T (P = \sum_{G} x \land t = {(- 1)}^{\|x\|})) \to s = t))$
51	23 38 50	sylanbrc	$⊢ P \in dom N \to \exists! s \exists w \in Word T (P = \sum_{G} w \land s = {(- 1)}^{\|w\|})$

Metamath Proof Explorer

Theorem psgneu

Proof