Step | Hyp | Ref
| Expression |
1 | | psgnghm.s |
. . . . . 6
⊢ 𝑆 = (SymGrp‘𝐷) |
2 | | eqid 2823 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2823 |
. . . . . 6
⊢ {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} =
{𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈
Fin} |
4 | | psgnghm.n |
. . . . . 6
⊢ 𝑁 = (pmSgn‘𝐷) |
5 | 1, 2, 3, 4 | psgnfn 18631 |
. . . . 5
⊢ 𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} |
6 | | fndm 6457 |
. . . . 5
⊢ (𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} → dom 𝑁 = {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin}) |
7 | 5, 6 | ax-mp 5 |
. . . 4
⊢ dom 𝑁 = {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} |
8 | 7 | ssrab3 4059 |
. . 3
⊢ dom 𝑁 ⊆ (Base‘𝑆) |
9 | | psgnghm.f |
. . . 4
⊢ 𝐹 = (𝑆 ↾s dom 𝑁) |
10 | 9, 2 | ressbas2 16557 |
. . 3
⊢ (dom
𝑁 ⊆ (Base‘𝑆) → dom 𝑁 = (Base‘𝐹)) |
11 | 8, 10 | ax-mp 5 |
. 2
⊢ dom 𝑁 = (Base‘𝐹) |
12 | | psgnghm.u |
. . 3
⊢ 𝑈 =
((mulGrp‘ℂfld) ↾s {1,
-1}) |
13 | 12 | cnmsgnbas 20724 |
. 2
⊢ {1, -1} =
(Base‘𝑈) |
14 | 11 | fvexi 6686 |
. . 3
⊢ dom 𝑁 ∈ V |
15 | | eqid 2823 |
. . . 4
⊢
(+g‘𝑆) = (+g‘𝑆) |
16 | 9, 15 | ressplusg 16614 |
. . 3
⊢ (dom
𝑁 ∈ V →
(+g‘𝑆) =
(+g‘𝐹)) |
17 | 14, 16 | ax-mp 5 |
. 2
⊢
(+g‘𝑆) = (+g‘𝐹) |
18 | | prex 5335 |
. . 3
⊢ {1, -1}
∈ V |
19 | | eqid 2823 |
. . . . 5
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
20 | | cnfldmul 20553 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
21 | 19, 20 | mgpplusg 19245 |
. . . 4
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
22 | 12, 21 | ressplusg 16614 |
. . 3
⊢ ({1, -1}
∈ V → · = (+g‘𝑈)) |
23 | 18, 22 | ax-mp 5 |
. 2
⊢ ·
= (+g‘𝑈) |
24 | 1, 4 | psgndmsubg 18632 |
. . 3
⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝑆)) |
25 | 9 | subggrp 18284 |
. . 3
⊢ (dom
𝑁 ∈
(SubGrp‘𝑆) →
𝐹 ∈
Grp) |
26 | 24, 25 | syl 17 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝐹 ∈ Grp) |
27 | 12 | cnmsgngrp 20725 |
. . 3
⊢ 𝑈 ∈ Grp |
28 | 27 | a1i 11 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝑈 ∈ Grp) |
29 | | fnfun 6455 |
. . . . . 6
⊢ (𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} → Fun 𝑁) |
30 | 5, 29 | ax-mp 5 |
. . . . 5
⊢ Fun 𝑁 |
31 | | funfn 6387 |
. . . . 5
⊢ (Fun
𝑁 ↔ 𝑁 Fn dom 𝑁) |
32 | 30, 31 | mpbi 232 |
. . . 4
⊢ 𝑁 Fn dom 𝑁 |
33 | 32 | a1i 11 |
. . 3
⊢ (𝐷 ∈ 𝑉 → 𝑁 Fn dom 𝑁) |
34 | | eqid 2823 |
. . . . . 6
⊢ ran
(pmTrsp‘𝐷) = ran
(pmTrsp‘𝐷) |
35 | 1, 34, 4 | psgnvali 18638 |
. . . . 5
⊢ (𝑥 ∈ dom 𝑁 → ∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧)))) |
36 | | lencl 13885 |
. . . . . . . . . 10
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
(♯‘𝑧) ∈
ℕ0) |
37 | 36 | nn0zd 12088 |
. . . . . . . . 9
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
(♯‘𝑧) ∈
ℤ) |
38 | | m1expcl2 13454 |
. . . . . . . . . 10
⊢
((♯‘𝑧)
∈ ℤ → (-1↑(♯‘𝑧)) ∈ {-1, 1}) |
39 | | prcom 4670 |
. . . . . . . . . 10
⊢ {-1, 1} =
{1, -1} |
40 | 38, 39 | eleqtrdi 2925 |
. . . . . . . . 9
⊢
((♯‘𝑧)
∈ ℤ → (-1↑(♯‘𝑧)) ∈ {1, -1}) |
41 | | eleq1a 2910 |
. . . . . . . . 9
⊢
((-1↑(♯‘𝑧)) ∈ {1, -1} → ((𝑁‘𝑥) = (-1↑(♯‘𝑧)) → (𝑁‘𝑥) ∈ {1, -1})) |
42 | 37, 40, 41 | 3syl 18 |
. . . . . . . 8
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
((𝑁‘𝑥) =
(-1↑(♯‘𝑧))
→ (𝑁‘𝑥) ∈ {1,
-1})) |
43 | 42 | adantld 493 |
. . . . . . 7
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1})) |
44 | 43 | rexlimiv 3282 |
. . . . . 6
⊢
(∃𝑧 ∈
Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1}) |
45 | 44 | a1i 11 |
. . . . 5
⊢ (𝐷 ∈ 𝑉 → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1})) |
46 | 35, 45 | syl5 34 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → (𝑥 ∈ dom 𝑁 → (𝑁‘𝑥) ∈ {1, -1})) |
47 | 46 | ralrimiv 3183 |
. . 3
⊢ (𝐷 ∈ 𝑉 → ∀𝑥 ∈ dom 𝑁(𝑁‘𝑥) ∈ {1, -1}) |
48 | | ffnfv 6884 |
. . 3
⊢ (𝑁:dom 𝑁⟶{1, -1} ↔ (𝑁 Fn dom 𝑁 ∧ ∀𝑥 ∈ dom 𝑁(𝑁‘𝑥) ∈ {1, -1})) |
49 | 33, 47, 48 | sylanbrc 585 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝑁:dom 𝑁⟶{1, -1}) |
50 | | ccatcl 13928 |
. . . . . . 7
⊢ ((𝑧 ∈ Word ran
(pmTrsp‘𝐷) ∧
𝑤 ∈ Word ran
(pmTrsp‘𝐷)) →
(𝑧 ++ 𝑤) ∈ Word ran (pmTrsp‘𝐷)) |
51 | 1, 34, 4 | psgnvalii 18639 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ++ 𝑤) ∈ Word ran (pmTrsp‘𝐷)) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (-1↑(♯‘(𝑧 ++ 𝑤)))) |
52 | 50, 51 | sylan2 594 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (-1↑(♯‘(𝑧 ++ 𝑤)))) |
53 | 1 | symggrp 18530 |
. . . . . . . . . 10
⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp) |
54 | | grpmnd 18112 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Grp → 𝑆 ∈ Mnd) |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Mnd) |
56 | 34, 1, 2 | symgtrf 18599 |
. . . . . . . . . . 11
⊢ ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆) |
57 | | sswrd 13872 |
. . . . . . . . . . 11
⊢ (ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆) → Word
ran (pmTrsp‘𝐷)
⊆ Word (Base‘𝑆)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . 10
⊢ Word ran
(pmTrsp‘𝐷) ⊆
Word (Base‘𝑆) |
59 | 58 | sseli 3965 |
. . . . . . . . 9
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
𝑧 ∈ Word
(Base‘𝑆)) |
60 | 58 | sseli 3965 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word ran
(pmTrsp‘𝐷) →
𝑤 ∈ Word
(Base‘𝑆)) |
61 | 2, 15 | gsumccat 18008 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ 𝑧 ∈ Word (Base‘𝑆) ∧ 𝑤 ∈ Word (Base‘𝑆)) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
62 | 55, 59, 60, 61 | syl3an 1156 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷)) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
63 | 62 | 3expb 1116 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
64 | 63 | fveq2d 6676 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤)))) |
65 | | ccatlen 13929 |
. . . . . . . . 9
⊢ ((𝑧 ∈ Word ran
(pmTrsp‘𝐷) ∧
𝑤 ∈ Word ran
(pmTrsp‘𝐷)) →
(♯‘(𝑧 ++ 𝑤)) = ((♯‘𝑧) + (♯‘𝑤))) |
66 | 65 | adantl 484 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (♯‘(𝑧 ++ 𝑤)) = ((♯‘𝑧) + (♯‘𝑤))) |
67 | 66 | oveq2d 7174 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑(♯‘(𝑧
++ 𝑤))) =
(-1↑((♯‘𝑧)
+ (♯‘𝑤)))) |
68 | | neg1cn 11754 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
69 | 68 | a1i 11 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → -1 ∈
ℂ) |
70 | | lencl 13885 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word ran
(pmTrsp‘𝐷) →
(♯‘𝑤) ∈
ℕ0) |
71 | 70 | ad2antll 727 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (♯‘𝑤) ∈
ℕ0) |
72 | 36 | ad2antrl 726 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (♯‘𝑧) ∈
ℕ0) |
73 | 69, 71, 72 | expaddd 13515 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑((♯‘𝑧)
+ (♯‘𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤)))) |
74 | 67, 73 | eqtrd 2858 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑(♯‘(𝑧
++ 𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤)))) |
75 | 52, 64, 74 | 3eqtr3d 2866 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤)))) |
76 | | oveq12 7167 |
. . . . . . . 8
⊢ ((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) → (𝑥(+g‘𝑆)𝑦) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
77 | 76 | fveq2d 6676 |
. . . . . . 7
⊢ ((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤)))) |
78 | | oveq12 7167 |
. . . . . . 7
⊢ (((𝑁‘𝑥) = (-1↑(♯‘𝑧)) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤))) → ((𝑁‘𝑥) · (𝑁‘𝑦)) = ((-1↑(♯‘𝑧)) ·
(-1↑(♯‘𝑤)))) |
79 | 77, 78 | eqeqan12d 2840 |
. . . . . 6
⊢ (((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) ∧ ((𝑁‘𝑥) = (-1↑(♯‘𝑧)) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) → ((𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)) ↔ (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤))))) |
80 | 79 | an4s 658 |
. . . . 5
⊢ (((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) → ((𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)) ↔ (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) =
((-1↑(♯‘𝑧)) · (-1↑(♯‘𝑤))))) |
81 | 75, 80 | syl5ibrcom 249 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)))) |
82 | 81 | rexlimdvva 3296 |
. . 3
⊢ (𝐷 ∈ 𝑉 → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)))) |
83 | 1, 34, 4 | psgnvali 18638 |
. . . . 5
⊢ (𝑦 ∈ dom 𝑁 → ∃𝑤 ∈ Word ran (pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) |
84 | 35, 83 | anim12i 614 |
. . . 4
⊢ ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ ∃𝑤 ∈ Word ran
(pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤))))) |
85 | | reeanv 3369 |
. . . 4
⊢
(∃𝑧 ∈
Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤)))) ↔ (∃𝑧 ∈ Word ran
(pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ ∃𝑤 ∈ Word ran
(pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤))))) |
86 | 84, 85 | sylibr 236 |
. . 3
⊢ ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → ∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(♯‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(♯‘𝑤))))) |
87 | 82, 86 | impel 508 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁)) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦))) |
88 | 11, 13, 17, 23, 26, 28, 49, 87 | isghmd 18369 |
1
⊢ (𝐷 ∈ 𝑉 → 𝑁 ∈ (𝐹 GrpHom 𝑈)) |