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	\|- ( ph -> D e. V )
	psgnuni.w	\|- ( ph -> W e. Word T )
	psgnuni.x	\|- ( ph -> X e. Word T )
	psgnuni.e	\|- ( ph -> ( G gsum W ) = ( G gsum X ) )
Assertion	psgnuni	\|- ( ph -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` X ) ) )

Proof

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

Metamath Proof Explorer

Theorem psgnuni

Proof