Step | Hyp | Ref
| Expression |
1 | | psgnghm.s |
. . . . . 6
⊢ 𝑆 = (SymGrp‘𝐷) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2622 |
. . . . . 6
⊢ {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} =
{𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈
Fin} |
4 | | psgnghm.n |
. . . . . 6
⊢ 𝑁 = (pmSgn‘𝐷) |
5 | 1, 2, 3, 4 | psgnfn 17921 |
. . . . 5
⊢ 𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} |
6 | | fndm 5990 |
. . . . 5
⊢ (𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} → dom 𝑁 = {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin}) |
7 | 5, 6 | ax-mp 5 |
. . . 4
⊢ dom 𝑁 = {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} |
8 | | ssrab2 3687 |
. . . 4
⊢ {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} ⊆
(Base‘𝑆) |
9 | 7, 8 | eqsstri 3635 |
. . 3
⊢ dom 𝑁 ⊆ (Base‘𝑆) |
10 | | psgnghm.f |
. . . 4
⊢ 𝐹 = (𝑆 ↾s dom 𝑁) |
11 | 10, 2 | ressbas2 15931 |
. . 3
⊢ (dom
𝑁 ⊆ (Base‘𝑆) → dom 𝑁 = (Base‘𝐹)) |
12 | 9, 11 | ax-mp 5 |
. 2
⊢ dom 𝑁 = (Base‘𝐹) |
13 | | psgnghm.u |
. . 3
⊢ 𝑈 =
((mulGrp‘ℂfld) ↾s {1,
-1}) |
14 | 13 | cnmsgnbas 19924 |
. 2
⊢ {1, -1} =
(Base‘𝑈) |
15 | | fvex 6201 |
. . . 4
⊢
(Base‘𝐹)
∈ V |
16 | 12, 15 | eqeltri 2697 |
. . 3
⊢ dom 𝑁 ∈ V |
17 | | eqid 2622 |
. . . 4
⊢
(+g‘𝑆) = (+g‘𝑆) |
18 | 10, 17 | ressplusg 15993 |
. . 3
⊢ (dom
𝑁 ∈ V →
(+g‘𝑆) =
(+g‘𝐹)) |
19 | 16, 18 | ax-mp 5 |
. 2
⊢
(+g‘𝑆) = (+g‘𝐹) |
20 | | prex 4909 |
. . 3
⊢ {1, -1}
∈ V |
21 | | eqid 2622 |
. . . . 5
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
22 | | cnfldmul 19752 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
23 | 21, 22 | mgpplusg 18493 |
. . . 4
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
24 | 13, 23 | ressplusg 15993 |
. . 3
⊢ ({1, -1}
∈ V → · = (+g‘𝑈)) |
25 | 20, 24 | ax-mp 5 |
. 2
⊢ ·
= (+g‘𝑈) |
26 | 1, 4 | psgndmsubg 17922 |
. . 3
⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝑆)) |
27 | 10 | subggrp 17597 |
. . 3
⊢ (dom
𝑁 ∈
(SubGrp‘𝑆) →
𝐹 ∈
Grp) |
28 | 26, 27 | syl 17 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝐹 ∈ Grp) |
29 | 13 | cnmsgngrp 19925 |
. . 3
⊢ 𝑈 ∈ Grp |
30 | 29 | a1i 11 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝑈 ∈ Grp) |
31 | | fnfun 5988 |
. . . . . 6
⊢ (𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} → Fun 𝑁) |
32 | 5, 31 | ax-mp 5 |
. . . . 5
⊢ Fun 𝑁 |
33 | | funfn 5918 |
. . . . 5
⊢ (Fun
𝑁 ↔ 𝑁 Fn dom 𝑁) |
34 | 32, 33 | mpbi 220 |
. . . 4
⊢ 𝑁 Fn dom 𝑁 |
35 | 34 | a1i 11 |
. . 3
⊢ (𝐷 ∈ 𝑉 → 𝑁 Fn dom 𝑁) |
36 | | eqid 2622 |
. . . . . 6
⊢ ran
(pmTrsp‘𝐷) = ran
(pmTrsp‘𝐷) |
37 | 1, 36, 4 | psgnvali 17928 |
. . . . 5
⊢ (𝑥 ∈ dom 𝑁 → ∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧)))) |
38 | | lencl 13324 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
(#‘𝑧) ∈
ℕ0) |
39 | 38 | nn0zd 11480 |
. . . . . . . . . 10
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
(#‘𝑧) ∈
ℤ) |
40 | | m1expcl2 12882 |
. . . . . . . . . . 11
⊢
((#‘𝑧) ∈
ℤ → (-1↑(#‘𝑧)) ∈ {-1, 1}) |
41 | | prcom 4267 |
. . . . . . . . . . 11
⊢ {-1, 1} =
{1, -1} |
42 | 40, 41 | syl6eleq 2711 |
. . . . . . . . . 10
⊢
((#‘𝑧) ∈
ℤ → (-1↑(#‘𝑧)) ∈ {1, -1}) |
43 | 39, 42 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
(-1↑(#‘𝑧))
∈ {1, -1}) |
44 | 43 | adantl 482 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷)) →
(-1↑(#‘𝑧))
∈ {1, -1}) |
45 | | eleq1a 2696 |
. . . . . . . 8
⊢
((-1↑(#‘𝑧)) ∈ {1, -1} → ((𝑁‘𝑥) = (-1↑(#‘𝑧)) → (𝑁‘𝑥) ∈ {1, -1})) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷)) → ((𝑁‘𝑥) = (-1↑(#‘𝑧)) → (𝑁‘𝑥) ∈ {1, -1})) |
47 | 46 | adantld 483 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷)) → ((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1})) |
48 | 47 | rexlimdva 3031 |
. . . . 5
⊢ (𝐷 ∈ 𝑉 → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1})) |
49 | 37, 48 | syl5 34 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → (𝑥 ∈ dom 𝑁 → (𝑁‘𝑥) ∈ {1, -1})) |
50 | 49 | ralrimiv 2965 |
. . 3
⊢ (𝐷 ∈ 𝑉 → ∀𝑥 ∈ dom 𝑁(𝑁‘𝑥) ∈ {1, -1}) |
51 | | ffnfv 6388 |
. . 3
⊢ (𝑁:dom 𝑁⟶{1, -1} ↔ (𝑁 Fn dom 𝑁 ∧ ∀𝑥 ∈ dom 𝑁(𝑁‘𝑥) ∈ {1, -1})) |
52 | 35, 50, 51 | sylanbrc 698 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝑁:dom 𝑁⟶{1, -1}) |
53 | 1, 36, 4 | psgnvali 17928 |
. . . . . 6
⊢ (𝑦 ∈ dom 𝑁 → ∃𝑤 ∈ Word ran (pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) |
54 | 37, 53 | anim12i 590 |
. . . . 5
⊢ ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ ∃𝑤 ∈ Word ran (pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤))))) |
55 | | reeanv 3107 |
. . . . 5
⊢
(∃𝑧 ∈
Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) ↔ (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ ∃𝑤 ∈ Word ran (pmTrsp‘𝐷)(𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤))))) |
56 | 54, 55 | sylibr 224 |
. . . 4
⊢ ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → ∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤))))) |
57 | | ccatcl 13359 |
. . . . . . . 8
⊢ ((𝑧 ∈ Word ran
(pmTrsp‘𝐷) ∧
𝑤 ∈ Word ran
(pmTrsp‘𝐷)) →
(𝑧 ++ 𝑤) ∈ Word ran (pmTrsp‘𝐷)) |
58 | 1, 36, 4 | psgnvalii 17929 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ++ 𝑤) ∈ Word ran (pmTrsp‘𝐷)) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (-1↑(#‘(𝑧 ++ 𝑤)))) |
59 | 57, 58 | sylan2 491 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (-1↑(#‘(𝑧 ++ 𝑤)))) |
60 | 1 | symggrp 17820 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp) |
61 | | grpmnd 17429 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Grp → 𝑆 ∈ Mnd) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Mnd) |
63 | 36, 1, 2 | symgtrf 17889 |
. . . . . . . . . . . 12
⊢ ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆) |
64 | | sswrd 13313 |
. . . . . . . . . . . 12
⊢ (ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆) → Word
ran (pmTrsp‘𝐷)
⊆ Word (Base‘𝑆)) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Word ran
(pmTrsp‘𝐷) ⊆
Word (Base‘𝑆) |
66 | 65 | sseli 3599 |
. . . . . . . . . 10
⊢ (𝑧 ∈ Word ran
(pmTrsp‘𝐷) →
𝑧 ∈ Word
(Base‘𝑆)) |
67 | 65 | sseli 3599 |
. . . . . . . . . 10
⊢ (𝑤 ∈ Word ran
(pmTrsp‘𝐷) →
𝑤 ∈ Word
(Base‘𝑆)) |
68 | 2, 17 | gsumccat 17378 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Mnd ∧ 𝑧 ∈ Word (Base‘𝑆) ∧ 𝑤 ∈ Word (Base‘𝑆)) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
69 | 62, 66, 67, 68 | syl3an 1368 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷)) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
70 | 69 | 3expb 1266 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑆 Σg (𝑧 ++ 𝑤)) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
71 | 70 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘(𝑆 Σg (𝑧 ++ 𝑤))) = (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤)))) |
72 | | ccatlen 13360 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ Word ran
(pmTrsp‘𝐷) ∧
𝑤 ∈ Word ran
(pmTrsp‘𝐷)) →
(#‘(𝑧 ++ 𝑤)) = ((#‘𝑧) + (#‘𝑤))) |
73 | 72 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (#‘(𝑧 ++ 𝑤)) = ((#‘𝑧) + (#‘𝑤))) |
74 | 73 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑(#‘(𝑧 ++
𝑤))) =
(-1↑((#‘𝑧) +
(#‘𝑤)))) |
75 | | neg1cn 11124 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
76 | 75 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → -1 ∈
ℂ) |
77 | | lencl 13324 |
. . . . . . . . . 10
⊢ (𝑤 ∈ Word ran
(pmTrsp‘𝐷) →
(#‘𝑤) ∈
ℕ0) |
78 | 77 | ad2antll 765 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (#‘𝑤) ∈
ℕ0) |
79 | 38 | ad2antrl 764 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (#‘𝑧) ∈
ℕ0) |
80 | 76, 78, 79 | expaddd 13010 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑((#‘𝑧) +
(#‘𝑤))) =
((-1↑(#‘𝑧))
· (-1↑(#‘𝑤)))) |
81 | 74, 80 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) →
(-1↑(#‘(𝑧 ++
𝑤))) =
((-1↑(#‘𝑧))
· (-1↑(#‘𝑤)))) |
82 | 59, 71, 81 | 3eqtr3d 2664 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) = ((-1↑(#‘𝑧)) ·
(-1↑(#‘𝑤)))) |
83 | | oveq12 6659 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) → (𝑥(+g‘𝑆)𝑦) = ((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) |
84 | 83 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤)))) |
85 | | oveq12 6659 |
. . . . . . . 8
⊢ (((𝑁‘𝑥) = (-1↑(#‘𝑧)) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤))) → ((𝑁‘𝑥) · (𝑁‘𝑦)) = ((-1↑(#‘𝑧)) · (-1↑(#‘𝑤)))) |
86 | 84, 85 | eqeqan12d 2638 |
. . . . . . 7
⊢ (((𝑥 = (𝑆 Σg 𝑧) ∧ 𝑦 = (𝑆 Σg 𝑤)) ∧ ((𝑁‘𝑥) = (-1↑(#‘𝑧)) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) → ((𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)) ↔ (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) = ((-1↑(#‘𝑧)) ·
(-1↑(#‘𝑤))))) |
87 | 86 | an4s 869 |
. . . . . 6
⊢ (((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) → ((𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)) ↔ (𝑁‘((𝑆 Σg 𝑧)(+g‘𝑆)(𝑆 Σg 𝑤))) = ((-1↑(#‘𝑧)) ·
(-1↑(#‘𝑤))))) |
88 | 82, 87 | syl5ibrcom 237 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)))) |
89 | 88 | rexlimdvva 3038 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σg 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σg 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)))) |
90 | 56, 89 | syl5 34 |
. . 3
⊢ (𝐷 ∈ 𝑉 → ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)))) |
91 | 90 | imp 445 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁)) → (𝑁‘(𝑥(+g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦))) |
92 | 12, 14, 19, 25, 28, 30, 52, 91 | isghmd 17669 |
1
⊢ (𝐷 ∈ 𝑉 → 𝑁 ∈ (𝐹 GrpHom 𝑈)) |