Step | Hyp | Ref
| Expression |
1 | | psgnghm.s |
. . . . . 6
⊢ 𝑆 = (SymGrp‘𝐷) |
2 | | eqid 2798 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2798 |
. . . . . 6
⊢ {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} =
{𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈
Fin} |
4 | | psgnghm.n |
. . . . . 6
⊢ 𝑁 = (pmSgn‘𝐷) |
5 | 1, 2, 3, 4 | psgnfn 18621 |
. . . . 5
⊢ 𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} |
6 | 5 | fndmi 6426 |
. . . 4
⊢ dom 𝑁 = {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} |
7 | 6 | ssrab3 4008 |
. . 3
⊢ dom 𝑁 ⊆ (Base‘𝑆) |
8 | | psgnghm.f |
. . . 4
⊢ 𝐹 = (𝑆 ↾s dom 𝑁) |
9 | 8, 2 | ressbas2 16547 |
. . 3
⊢ (dom
𝑁 ⊆ (Base‘𝑆) → dom 𝑁 = (Base‘𝐹)) |
10 | 7, 9 | ax-mp 5 |
. 2
⊢ dom 𝑁 = (Base‘𝐹) |
11 | | psgnghm.u |
. . 3
⊢ 𝑈 =
((mulGrp‘ℂfld) ↾s {1,
-1}) |
12 | 11 | cnmsgnbas 20267 |
. 2
⊢ {1, -1} =
(Base‘𝑈) |
13 | 10 | fvexi 6659 |
. . 3
⊢ dom 𝑁 ∈ V |
14 | | eqid 2798 |
. . . 4
⊢
(+g‘𝑆) = (+g‘𝑆) |
15 | 8, 14 | ressplusg 16604 |
. . 3
⊢ (dom
𝑁 ∈ V →
(+g‘𝑆) =
(+g‘𝐹)) |
16 | 13, 15 | ax-mp 5 |
. 2
⊢
(+g‘𝑆) = (+g‘𝐹) |
17 | | prex 5298 |
. . 3
⊢ {1, -1}
∈ V |
18 | | eqid 2798 |
. . . . 5
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
19 | | cnfldmul 20097 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
20 | 18, 19 | mgpplusg 19236 |
. . . 4
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
21 | 11, 20 | ressplusg 16604 |
. . 3
⊢ ({1, -1}
∈ V → · = (+g‘𝑈)) |
22 | 17, 21 | ax-mp 5 |
. 2
⊢ ·
= (+g‘𝑈) |
23 | 1, 4 | psgndmsubg 18622 |
. . 3
⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝑆)) |
24 | 8 | subggrp 18274 |
. . 3
⊢ (dom
𝑁 ∈
(SubGrp‘𝑆) →
𝐹 ∈
Grp) |
25 | 23, 24 | syl 17 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝐹 ∈ Grp) |
26 | 11 | cnmsgngrp 20268 |
. . 3
⊢ 𝑈 ∈ Grp |
27 | 26 | a1i 11 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝑈 ∈ Grp) |
28 | | fnfun 6423 |
. . . . . 6
⊢ (𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} → Fun 𝑁) |
29 | 5, 28 | ax-mp 5 |
. . . . 5
⊢ Fun 𝑁 |
30 | | funfn 6354 |
. . . . 5
⊢ (Fun
𝑁 ↔ 𝑁 Fn dom 𝑁) |
31 | 29, 30 | mpbi 233 |
. . . 4
⊢ 𝑁 Fn dom 𝑁 |
32 | 31 | a1i 11 |
. . 3
⊢ (𝐷 ∈ 𝑉 → 𝑁 Fn dom 𝑁) |
33 | | eqid 2798 |
. . . . . 6
⊢ ran
(pmTrsp‘𝐷) = ran
(pmTrsp‘𝐷) |
34 | 1, 33, 4 | psgnvali 18628 |
. . . . 5
⊢ (𝑥 ∈ dom 𝑁 → ∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧)))) |
35 | | lencl 13876 |
. . . . . . . . . 10
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
(♯‘𝑧) ∈
ℕ0) |
36 | 35 | nn0zd 12073 |
. . . . . . . . 9
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
(♯‘𝑧) ∈
ℤ) |
37 | | m1expcl2 13447 |
. . . . . . . . . 10
⊢
((♯‘𝑧)
∈ ℤ → (-1↑(♯‘𝑧)) ∈ {-1, 1}) |
38 | | prcom 4628 |
. . . . . . . . . 10
⊢ {-1, 1} =
{1, -1} |
39 | 37, 38 | eleqtrdi 2900 |
. . . . . . . . 9
⊢
((♯‘𝑧)
∈ ℤ → (-1↑(♯‘𝑧)) ∈ {1, -1}) |
40 | | eleq1a 2885 |
. . . . . . . . 9
⊢
((-1↑(♯‘𝑧)) ∈ {1, -1} → ((𝑁‘𝑥) = (-1↑(♯‘𝑧)) → (𝑁‘𝑥) ∈ {1, -1})) |
41 | 36, 39, 40 | 3syl 18 |
. . . . . . . 8
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
((𝑁‘𝑥) =
(-1↑(♯‘𝑧))
→ (𝑁‘𝑥) ∈ {1,
-1})) |
42 | 41 | adantld 494 |
. . . . . . 7
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1})) |
43 | 42 | rexlimiv 3239 |
. . . . . 6
⊢
(∃𝑧 ∈
Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1}) |
44 | 43 | a1i 11 |
. . . . 5
⊢ (𝐷 ∈ 𝑉 → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1})) |
45 | 34, 44 | syl5 34 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → (𝑥 ∈ dom 𝑁 → (𝑁‘𝑥) ∈ {1, -1})) |
46 | 45 | ralrimiv 3148 |
. . 3
⊢ (𝐷 ∈ 𝑉 → ∀𝑥 ∈ dom 𝑁(𝑁‘𝑥) ∈ {1, -1}) |
47 | | ffnfv 6859 |
. . 3
⊢ (𝑁:dom 𝑁⟶{1, -1} ↔ (𝑁 Fn dom 𝑁 ∧ ∀𝑥 ∈ dom 𝑁(𝑁‘𝑥) ∈ {1, -1})) |
48 | 32, 46, 47 | sylanbrc 586 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝑁:dom 𝑁⟶{1, -1}) |
49 | | ccatcl 13917 |
. . . . . . 7
⊢ ((𝑧 ∈ Word ran
(pmTrsp‘𝐷) ∧
𝑤 ∈ Word ran
(pmTrsp‘𝐷)) →
(𝑧 ++ 𝑤) ∈ Word ran (pmTrsp‘𝐷)) |
50 | 1, 33, 4 | psgnvalii 18629 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ++ 𝑤) ∈ Word ran (pmTrsp‘𝐷)) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (-1↑(♯‘(𝑧 ++ 𝑤)))) |
51 | 49, 50 | sylan2 595 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (-1↑(♯‘(𝑧 ++ 𝑤)))) |
52 | 1 | symggrp 18520 |
. . . . . . . . . 10
⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp) |
53 | | grpmnd 18102 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Grp → 𝑆 ∈ Mnd) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Mnd) |
55 | 33, 1, 2 | symgtrf 18589 |
. . . . . . . . . . 11
⊢ ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆) |
56 | | sswrd 13865 |
. . . . . . . . . . 11
⊢ (ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆) → Word
ran (pmTrsp‘𝐷)
⊆ Word (Base‘𝑆)) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . 10
⊢ Word ran
(pmTrsp‘𝐷) ⊆
Word (Base‘𝑆) |
58 | 57 | sseli 3911 |
. . . . . . . . 9
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
𝑧 ∈ Word
(Base‘𝑆)) |
59 | 57 | sseli 3911 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word ran
(pmTrsp‘𝐷) →
𝑤 ∈ Word
(Base‘𝑆)) |
60 | 2, 14 | gsumccat 17998 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ 𝑧 ∈ Word (Base‘𝑆) ∧ 𝑤 ∈ Word (Base‘𝑆)) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
61 | 54, 58, 59, 60 | syl3an 1157 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷)) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
62 | 61 | 3expb 1117 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
63 | 62 | fveq2d 6649 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤)))) |
64 | | ccatlen 13918 |
. . . . . . . . 9
⊢ ((𝑧 ∈ Word ran
(pmTrsp‘𝐷) ∧
𝑤 ∈ Word ran
(pmTrsp‘𝐷)) →
(♯‘(𝑧 ++ 𝑤)) = ((♯‘𝑧) + (♯‘𝑤))) |
65 | 64 | adantl 485 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (♯‘(𝑧 ++ 𝑤)) = ((♯‘𝑧) + (♯‘𝑤))) |
66 | 65 | oveq2d 7151 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑(♯‘(𝑧
++ 𝑤))) =
(-1↑((♯‘𝑧)
+ (♯‘𝑤)))) |
67 | | neg1cn 11739 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
68 | 67 | a1i 11 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → -1 ∈
ℂ) |
69 | | lencl 13876 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word ran
(pmTrsp‘𝐷) →
(♯‘𝑤) ∈
ℕ0) |
70 | 69 | ad2antll 728 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (♯‘𝑤) ∈
ℕ0) |
71 | 35 | ad2antrl 727 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (♯‘𝑧) ∈
ℕ0) |
72 | 68, 70, 71 | expaddd 13508 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑((♯‘𝑧)
+ (♯‘𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤)))) |
73 | 66, 72 | eqtrd 2833 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑(♯‘(𝑧
++ 𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤)))) |
74 | 51, 63, 73 | 3eqtr3d 2841 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤)))) |
75 | | oveq12 7144 |
. . . . . . . 8
⊢ ((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) → (𝑥(+g‘𝑆)𝑦) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
76 | 75 | fveq2d 6649 |
. . . . . . 7
⊢ ((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤)))) |
77 | | oveq12 7144 |
. . . . . . 7
⊢ (((𝑁‘𝑥) = (-1↑(♯‘𝑧)) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤))) → ((𝑁‘𝑥) · (𝑁‘𝑦)) = ((-1↑(♯‘𝑧)) ·
(-1↑(♯‘𝑤)))) |
78 | 76, 77 | eqeqan12d 2815 |
. . . . . 6
⊢ (((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) ∧ ((𝑁‘𝑥) = (-1↑(♯‘𝑧)) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) → ((𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)) ↔ (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤))))) |
79 | 78 | an4s 659 |
. . . . 5
⊢ (((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) → ((𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)) ↔ (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤))))) |
80 | 74, 79 | syl5ibrcom 250 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)))) |
81 | 80 | rexlimdvva 3253 |
. . 3
⊢ (𝐷 ∈ 𝑉 → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)))) |
82 | 1, 33, 4 | psgnvali 18628 |
. . . . 5
⊢ (𝑦 ∈ dom 𝑁 → ∃𝑤 ∈ Word ran (pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) |
83 | 34, 82 | anim12i 615 |
. . . 4
⊢ ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ ∃𝑤 ∈ Word ran
(pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤))))) |
84 | | reeanv 3320 |
. . . 4
⊢
(∃𝑧 ∈
Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) ↔ (∃𝑧 ∈ Word ran
(pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ ∃𝑤 ∈ Word ran
(pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤))))) |
85 | 83, 84 | sylibr 237 |
. . 3
⊢ ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → ∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤))))) |
86 | 81, 85 | impel 509 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁)) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦))) |
87 | 10, 12, 16, 22, 25, 27, 48, 86 | isghmd 18359 |
1
⊢ (𝐷 ∈ 𝑉 → 𝑁 ∈ (𝐹 GrpHom 𝑈)) |