This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 sselid ⊢ ( 𝜑 → 𝑊 ∈ 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 sselid ⊢ ( 𝜑 → ( 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 ↑ ( ♯ ‘ 𝑋 ) ) )