Step | Hyp | Ref
| Expression |
1 | | psgnghm.s |
. . . . . 6
โข ๐ = (SymGrpโ๐ท) |
2 | | eqid 2737 |
. . . . . 6
โข
(Baseโ๐) =
(Baseโ๐) |
3 | | eqid 2737 |
. . . . . 6
โข {๐ฅ โ (Baseโ๐) โฃ dom (๐ฅ โ I ) โ Fin} =
{๐ฅ โ (Baseโ๐) โฃ dom (๐ฅ โ I ) โ
Fin} |
4 | | psgnghm.n |
. . . . . 6
โข ๐ = (pmSgnโ๐ท) |
5 | 1, 2, 3, 4 | psgnfn 19284 |
. . . . 5
โข ๐ Fn {๐ฅ โ (Baseโ๐) โฃ dom (๐ฅ โ I ) โ Fin} |
6 | 5 | fndmi 6607 |
. . . 4
โข dom ๐ = {๐ฅ โ (Baseโ๐) โฃ dom (๐ฅ โ I ) โ Fin} |
7 | 6 | ssrab3 4041 |
. . 3
โข dom ๐ โ (Baseโ๐) |
8 | | psgnghm.f |
. . . 4
โข ๐น = (๐ โพs dom ๐) |
9 | 8, 2 | ressbas2 17121 |
. . 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 20985 |
. 2
โข {1, -1} =
(Baseโ๐) |
13 | 10 | fvexi 6857 |
. . 3
โข dom ๐ โ V |
14 | | eqid 2737 |
. . . 4
โข
(+gโ๐) = (+gโ๐) |
15 | 8, 14 | ressplusg 17172 |
. . 3
โข (dom
๐ โ V โ
(+gโ๐) =
(+gโ๐น)) |
16 | 13, 15 | ax-mp 5 |
. 2
โข
(+gโ๐) = (+gโ๐น) |
17 | | prex 5390 |
. . 3
โข {1, -1}
โ V |
18 | | eqid 2737 |
. . . . 5
โข
(mulGrpโโfld) =
(mulGrpโโfld) |
19 | | cnfldmul 20805 |
. . . . 5
โข ยท
= (.rโโfld) |
20 | 18, 19 | mgpplusg 19901 |
. . . 4
โข ยท
= (+gโ(mulGrpโโfld)) |
21 | 11, 20 | ressplusg 17172 |
. . 3
โข ({1, -1}
โ V โ ยท = (+gโ๐)) |
22 | 17, 21 | ax-mp 5 |
. 2
โข ยท
= (+gโ๐) |
23 | 1, 4 | psgndmsubg 19285 |
. . 3
โข (๐ท โ ๐ โ dom ๐ โ (SubGrpโ๐)) |
24 | 8 | subggrp 18932 |
. . 3
โข (dom
๐ โ
(SubGrpโ๐) โ
๐น โ
Grp) |
25 | 23, 24 | syl 17 |
. 2
โข (๐ท โ ๐ โ ๐น โ Grp) |
26 | 11 | cnmsgngrp 20986 |
. . 3
โข ๐ โ Grp |
27 | 26 | a1i 11 |
. 2
โข (๐ท โ ๐ โ ๐ โ Grp) |
28 | | fnfun 6603 |
. . . . . 6
โข (๐ Fn {๐ฅ โ (Baseโ๐) โฃ dom (๐ฅ โ I ) โ Fin} โ Fun ๐) |
29 | 5, 28 | ax-mp 5 |
. . . . 5
โข Fun ๐ |
30 | | funfn 6532 |
. . . . 5
โข (Fun
๐ โ ๐ Fn dom ๐) |
31 | 29, 30 | mpbi 229 |
. . . 4
โข ๐ Fn dom ๐ |
32 | 31 | a1i 11 |
. . 3
โข (๐ท โ ๐ โ ๐ Fn dom ๐) |
33 | | eqid 2737 |
. . . . . 6
โข ran
(pmTrspโ๐ท) = ran
(pmTrspโ๐ท) |
34 | 1, 33, 4 | psgnvali 19291 |
. . . . 5
โข (๐ฅ โ dom ๐ โ โ๐ง โ Word ran (pmTrspโ๐ท)(๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง)))) |
35 | | lencl 14422 |
. . . . . . . . . 10
โข (๐ง โ Word ran
(pmTrspโ๐ท) โ
(โฏโ๐ง) โ
โ0) |
36 | 35 | nn0zd 12526 |
. . . . . . . . 9
โข (๐ง โ Word ran
(pmTrspโ๐ท) โ
(โฏโ๐ง) โ
โค) |
37 | | m1expcl2 13992 |
. . . . . . . . . 10
โข
((โฏโ๐ง)
โ โค โ (-1โ(โฏโ๐ง)) โ {-1, 1}) |
38 | | prcom 4694 |
. . . . . . . . . 10
โข {-1, 1} =
{1, -1} |
39 | 37, 38 | eleqtrdi 2848 |
. . . . . . . . 9
โข
((โฏโ๐ง)
โ โค โ (-1โ(โฏโ๐ง)) โ {1, -1}) |
40 | | eleq1a 2833 |
. . . . . . . . 9
โข
((-1โ(โฏโ๐ง)) โ {1, -1} โ ((๐โ๐ฅ) = (-1โ(โฏโ๐ง)) โ (๐โ๐ฅ) โ {1, -1})) |
41 | 36, 39, 40 | 3syl 18 |
. . . . . . . 8
โข (๐ง โ Word ran
(pmTrspโ๐ท) โ
((๐โ๐ฅ) =
(-1โ(โฏโ๐ง))
โ (๐โ๐ฅ) โ {1,
-1})) |
42 | 41 | adantld 492 |
. . . . . . 7
โข (๐ง โ Word ran
(pmTrspโ๐ท) โ
((๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง))) โ (๐โ๐ฅ) โ {1, -1})) |
43 | 42 | rexlimiv 3146 |
. . . . . 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 3143 |
. . 3
โข (๐ท โ ๐ โ โ๐ฅ โ dom ๐(๐โ๐ฅ) โ {1, -1}) |
47 | | ffnfv 7067 |
. . 3
โข (๐:dom ๐โถ{1, -1} โ (๐ Fn dom ๐ โง โ๐ฅ โ dom ๐(๐โ๐ฅ) โ {1, -1})) |
48 | 32, 46, 47 | sylanbrc 584 |
. 2
โข (๐ท โ ๐ โ ๐:dom ๐โถ{1, -1}) |
49 | | ccatcl 14463 |
. . . . . . 7
โข ((๐ง โ Word ran
(pmTrspโ๐ท) โง
๐ค โ Word ran
(pmTrspโ๐ท)) โ
(๐ง ++ ๐ค) โ Word ran (pmTrspโ๐ท)) |
50 | 1, 33, 4 | psgnvalii 19292 |
. . . . . . 7
โข ((๐ท โ ๐ โง (๐ง ++ ๐ค) โ Word ran (pmTrspโ๐ท)) โ (๐โ(๐ ฮฃg (๐ง ++ ๐ค))) = (-1โ(โฏโ(๐ง ++ ๐ค)))) |
51 | 49, 50 | sylan2 594 |
. . . . . 6
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ (๐โ(๐ ฮฃg (๐ง ++ ๐ค))) = (-1โ(โฏโ(๐ง ++ ๐ค)))) |
52 | 1 | symggrp 19183 |
. . . . . . . . . 10
โข (๐ท โ ๐ โ ๐ โ Grp) |
53 | 52 | grpmndd 18761 |
. . . . . . . . 9
โข (๐ท โ ๐ โ ๐ โ Mnd) |
54 | 33, 1, 2 | symgtrf 19252 |
. . . . . . . . . . 11
โข ran
(pmTrspโ๐ท) โ
(Baseโ๐) |
55 | | sswrd 14411 |
. . . . . . . . . . 11
โข (ran
(pmTrspโ๐ท) โ
(Baseโ๐) โ Word
ran (pmTrspโ๐ท)
โ Word (Baseโ๐)) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . 10
โข Word ran
(pmTrspโ๐ท) โ
Word (Baseโ๐) |
57 | 56 | sseli 3941 |
. . . . . . . . 9
โข (๐ง โ Word ran
(pmTrspโ๐ท) โ
๐ง โ Word
(Baseโ๐)) |
58 | 56 | sseli 3941 |
. . . . . . . . 9
โข (๐ค โ Word ran
(pmTrspโ๐ท) โ
๐ค โ Word
(Baseโ๐)) |
59 | 2, 14 | gsumccat 18652 |
. . . . . . . . 9
โข ((๐ โ Mnd โง ๐ง โ Word (Baseโ๐) โง ๐ค โ Word (Baseโ๐)) โ (๐ ฮฃg (๐ง ++ ๐ค)) = ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค))) |
60 | 53, 57, 58, 59 | syl3an 1161 |
. . . . . . . 8
โข ((๐ท โ ๐ โง ๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท)) โ (๐ ฮฃg (๐ง ++ ๐ค)) = ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค))) |
61 | 60 | 3expb 1121 |
. . . . . . 7
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ (๐ ฮฃg (๐ง ++ ๐ค)) = ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค))) |
62 | 61 | fveq2d 6847 |
. . . . . 6
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ (๐โ(๐ ฮฃg (๐ง ++ ๐ค))) = (๐โ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค)))) |
63 | | ccatlen 14464 |
. . . . . . . . 9
โข ((๐ง โ Word ran
(pmTrspโ๐ท) โง
๐ค โ Word ran
(pmTrspโ๐ท)) โ
(โฏโ(๐ง ++ ๐ค)) = ((โฏโ๐ง) + (โฏโ๐ค))) |
64 | 63 | adantl 483 |
. . . . . . . 8
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ (โฏโ(๐ง ++ ๐ค)) = ((โฏโ๐ง) + (โฏโ๐ค))) |
65 | 64 | oveq2d 7374 |
. . . . . . 7
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ
(-1โ(โฏโ(๐ง
++ ๐ค))) =
(-1โ((โฏโ๐ง)
+ (โฏโ๐ค)))) |
66 | | neg1cn 12268 |
. . . . . . . . 9
โข -1 โ
โ |
67 | 66 | a1i 11 |
. . . . . . . 8
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ -1 โ
โ) |
68 | | lencl 14422 |
. . . . . . . . 9
โข (๐ค โ Word ran
(pmTrspโ๐ท) โ
(โฏโ๐ค) โ
โ0) |
69 | 68 | ad2antll 728 |
. . . . . . . 8
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ (โฏโ๐ค) โ
โ0) |
70 | 35 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ (โฏโ๐ง) โ
โ0) |
71 | 67, 69, 70 | expaddd 14054 |
. . . . . . 7
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ
(-1โ((โฏโ๐ง)
+ (โฏโ๐ค))) =
((-1โ(โฏโ๐ง)) ยท (-1โ(โฏโ๐ค)))) |
72 | 65, 71 | eqtrd 2777 |
. . . . . 6
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ
(-1โ(โฏโ(๐ง
++ ๐ค))) =
((-1โ(โฏโ๐ง)) ยท (-1โ(โฏโ๐ค)))) |
73 | 51, 62, 72 | 3eqtr3d 2785 |
. . . . 5
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ (๐โ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค))) =
((-1โ(โฏโ๐ง)) ยท (-1โ(โฏโ๐ค)))) |
74 | | oveq12 7367 |
. . . . . . . 8
โข ((๐ฅ = (๐ ฮฃg ๐ง) โง ๐ฆ = (๐ ฮฃg ๐ค)) โ (๐ฅ(+gโ๐)๐ฆ) = ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค))) |
75 | 74 | fveq2d 6847 |
. . . . . . 7
โข ((๐ฅ = (๐ ฮฃg ๐ง) โง ๐ฆ = (๐ ฮฃg ๐ค)) โ (๐โ(๐ฅ(+gโ๐)๐ฆ)) = (๐โ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค)))) |
76 | | oveq12 7367 |
. . . . . . 7
โข (((๐โ๐ฅ) = (-1โ(โฏโ๐ง)) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค))) โ ((๐โ๐ฅ) ยท (๐โ๐ฆ)) = ((-1โ(โฏโ๐ง)) ยท
(-1โ(โฏโ๐ค)))) |
77 | 75, 76 | eqeqan12d 2751 |
. . . . . 6
โข (((๐ฅ = (๐ ฮฃg ๐ง) โง ๐ฆ = (๐ ฮฃg ๐ค)) โง ((๐โ๐ฅ) = (-1โ(โฏโ๐ง)) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค)))) โ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โ (๐โ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค))) =
((-1โ(โฏโ๐ง)) ยท (-1โ(โฏโ๐ค))))) |
78 | 77 | an4s 659 |
. . . . 5
โข (((๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง))) โง (๐ฆ = (๐ ฮฃg ๐ค) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค)))) โ ((๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โ (๐โ((๐ ฮฃg ๐ง)(+gโ๐)(๐ ฮฃg ๐ค))) =
((-1โ(โฏโ๐ง)) ยท (-1โ(โฏโ๐ค))))) |
79 | 73, 78 | syl5ibrcom 247 |
. . . 4
โข ((๐ท โ ๐ โง (๐ง โ Word ran (pmTrspโ๐ท) โง ๐ค โ Word ran (pmTrspโ๐ท))) โ (((๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง))) โง (๐ฆ = (๐ ฮฃg ๐ค) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค)))) โ (๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)))) |
80 | 79 | rexlimdvva 3206 |
. . 3
โข (๐ท โ ๐ โ (โ๐ง โ Word ran (pmTrspโ๐ท)โ๐ค โ Word ran (pmTrspโ๐ท)((๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง))) โง (๐ฆ = (๐ ฮฃg ๐ค) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค)))) โ (๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)))) |
81 | 1, 33, 4 | psgnvali 19291 |
. . . . 5
โข (๐ฆ โ dom ๐ โ โ๐ค โ Word ran (pmTrspโ๐ท)(๐ฆ = (๐ ฮฃg ๐ค) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค)))) |
82 | 34, 81 | anim12i 614 |
. . . 4
โข ((๐ฅ โ dom ๐ โง ๐ฆ โ dom ๐) โ (โ๐ง โ Word ran (pmTrspโ๐ท)(๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง))) โง โ๐ค โ Word ran
(pmTrspโ๐ท)(๐ฆ = (๐ ฮฃg ๐ค) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค))))) |
83 | | reeanv 3218 |
. . . 4
โข
(โ๐ง โ
Word ran (pmTrspโ๐ท)โ๐ค โ Word ran (pmTrspโ๐ท)((๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง))) โง (๐ฆ = (๐ ฮฃg ๐ค) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค)))) โ (โ๐ง โ Word ran
(pmTrspโ๐ท)(๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง))) โง โ๐ค โ Word ran
(pmTrspโ๐ท)(๐ฆ = (๐ ฮฃg ๐ค) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค))))) |
84 | 82, 83 | sylibr 233 |
. . 3
โข ((๐ฅ โ dom ๐ โง ๐ฆ โ dom ๐) โ โ๐ง โ Word ran (pmTrspโ๐ท)โ๐ค โ Word ran (pmTrspโ๐ท)((๐ฅ = (๐ ฮฃg ๐ง) โง (๐โ๐ฅ) = (-1โ(โฏโ๐ง))) โง (๐ฆ = (๐ ฮฃg ๐ค) โง (๐โ๐ฆ) = (-1โ(โฏโ๐ค))))) |
85 | 80, 84 | impel 507 |
. 2
โข ((๐ท โ ๐ โง (๐ฅ โ dom ๐ โง ๐ฆ โ dom ๐)) โ (๐โ(๐ฅ(+gโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ))) |
86 | 10, 12, 16, 22, 25, 27, 48, 85 | isghmd 19018 |
1
โข (๐ท โ ๐ โ ๐ โ (๐น GrpHom ๐)) |