Proof of Theorem psgnuni
Step | Hyp | Ref
| Expression |
1 | | psgnuni.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Word 𝑇) |
2 | | lencl 13621 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) ∈
ℕ0) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
4 | 3 | nn0zd 11832 |
. . . 4
⊢ (𝜑 → (♯‘𝑊) ∈
ℤ) |
5 | | m1expcl 13201 |
. . . 4
⊢
((♯‘𝑊)
∈ ℤ → (-1↑(♯‘𝑊)) ∈ ℤ) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 →
(-1↑(♯‘𝑊))
∈ ℤ) |
7 | 6 | zcnd 11835 |
. 2
⊢ (𝜑 →
(-1↑(♯‘𝑊))
∈ ℂ) |
8 | | psgnuni.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ Word 𝑇) |
9 | | lencl 13621 |
. . . . . 6
⊢ (𝑋 ∈ Word 𝑇 → (♯‘𝑋) ∈
ℕ0) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ0) |
11 | 10 | nn0zd 11832 |
. . . 4
⊢ (𝜑 → (♯‘𝑋) ∈
ℤ) |
12 | | m1expcl 13201 |
. . . 4
⊢
((♯‘𝑋)
∈ ℤ → (-1↑(♯‘𝑋)) ∈ ℤ) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 →
(-1↑(♯‘𝑋))
∈ ℤ) |
14 | 13 | zcnd 11835 |
. 2
⊢ (𝜑 →
(-1↑(♯‘𝑋))
∈ ℂ) |
15 | | neg1cn 11496 |
. . . 4
⊢ -1 ∈
ℂ |
16 | | neg1ne0 11498 |
. . . 4
⊢ -1 ≠
0 |
17 | | expne0i 13210 |
. . . 4
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0 ∧ (♯‘𝑋) ∈ ℤ) →
(-1↑(♯‘𝑋))
≠ 0) |
18 | 15, 16, 17 | mp3an12 1524 |
. . 3
⊢
((♯‘𝑋)
∈ ℤ → (-1↑(♯‘𝑋)) ≠ 0) |
19 | 11, 18 | syl 17 |
. 2
⊢ (𝜑 →
(-1↑(♯‘𝑋))
≠ 0) |
20 | | m1expaddsub 18302 |
. . . . 5
⊢
(((♯‘𝑊)
∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= (-1↑((♯‘𝑊) + (♯‘𝑋)))) |
21 | 4, 11, 20 | syl2anc 579 |
. . . 4
⊢ (𝜑 →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= (-1↑((♯‘𝑊) + (♯‘𝑋)))) |
22 | | expsub 13226 |
. . . . . 6
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ ((♯‘𝑊) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ)) →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋)))) |
23 | 15, 16, 22 | mpanl12 692 |
. . . . 5
⊢
(((♯‘𝑊)
∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋)))) |
24 | 4, 11, 23 | syl2anc 579 |
. . . 4
⊢ (𝜑 →
(-1↑((♯‘𝑊)
− (♯‘𝑋)))
= ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋)))) |
25 | 21, 24 | eqtr3d 2815 |
. . 3
⊢ (𝜑 →
(-1↑((♯‘𝑊)
+ (♯‘𝑋))) =
((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋)))) |
26 | | revcl 13907 |
. . . . . . . 8
⊢ (𝑋 ∈ Word 𝑇 → (reverse‘𝑋) ∈ Word 𝑇) |
27 | 8, 26 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (reverse‘𝑋) ∈ Word 𝑇) |
28 | | ccatlen 13665 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑇 ∧ (reverse‘𝑋) ∈ Word 𝑇) → (♯‘(𝑊 ++ (reverse‘𝑋))) = ((♯‘𝑊) + (♯‘(reverse‘𝑋)))) |
29 | 1, 27, 28 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝑊 ++ (reverse‘𝑋))) = ((♯‘𝑊) +
(♯‘(reverse‘𝑋)))) |
30 | | revlen 13908 |
. . . . . . . 8
⊢ (𝑋 ∈ Word 𝑇 → (♯‘(reverse‘𝑋)) = (♯‘𝑋)) |
31 | 8, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(♯‘(reverse‘𝑋)) = (♯‘𝑋)) |
32 | 31 | oveq2d 6938 |
. . . . . 6
⊢ (𝜑 → ((♯‘𝑊) +
(♯‘(reverse‘𝑋))) = ((♯‘𝑊) + (♯‘𝑋))) |
33 | 29, 32 | eqtrd 2813 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑊 ++ (reverse‘𝑋))) = ((♯‘𝑊) + (♯‘𝑋))) |
34 | 33 | oveq2d 6938 |
. . . 4
⊢ (𝜑 →
(-1↑(♯‘(𝑊
++ (reverse‘𝑋)))) =
(-1↑((♯‘𝑊)
+ (♯‘𝑋)))) |
35 | | psgnuni.g |
. . . . 5
⊢ 𝐺 = (SymGrp‘𝐷) |
36 | | psgnuni.t |
. . . . 5
⊢ 𝑇 = ran (pmTrsp‘𝐷) |
37 | | psgnuni.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
38 | | ccatcl 13664 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑇 ∧ (reverse‘𝑋) ∈ Word 𝑇) → (𝑊 ++ (reverse‘𝑋)) ∈ Word 𝑇) |
39 | 1, 27, 38 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝑊 ++ (reverse‘𝑋)) ∈ Word 𝑇) |
40 | | psgnuni.e |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg 𝑊) = (𝐺 Σg 𝑋)) |
41 | 40 | fveq2d 6450 |
. . . . . . . . 9
⊢ (𝜑 →
((invg‘𝐺)‘(𝐺 Σg 𝑊)) =
((invg‘𝐺)‘(𝐺 Σg 𝑋))) |
42 | | eqid 2777 |
. . . . . . . . . . 11
⊢
(invg‘𝐺) = (invg‘𝐺) |
43 | 36, 35, 42 | symgtrinv 18275 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑋 ∈ Word 𝑇) → ((invg‘𝐺)‘(𝐺 Σg 𝑋)) = (𝐺 Σg
(reverse‘𝑋))) |
44 | 37, 8, 43 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 →
((invg‘𝐺)‘(𝐺 Σg 𝑋)) = (𝐺 Σg
(reverse‘𝑋))) |
45 | 41, 44 | eqtr2d 2814 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 Σg
(reverse‘𝑋)) =
((invg‘𝐺)‘(𝐺 Σg 𝑊))) |
46 | 45 | oveq2d 6938 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋))) =
((𝐺
Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊)))) |
47 | 35 | symggrp 18203 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp) |
48 | 37, 47 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Grp) |
49 | | grpmnd 17816 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Mnd) |
51 | | eqid 2777 |
. . . . . . . . . . . 12
⊢
(Base‘𝐺) =
(Base‘𝐺) |
52 | 36, 35, 51 | symgtrf 18272 |
. . . . . . . . . . 11
⊢ 𝑇 ⊆ (Base‘𝐺) |
53 | | sswrd 13607 |
. . . . . . . . . . 11
⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺)) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . 10
⊢ Word
𝑇 ⊆ Word
(Base‘𝐺) |
55 | 54, 1 | sseldi 3818 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ Word (Base‘𝐺)) |
56 | 51 | gsumwcl 17763 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺)) → (𝐺 Σg 𝑊) ∈ (Base‘𝐺)) |
57 | 50, 55, 56 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 Σg 𝑊) ∈ (Base‘𝐺)) |
58 | | eqid 2777 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
59 | | eqid 2777 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
60 | 51, 58, 59, 42 | grprinv 17856 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝐺 Σg
𝑊) ∈ (Base‘𝐺)) → ((𝐺 Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊))) = (0g‘𝐺)) |
61 | 48, 57, 60 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊))) = (0g‘𝐺)) |
62 | 46, 61 | eqtrd 2813 |
. . . . . 6
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋))) =
(0g‘𝐺)) |
63 | 54, 27 | sseldi 3818 |
. . . . . . 7
⊢ (𝜑 → (reverse‘𝑋) ∈ Word (Base‘𝐺)) |
64 | 51, 58 | gsumccat 17764 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺) ∧ (reverse‘𝑋) ∈ Word (Base‘𝐺)) → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋)))) |
65 | 50, 55, 63, 64 | syl3anc 1439 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋)))) |
66 | 35 | symgid 18204 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺)) |
67 | 37, 66 | syl 17 |
. . . . . 6
⊢ (𝜑 → ( I ↾ 𝐷) = (0g‘𝐺)) |
68 | 62, 65, 67 | 3eqtr4d 2823 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ( I ↾ 𝐷)) |
69 | 35, 36, 37, 39, 68 | psgnunilem4 18301 |
. . . 4
⊢ (𝜑 →
(-1↑(♯‘(𝑊
++ (reverse‘𝑋)))) =
1) |
70 | 34, 69 | eqtr3d 2815 |
. . 3
⊢ (𝜑 →
(-1↑((♯‘𝑊)
+ (♯‘𝑋))) =
1) |
71 | 25, 70 | eqtr3d 2815 |
. 2
⊢ (𝜑 →
((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋))) = 1) |
72 | 7, 14, 19, 71 | diveq1d 11159 |
1
⊢ (𝜑 →
(-1↑(♯‘𝑊))
= (-1↑(♯‘𝑋))) |