Proof of Theorem psgnuni
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | psgnuni.w | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ Word 𝑇) | 
| 2 |  | lencl 14572 | . . . . . 6
⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) ∈
ℕ0) | 
| 3 | 1, 2 | syl 17 | . . . . 5
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) | 
| 4 | 3 | nn0zd 12641 | . . . 4
⊢ (𝜑 → (♯‘𝑊) ∈
ℤ) | 
| 5 |  | m1expcl 14128 | . . . 4
⊢
((♯‘𝑊)
∈ ℤ → (-1↑(♯‘𝑊)) ∈ ℤ) | 
| 6 | 4, 5 | syl 17 | . . 3
⊢ (𝜑 →
(-1↑(♯‘𝑊))
∈ ℤ) | 
| 7 | 6 | zcnd 12725 | . 2
⊢ (𝜑 →
(-1↑(♯‘𝑊))
∈ ℂ) | 
| 8 |  | psgnuni.x | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ Word 𝑇) | 
| 9 |  | lencl 14572 | . . . . . 6
⊢ (𝑋 ∈ Word 𝑇 → (♯‘𝑋) ∈
ℕ0) | 
| 10 | 8, 9 | syl 17 | . . . . 5
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ0) | 
| 11 | 10 | nn0zd 12641 | . . . 4
⊢ (𝜑 → (♯‘𝑋) ∈
ℤ) | 
| 12 |  | m1expcl 14128 | . . . 4
⊢
((♯‘𝑋)
∈ ℤ → (-1↑(♯‘𝑋)) ∈ ℤ) | 
| 13 | 11, 12 | syl 17 | . . 3
⊢ (𝜑 →
(-1↑(♯‘𝑋))
∈ ℤ) | 
| 14 | 13 | zcnd 12725 | . 2
⊢ (𝜑 →
(-1↑(♯‘𝑋))
∈ ℂ) | 
| 15 |  | neg1cn 12381 | . . 3
⊢ -1 ∈
ℂ | 
| 16 |  | neg1ne0 12383 | . . 3
⊢ -1 ≠
0 | 
| 17 |  | expne0i 14136 | . . 3
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0 ∧ (♯‘𝑋) ∈ ℤ) →
(-1↑(♯‘𝑋))
≠ 0) | 
| 18 | 15, 16, 11, 17 | mp3an12i 1466 | . 2
⊢ (𝜑 →
(-1↑(♯‘𝑋))
≠ 0) | 
| 19 |  | m1expaddsub 19517 | . . . 4
⊢
(((♯‘𝑊)
∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= (-1↑((♯‘𝑊) + (♯‘𝑋)))) | 
| 20 | 4, 11, 19 | syl2anc 584 | . . 3
⊢ (𝜑 →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= (-1↑((♯‘𝑊) + (♯‘𝑋)))) | 
| 21 |  | expsub 14152 | . . . . 5
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ ((♯‘𝑊) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ)) →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋)))) | 
| 22 | 15, 16, 21 | mpanl12 702 | . . . 4
⊢
(((♯‘𝑊)
∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋)))) | 
| 23 | 4, 11, 22 | syl2anc 584 | . . 3
⊢ (𝜑 →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋)))) | 
| 24 |  | revcl 14800 | . . . . . . . 8
⊢ (𝑋 ∈ Word 𝑇 → (reverse‘𝑋) ∈ Word 𝑇) | 
| 25 | 8, 24 | syl 17 | . . . . . . 7
⊢ (𝜑 → (reverse‘𝑋) ∈ Word 𝑇) | 
| 26 |  | ccatlen 14614 | . . . . . . 7
⊢ ((𝑊 ∈ Word 𝑇 ∧ (reverse‘𝑋) ∈ Word 𝑇) → (♯‘(𝑊 ++ (reverse‘𝑋))) = ((♯‘𝑊) + (♯‘(reverse‘𝑋)))) | 
| 27 | 1, 25, 26 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (♯‘(𝑊 ++ (reverse‘𝑋))) = ((♯‘𝑊) +
(♯‘(reverse‘𝑋)))) | 
| 28 |  | revlen 14801 | . . . . . . . 8
⊢ (𝑋 ∈ Word 𝑇 → (♯‘(reverse‘𝑋)) = (♯‘𝑋)) | 
| 29 | 8, 28 | syl 17 | . . . . . . 7
⊢ (𝜑 →
(♯‘(reverse‘𝑋)) = (♯‘𝑋)) | 
| 30 | 29 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → ((♯‘𝑊) +
(♯‘(reverse‘𝑋))) = ((♯‘𝑊) + (♯‘𝑋))) | 
| 31 | 27, 30 | eqtr2d 2777 | . . . . 5
⊢ (𝜑 → ((♯‘𝑊) + (♯‘𝑋)) = (♯‘(𝑊 ++ (reverse‘𝑋)))) | 
| 32 | 31 | oveq2d 7448 | . . . 4
⊢ (𝜑 →
(-1↑((♯‘𝑊)
+ (♯‘𝑋))) =
(-1↑(♯‘(𝑊
++ (reverse‘𝑋))))) | 
| 33 |  | psgnuni.g | . . . . 5
⊢ 𝐺 = (SymGrp‘𝐷) | 
| 34 |  | psgnuni.t | . . . . 5
⊢ 𝑇 = ran (pmTrsp‘𝐷) | 
| 35 |  | psgnuni.d | . . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑉) | 
| 36 |  | ccatcl 14613 | . . . . . 6
⊢ ((𝑊 ∈ Word 𝑇 ∧ (reverse‘𝑋) ∈ Word 𝑇) → (𝑊 ++ (reverse‘𝑋)) ∈ Word 𝑇) | 
| 37 | 1, 25, 36 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝑊 ++ (reverse‘𝑋)) ∈ Word 𝑇) | 
| 38 |  | psgnuni.e | . . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg 𝑊) = (𝐺 Σg 𝑋)) | 
| 39 | 38 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 →
((invg‘𝐺)‘(𝐺 Σg 𝑊)) =
((invg‘𝐺)‘(𝐺 Σg 𝑋))) | 
| 40 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 41 | 34, 33, 40 | symgtrinv 19491 | . . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑋 ∈ Word 𝑇) → ((invg‘𝐺)‘(𝐺 Σg 𝑋)) = (𝐺 Σg
(reverse‘𝑋))) | 
| 42 | 35, 8, 41 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 →
((invg‘𝐺)‘(𝐺 Σg 𝑋)) = (𝐺 Σg
(reverse‘𝑋))) | 
| 43 | 39, 42 | eqtr2d 2777 | . . . . . . . 8
⊢ (𝜑 → (𝐺 Σg
(reverse‘𝑋)) =
((invg‘𝐺)‘(𝐺 Σg 𝑊))) | 
| 44 | 43 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋))) =
((𝐺
Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊)))) | 
| 45 | 33 | symggrp 19419 | . . . . . . . . 9
⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp) | 
| 46 | 35, 45 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 47 |  | grpmnd 18959 | . . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | 
| 48 | 35, 45, 47 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Mnd) | 
| 49 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 50 | 34, 33, 49 | symgtrf 19488 | . . . . . . . . . . 11
⊢ 𝑇 ⊆ (Base‘𝐺) | 
| 51 |  | sswrd 14561 | . . . . . . . . . . 11
⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺)) | 
| 52 | 50, 51 | ax-mp 5 | . . . . . . . . . 10
⊢ Word
𝑇 ⊆ Word
(Base‘𝐺) | 
| 53 | 52, 1 | sselid 3980 | . . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ Word (Base‘𝐺)) | 
| 54 | 49 | gsumwcl 18853 | . . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺)) → (𝐺 Σg 𝑊) ∈ (Base‘𝐺)) | 
| 55 | 48, 53, 54 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐺 Σg 𝑊) ∈ (Base‘𝐺)) | 
| 56 |  | eqid 2736 | . . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 57 |  | eqid 2736 | . . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 58 | 49, 56, 57, 40 | grprinv 19009 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝐺 Σg
𝑊) ∈ (Base‘𝐺)) → ((𝐺 Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊))) = (0g‘𝐺)) | 
| 59 | 46, 55, 58 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊))) = (0g‘𝐺)) | 
| 60 | 44, 59 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋))) =
(0g‘𝐺)) | 
| 61 | 52, 25 | sselid 3980 | . . . . . . 7
⊢ (𝜑 → (reverse‘𝑋) ∈ Word (Base‘𝐺)) | 
| 62 | 49, 56 | gsumccat 18855 | . . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺) ∧ (reverse‘𝑋) ∈ Word (Base‘𝐺)) → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋)))) | 
| 63 | 48, 53, 61, 62 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋)))) | 
| 64 | 33 | symgid 19420 | . . . . . . 7
⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺)) | 
| 65 | 35, 64 | syl 17 | . . . . . 6
⊢ (𝜑 → ( I ↾ 𝐷) = (0g‘𝐺)) | 
| 66 | 60, 63, 65 | 3eqtr4d 2786 | . . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ( I ↾ 𝐷)) | 
| 67 | 33, 34, 35, 37, 66 | psgnunilem4 19516 | . . . 4
⊢ (𝜑 →
(-1↑(♯‘(𝑊
++ (reverse‘𝑋)))) =
1) | 
| 68 | 32, 67 | eqtrd 2776 | . . 3
⊢ (𝜑 →
(-1↑((♯‘𝑊)
+ (♯‘𝑋))) =
1) | 
| 69 | 20, 23, 68 | 3eqtr3d 2784 | . 2
⊢ (𝜑 →
((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋))) = 1) | 
| 70 | 7, 14, 18, 69 | diveq1d 12052 | 1
⊢ (𝜑 →
(-1↑(♯‘𝑊))
= (-1↑(♯‘𝑋))) |