psgnuni

Description: If the same permutation can be written in more than one way as a product of transpositions, the parity of those products must agree; otherwise the product of one with the inverse of the other would be an odd representation of the identity. (Contributed by Stefan O'Rear, 27-Aug-2015)

	Ref	Expression
Hypotheses	psgnuni.g	$⊢ G = SymGrp (D)$
	psgnuni.t	$⊢ T = ran pmTrsp (D)$
	psgnuni.d	$⊢ φ \to D \in V$
	psgnuni.w	$⊢ φ \to W \in Word T$
	psgnuni.x	$⊢ φ \to X \in Word T$
	psgnuni.e	$⊢ φ \to \sum_{G} W = \sum_{G} X$
Assertion	psgnuni	$⊢ φ \to {(- 1)}^{\|W\|} = {(- 1)}^{\|X\|}$

Proof

Step	Hyp	Ref	Expression
1		psgnuni.g	$⊢ G = SymGrp (D)$
2		psgnuni.t	$⊢ T = ran pmTrsp (D)$
3		psgnuni.d	$⊢ φ \to D \in V$
4		psgnuni.w	$⊢ φ \to W \in Word T$
5		psgnuni.x	$⊢ φ \to X \in Word T$
6		psgnuni.e	$⊢ φ \to \sum_{G} W = \sum_{G} X$
7		lencl	$⊢ W \in Word T \to \|W\| \in ℕ_{0}$
8	4 7	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
9	8	nn0zd	$⊢ φ \to \|W\| \in ℤ$
10		m1expcl	$⊢ \|W\| \in ℤ \to {(- 1)}^{\|W\|} \in ℤ$
11	9 10	syl	$⊢ φ \to {(- 1)}^{\|W\|} \in ℤ$
12	11	zcnd	$⊢ φ \to {(- 1)}^{\|W\|} \in ℂ$
13		lencl	$⊢ X \in Word T \to \|X\| \in ℕ_{0}$
14	5 13	syl	$⊢ φ \to \|X\| \in ℕ_{0}$
15	14	nn0zd	$⊢ φ \to \|X\| \in ℤ$
16		m1expcl	$⊢ \|X\| \in ℤ \to {(- 1)}^{\|X\|} \in ℤ$
17	15 16	syl	$⊢ φ \to {(- 1)}^{\|X\|} \in ℤ$
18	17	zcnd	$⊢ φ \to {(- 1)}^{\|X\|} \in ℂ$
19		neg1cn	$⊢ - 1 \in ℂ$
20		neg1ne0	$⊢ - 1 \neq 0$
21		expne0i	$⊢ (- 1 \in ℂ \land - 1 \neq 0 \land \|X\| \in ℤ) \to {(- 1)}^{\|X\|} \neq 0$
22	19 20 15 21	mp3an12i	$⊢ φ \to {(- 1)}^{\|X\|} \neq 0$
23		m1expaddsub	$⊢ (\|W\| \in ℤ \land \|X\| \in ℤ) \to {(- 1)}^{\|W\| - \|X\|} = {(- 1)}^{\|W\| + \|X\|}$
24	9 15 23	syl2anc	$⊢ φ \to {(- 1)}^{\|W\| - \|X\|} = {(- 1)}^{\|W\| + \|X\|}$
25		expsub	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (\|W\| \in ℤ \land \|X\| \in ℤ)) \to {(- 1)}^{\|W\| - \|X\|} = \frac{{(- 1)}^{\|W\|}}{{(- 1)}^{\|X\|}}$
26	19 20 25	mpanl12	$⊢ (\|W\| \in ℤ \land \|X\| \in ℤ) \to {(- 1)}^{\|W\| - \|X\|} = \frac{{(- 1)}^{\|W\|}}{{(- 1)}^{\|X\|}}$
27	9 15 26	syl2anc	$⊢ φ \to {(- 1)}^{\|W\| - \|X\|} = \frac{{(- 1)}^{\|W\|}}{{(- 1)}^{\|X\|}}$
28		revcl	$⊢ X \in Word T \to reverse (X) \in Word T$
29	5 28	syl	$⊢ φ \to reverse (X) \in Word T$
30		ccatlen	$⊢ (W \in Word T \land reverse (X) \in Word T) \to \|W ++ reverse (X)\| = \|W\| + \|reverse (X)\|$
31	4 29 30	syl2anc	$⊢ φ \to \|W ++ reverse (X)\| = \|W\| + \|reverse (X)\|$
32		revlen	$⊢ X \in Word T \to \|reverse (X)\| = \|X\|$
33	5 32	syl	$⊢ φ \to \|reverse (X)\| = \|X\|$
34	33	oveq2d	$⊢ φ \to \|W\| + \|reverse (X)\| = \|W\| + \|X\|$
35	31 34	eqtr2d	$⊢ φ \to \|W\| + \|X\| = \|W ++ reverse (X)\|$
36	35	oveq2d	$⊢ φ \to {(- 1)}^{\|W\| + \|X\|} = {(- 1)}^{\|W ++ reverse (X)\|}$
37		ccatcl	$⊢ (W \in Word T \land reverse (X) \in Word T) \to W ++ reverse (X) \in Word T$
38	4 29 37	syl2anc	$⊢ φ \to W ++ reverse (X) \in Word T$
39	6	fveq2d	$⊢ φ \to {inv}_{g} (G) (\sum_{G} W) = {inv}_{g} (G) (\sum_{G} X)$
40		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
41	2 1 40	symgtrinv	$⊢ (D \in V \land X \in Word T) \to {inv}_{g} (G) (\sum_{G} X) = \sum_{G} reverse (X)$
42	3 5 41	syl2anc	$⊢ φ \to {inv}_{g} (G) (\sum_{G} X) = \sum_{G} reverse (X)$
43	39 42	eqtr2d	$⊢ φ \to \sum_{G} reverse (X) = {inv}_{g} (G) (\sum_{G} W)$
44	43	oveq2d	$⊢ φ \to (\sum_{G}, W) +_{G} (\sum_{G}, reverse (X)) = (\sum_{G}, W) +_{G} {inv}_{g} (G) (\sum_{G} W)$
45	1	symggrp	$⊢ D \in V \to G \in Grp$
46	3 45	syl	$⊢ φ \to G \in Grp$
47		grpmnd	$⊢ G \in Grp \to G \in Mnd$
48	3 45 47	3syl	$⊢ φ \to G \in Mnd$
49		eqid	$⊢ {Base}_{G} = {Base}_{G}$
50	2 1 49	symgtrf	$⊢ T \subseteq {Base}_{G}$
51		sswrd	$⊢ T \subseteq {Base}_{G} \to Word T \subseteq Word {Base}_{G}$
52	50 51	ax-mp	$⊢ Word T \subseteq Word {Base}_{G}$
53	52 4	sselid	$⊢ φ \to W \in Word {Base}_{G}$
54	49	gsumwcl	$⊢ (G \in Mnd \land W \in Word {Base}_{G}) \to \sum_{G} W \in {Base}_{G}$
55	48 53 54	syl2anc	$⊢ φ \to \sum_{G} W \in {Base}_{G}$
56		eqid	$⊢ +_{G} = +_{G}$
57		eqid	$⊢ 0_{G} = 0_{G}$
58	49 56 57 40	grprinv	$⊢ (G \in Grp \land \sum_{G} W \in {Base}_{G}) \to (\sum_{G}, W) +_{G} {inv}_{g} (G) (\sum_{G} W) = 0_{G}$
59	46 55 58	syl2anc	$⊢ φ \to (\sum_{G}, W) +_{G} {inv}_{g} (G) (\sum_{G} W) = 0_{G}$
60	44 59	eqtrd	$⊢ φ \to (\sum_{G}, W) +_{G} (\sum_{G}, reverse (X)) = 0_{G}$
61	52 29	sselid	$⊢ φ \to reverse (X) \in Word {Base}_{G}$
62	49 56	gsumccat	$⊢ (G \in Mnd \land W \in Word {Base}_{G} \land reverse (X) \in Word {Base}_{G}) \to \sum_{G} (W ++ reverse (X)) = (\sum_{G}, W) +_{G} (\sum_{G}, reverse (X))$
63	48 53 61 62	syl3anc	$⊢ φ \to \sum_{G} (W ++ reverse (X)) = (\sum_{G}, W) +_{G} (\sum_{G}, reverse (X))$
64	1	symgid	$⊢ D \in V \to {I ↾}_{D} = 0_{G}$
65	3 64	syl	$⊢ φ \to {I ↾}_{D} = 0_{G}$
66	60 63 65	3eqtr4d	$⊢ φ \to \sum_{G} (W ++ reverse (X)) = {I ↾}_{D}$
67	1 2 3 38 66	psgnunilem4	$⊢ φ \to {(- 1)}^{\|W ++ reverse (X)\|} = 1$
68	36 67	eqtrd	$⊢ φ \to {(- 1)}^{\|W\| + \|X\|} = 1$
69	24 27 68	3eqtr3d	$⊢ φ \to \frac{{(- 1)}^{\|W\|}}{{(- 1)}^{\|X\|}} = 1$
70	12 18 22 69	diveq1d	$⊢ φ \to {(- 1)}^{\|W\|} = {(- 1)}^{\|X\|}$

Metamath Proof Explorer

Theorem psgnuni

Proof