Proof of Theorem psgnuni
Step | Hyp | Ref
| Expression |
1 | | psgnuni.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Word 𝑇) |
2 | | lencl 13324 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑇 → (#‘𝑊) ∈
ℕ0) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝑊) ∈
ℕ0) |
4 | 3 | nn0zd 11480 |
. . . 4
⊢ (𝜑 → (#‘𝑊) ∈ ℤ) |
5 | | m1expcl 12883 |
. . . 4
⊢
((#‘𝑊) ∈
ℤ → (-1↑(#‘𝑊)) ∈ ℤ) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → (-1↑(#‘𝑊)) ∈
ℤ) |
7 | 6 | zcnd 11483 |
. 2
⊢ (𝜑 → (-1↑(#‘𝑊)) ∈
ℂ) |
8 | | psgnuni.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ Word 𝑇) |
9 | | lencl 13324 |
. . . . . 6
⊢ (𝑋 ∈ Word 𝑇 → (#‘𝑋) ∈
ℕ0) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝑋) ∈
ℕ0) |
11 | 10 | nn0zd 11480 |
. . . 4
⊢ (𝜑 → (#‘𝑋) ∈ ℤ) |
12 | | m1expcl 12883 |
. . . 4
⊢
((#‘𝑋) ∈
ℤ → (-1↑(#‘𝑋)) ∈ ℤ) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 → (-1↑(#‘𝑋)) ∈
ℤ) |
14 | 13 | zcnd 11483 |
. 2
⊢ (𝜑 → (-1↑(#‘𝑋)) ∈
ℂ) |
15 | | neg1cn 11124 |
. . . 4
⊢ -1 ∈
ℂ |
16 | | neg1ne0 11126 |
. . . 4
⊢ -1 ≠
0 |
17 | | expne0i 12892 |
. . . 4
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0 ∧ (#‘𝑋) ∈ ℤ) →
(-1↑(#‘𝑋)) ≠
0) |
18 | 15, 16, 17 | mp3an12 1414 |
. . 3
⊢
((#‘𝑋) ∈
ℤ → (-1↑(#‘𝑋)) ≠ 0) |
19 | 11, 18 | syl 17 |
. 2
⊢ (𝜑 → (-1↑(#‘𝑋)) ≠ 0) |
20 | | m1expaddsub 17918 |
. . . . 5
⊢
(((#‘𝑊) ∈
ℤ ∧ (#‘𝑋)
∈ ℤ) → (-1↑((#‘𝑊) − (#‘𝑋))) = (-1↑((#‘𝑊) + (#‘𝑋)))) |
21 | 4, 11, 20 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (-1↑((#‘𝑊) − (#‘𝑋))) = (-1↑((#‘𝑊) + (#‘𝑋)))) |
22 | | expsub 12908 |
. . . . . 6
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ ((#‘𝑊) ∈ ℤ ∧ (#‘𝑋) ∈ ℤ)) →
(-1↑((#‘𝑊)
− (#‘𝑋))) =
((-1↑(#‘𝑊)) /
(-1↑(#‘𝑋)))) |
23 | 15, 16, 22 | mpanl12 718 |
. . . . 5
⊢
(((#‘𝑊) ∈
ℤ ∧ (#‘𝑋)
∈ ℤ) → (-1↑((#‘𝑊) − (#‘𝑋))) = ((-1↑(#‘𝑊)) / (-1↑(#‘𝑋)))) |
24 | 4, 11, 23 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (-1↑((#‘𝑊) − (#‘𝑋))) = ((-1↑(#‘𝑊)) / (-1↑(#‘𝑋)))) |
25 | 21, 24 | eqtr3d 2658 |
. . 3
⊢ (𝜑 → (-1↑((#‘𝑊) + (#‘𝑋))) = ((-1↑(#‘𝑊)) / (-1↑(#‘𝑋)))) |
26 | | revcl 13510 |
. . . . . . . 8
⊢ (𝑋 ∈ Word 𝑇 → (reverse‘𝑋) ∈ Word 𝑇) |
27 | 8, 26 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (reverse‘𝑋) ∈ Word 𝑇) |
28 | | ccatlen 13360 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑇 ∧ (reverse‘𝑋) ∈ Word 𝑇) → (#‘(𝑊 ++ (reverse‘𝑋))) = ((#‘𝑊) + (#‘(reverse‘𝑋)))) |
29 | 1, 27, 28 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (#‘(𝑊 ++ (reverse‘𝑋))) = ((#‘𝑊) +
(#‘(reverse‘𝑋)))) |
30 | | revlen 13511 |
. . . . . . . 8
⊢ (𝑋 ∈ Word 𝑇 → (#‘(reverse‘𝑋)) = (#‘𝑋)) |
31 | 8, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(#‘(reverse‘𝑋))
= (#‘𝑋)) |
32 | 31 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → ((#‘𝑊) +
(#‘(reverse‘𝑋))) = ((#‘𝑊) + (#‘𝑋))) |
33 | 29, 32 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (#‘(𝑊 ++ (reverse‘𝑋))) = ((#‘𝑊) + (#‘𝑋))) |
34 | 33 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → (-1↑(#‘(𝑊 ++ (reverse‘𝑋)))) = (-1↑((#‘𝑊) + (#‘𝑋)))) |
35 | | psgnuni.g |
. . . . 5
⊢ 𝐺 = (SymGrp‘𝐷) |
36 | | psgnuni.t |
. . . . 5
⊢ 𝑇 = ran (pmTrsp‘𝐷) |
37 | | psgnuni.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
38 | | ccatcl 13359 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑇 ∧ (reverse‘𝑋) ∈ Word 𝑇) → (𝑊 ++ (reverse‘𝑋)) ∈ Word 𝑇) |
39 | 1, 27, 38 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝑊 ++ (reverse‘𝑋)) ∈ Word 𝑇) |
40 | | psgnuni.e |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg 𝑊) = (𝐺 Σg 𝑋)) |
41 | 40 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 →
((invg‘𝐺)‘(𝐺 Σg 𝑊)) =
((invg‘𝐺)‘(𝐺 Σg 𝑋))) |
42 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(invg‘𝐺) = (invg‘𝐺) |
43 | 36, 35, 42 | symgtrinv 17892 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑋 ∈ Word 𝑇) → ((invg‘𝐺)‘(𝐺 Σg 𝑋)) = (𝐺 Σg
(reverse‘𝑋))) |
44 | 37, 8, 43 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 →
((invg‘𝐺)‘(𝐺 Σg 𝑋)) = (𝐺 Σg
(reverse‘𝑋))) |
45 | 41, 44 | eqtr2d 2657 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 Σg
(reverse‘𝑋)) =
((invg‘𝐺)‘(𝐺 Σg 𝑊))) |
46 | 45 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋))) =
((𝐺
Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊)))) |
47 | 35 | symggrp 17820 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp) |
48 | 37, 47 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Grp) |
49 | | grpmnd 17429 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Mnd) |
51 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Base‘𝐺) =
(Base‘𝐺) |
52 | 36, 35, 51 | symgtrf 17889 |
. . . . . . . . . . 11
⊢ 𝑇 ⊆ (Base‘𝐺) |
53 | | sswrd 13313 |
. . . . . . . . . . 11
⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺)) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . 10
⊢ Word
𝑇 ⊆ Word
(Base‘𝐺) |
55 | 54, 1 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ Word (Base‘𝐺)) |
56 | 51 | gsumwcl 17377 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺)) → (𝐺 Σg 𝑊) ∈ (Base‘𝐺)) |
57 | 50, 55, 56 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 Σg 𝑊) ∈ (Base‘𝐺)) |
58 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
59 | | eqid 2622 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
60 | 51, 58, 59, 42 | grprinv 17469 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝐺 Σg
𝑊) ∈ (Base‘𝐺)) → ((𝐺 Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊))) = (0g‘𝐺)) |
61 | 48, 57, 60 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)((invg‘𝐺)‘(𝐺 Σg 𝑊))) = (0g‘𝐺)) |
62 | 46, 61 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋))) =
(0g‘𝐺)) |
63 | 54, 27 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → (reverse‘𝑋) ∈ Word (Base‘𝐺)) |
64 | 51, 58 | gsumccat 17378 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺) ∧ (reverse‘𝑋) ∈ Word (Base‘𝐺)) → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋)))) |
65 | 50, 55, 63, 64 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g‘𝐺)(𝐺 Σg
(reverse‘𝑋)))) |
66 | 35 | symgid 17821 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺)) |
67 | 37, 66 | syl 17 |
. . . . . 6
⊢ (𝜑 → ( I ↾ 𝐷) = (0g‘𝐺)) |
68 | 62, 65, 67 | 3eqtr4d 2666 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ( I ↾ 𝐷)) |
69 | 35, 36, 37, 39, 68 | psgnunilem4 17917 |
. . . 4
⊢ (𝜑 → (-1↑(#‘(𝑊 ++ (reverse‘𝑋)))) = 1) |
70 | 34, 69 | eqtr3d 2658 |
. . 3
⊢ (𝜑 → (-1↑((#‘𝑊) + (#‘𝑋))) = 1) |
71 | 25, 70 | eqtr3d 2658 |
. 2
⊢ (𝜑 → ((-1↑(#‘𝑊)) / (-1↑(#‘𝑋))) = 1) |
72 | 7, 14, 19, 71 | diveq1d 10809 |
1
⊢ (𝜑 → (-1↑(#‘𝑊)) = (-1↑(#‘𝑋))) |