Theorem 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	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnuni.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	psgnuni.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	psgnuni.w	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑇 )
	psgnuni.x	⊢ ( 𝜑 → 𝑋 ∈ Word 𝑇 )
	psgnuni.e	⊢ ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑋 ) )
Assertion	psgnuni	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnuni.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2		psgnuni.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3		psgnuni.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4		psgnuni.w	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑇 )
5		psgnuni.x	⊢ ( 𝜑 → 𝑋 ∈ Word 𝑇 )
6		psgnuni.e	⊢ ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑋 ) )
7		lencl	⊢ ( 𝑊 ∈ Word 𝑇 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
8	4 7	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
9	8	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
10		m1expcl	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
11	9 10	syl	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
12	11	zcnd	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
13		lencl	⊢ ( 𝑋 ∈ Word 𝑇 → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
14	5 13	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
15	14	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℤ )
16		m1expcl	⊢ ( ( ♯ ‘ 𝑋 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ∈ ℤ )
17	15 16	syl	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ∈ ℤ )
18	17	zcnd	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ∈ ℂ )
19		neg1cn	⊢ - 1 ∈ ℂ
20		neg1ne0	⊢ - 1 ≠ 0
21		expne0i	⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ≠ 0 )
22	19 20 15 21	mp3an12i	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ≠ 0 )
23		m1expaddsub	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) − ( ♯ ‘ 𝑋 ) ) ) = ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ 𝑋 ) ) ) )
24	9 15 23	syl2anc	⊢ ( 𝜑 → ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) − ( ♯ ‘ 𝑋 ) ) ) = ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ 𝑋 ) ) ) )
25		expsub	⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) ) → ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) − ( ♯ ‘ 𝑋 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) / ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ) )
26	19 20 25	mpanl12	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) − ( ♯ ‘ 𝑋 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) / ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ) )
27	9 15 26	syl2anc	⊢ ( 𝜑 → ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) − ( ♯ ‘ 𝑋 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) / ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ) )
28		revcl	⊢ ( 𝑋 ∈ Word 𝑇 → ( reverse ‘ 𝑋 ) ∈ Word 𝑇 )
29	5 28	syl	⊢ ( 𝜑 → ( reverse ‘ 𝑋 ) ∈ Word 𝑇 )
30		ccatlen	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( reverse ‘ 𝑋 ) ∈ Word 𝑇 ) → ( ♯ ‘ ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ( reverse ‘ 𝑋 ) ) ) )
31	4 29 30	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ( reverse ‘ 𝑋 ) ) ) )
32		revlen	⊢ ( 𝑋 ∈ Word 𝑇 → ( ♯ ‘ ( reverse ‘ 𝑋 ) ) = ( ♯ ‘ 𝑋 ) )
33	5 32	syl	⊢ ( 𝜑 → ( ♯ ‘ ( reverse ‘ 𝑋 ) ) = ( ♯ ‘ 𝑋 ) )
34	33	oveq2d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ( reverse ‘ 𝑋 ) ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ 𝑋 ) ) )
35	31 34	eqtr2d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ 𝑋 ) ) = ( ♯ ‘ ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ) )
36	35	oveq2d	⊢ ( 𝜑 → ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ 𝑋 ) ) ) = ( - 1 ↑ ( ♯ ‘ ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ) ) )
37		ccatcl	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( reverse ‘ 𝑋 ) ∈ Word 𝑇 ) → ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ∈ Word 𝑇 )
38	4 29 37	syl2anc	⊢ ( 𝜑 → ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ∈ Word 𝑇 )
39	6	fveq2d	⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝑊 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝑋 ) ) )
40		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
41	2 1 40	symgtrinv	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑋 ∈ Word 𝑇 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝑋 ) ) = ( 𝐺 Σg ( reverse ‘ 𝑋 ) ) )
42	3 5 41	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝑋 ) ) = ( 𝐺 Σg ( reverse ‘ 𝑋 ) ) )
43	39 42	eqtr2d	⊢ ( 𝜑 → ( 𝐺 Σg ( reverse ‘ 𝑋 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝑊 ) ) )
44	43	oveq2d	⊢ ( 𝜑 → ( ( 𝐺 Σg 𝑊 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( reverse ‘ 𝑋 ) ) ) = ( ( 𝐺 Σg 𝑊 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝑊 ) ) ) )
45	1	symggrp	⊢ ( 𝐷 ∈ 𝑉 → 𝐺 ∈ Grp )
46	3 45	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
47		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
48	3 45 47	3syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
49		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
50	2 1 49	symgtrf	⊢ 𝑇 ⊆ ( Base ‘ 𝐺 )
51		sswrd	⊢ ( 𝑇 ⊆ ( Base ‘ 𝐺 ) → Word 𝑇 ⊆ Word ( Base ‘ 𝐺 ) )
52	50 51	ax-mp	⊢ Word 𝑇 ⊆ Word ( Base ‘ 𝐺 )
53	52 4	sseldi	⊢ ( 𝜑 → 𝑊 ∈ Word ( Base ‘ 𝐺 ) )
54	49	gsumwcl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg 𝑊 ) ∈ ( Base ‘ 𝐺 ) )
55	48 53 54	syl2anc	⊢ ( 𝜑 → ( 𝐺 Σg 𝑊 ) ∈ ( Base ‘ 𝐺 ) )
56		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
57		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
58	49 56 57 40	grprinv	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐺 Σg 𝑊 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐺 Σg 𝑊 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝑊 ) ) ) = ( 0g ‘ 𝐺 ) )
59	46 55 58	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 Σg 𝑊 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝑊 ) ) ) = ( 0g ‘ 𝐺 ) )
60	44 59	eqtrd	⊢ ( 𝜑 → ( ( 𝐺 Σg 𝑊 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( reverse ‘ 𝑋 ) ) ) = ( 0g ‘ 𝐺 ) )
61	52 29	sseldi	⊢ ( 𝜑 → ( reverse ‘ 𝑋 ) ∈ Word ( Base ‘ 𝐺 ) )
62	49 56	gsumccat	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word ( Base ‘ 𝐺 ) ∧ ( reverse ‘ 𝑋 ) ∈ Word ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ) = ( ( 𝐺 Σg 𝑊 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( reverse ‘ 𝑋 ) ) ) )
63	48 53 61 62	syl3anc	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ) = ( ( 𝐺 Σg 𝑊 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( reverse ‘ 𝑋 ) ) ) )
64	1	symgid	⊢ ( 𝐷 ∈ 𝑉 → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
65	3 64	syl	⊢ ( 𝜑 → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
66	60 63 65	3eqtr4d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ) = ( I ↾ 𝐷 ) )
67	1 2 3 38 66	psgnunilem4	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ ( 𝑊 ++ ( reverse ‘ 𝑋 ) ) ) ) = 1 )
68	36 67	eqtrd	⊢ ( 𝜑 → ( - 1 ↑ ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ 𝑋 ) ) ) = 1 )
69	24 27 68	3eqtr3d	⊢ ( 𝜑 → ( ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) / ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) ) = 1 )
70	12 18 22 69	diveq1d	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑋 ) ) )