Step | Hyp | Ref
| Expression |
1 | | mdetralt.x |
. . 3
โข (๐ โ ๐ โ ๐ต) |
2 | | mdetralt.d |
. . . 4
โข ๐ท = (๐ maDet ๐
) |
3 | | mdetralt.a |
. . . 4
โข ๐ด = (๐ Mat ๐
) |
4 | | mdetralt.b |
. . . 4
โข ๐ต = (Baseโ๐ด) |
5 | | eqid 2733 |
. . . 4
โข
(Baseโ(SymGrpโ๐)) = (Baseโ(SymGrpโ๐)) |
6 | | eqid 2733 |
. . . 4
โข
(โคRHomโ๐
) = (โคRHomโ๐
) |
7 | | eqid 2733 |
. . . 4
โข
(pmSgnโ๐) =
(pmSgnโ๐) |
8 | | eqid 2733 |
. . . 4
โข
(.rโ๐
) = (.rโ๐
) |
9 | | eqid 2733 |
. . . 4
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
10 | 2, 3, 4, 5, 6, 7, 8, 9 | mdetleib 21952 |
. . 3
โข (๐ โ ๐ต โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) |
11 | 1, 10 | syl 17 |
. 2
โข (๐ โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) |
12 | | eqid 2733 |
. . 3
โข
(Baseโ๐
) =
(Baseโ๐
) |
13 | | eqid 2733 |
. . 3
โข
(+gโ๐
) = (+gโ๐
) |
14 | | mdetralt.r |
. . . . 5
โข (๐ โ ๐
โ CRing) |
15 | | crngring 19981 |
. . . . 5
โข (๐
โ CRing โ ๐
โ Ring) |
16 | 14, 15 | syl 17 |
. . . 4
โข (๐ โ ๐
โ Ring) |
17 | | ringcmn 20008 |
. . . 4
โข (๐
โ Ring โ ๐
โ CMnd) |
18 | 16, 17 | syl 17 |
. . 3
โข (๐ โ ๐
โ CMnd) |
19 | 3, 4 | matrcl 21775 |
. . . . . 6
โข (๐ โ ๐ต โ (๐ โ Fin โง ๐
โ V)) |
20 | 1, 19 | syl 17 |
. . . . 5
โข (๐ โ (๐ โ Fin โง ๐
โ V)) |
21 | 20 | simpld 496 |
. . . 4
โข (๐ โ ๐ โ Fin) |
22 | | eqid 2733 |
. . . . 5
โข
(SymGrpโ๐) =
(SymGrpโ๐) |
23 | 22, 5 | symgbasfi 19165 |
. . . 4
โข (๐ โ Fin โ
(Baseโ(SymGrpโ๐)) โ Fin) |
24 | 21, 23 | syl 17 |
. . 3
โข (๐ โ
(Baseโ(SymGrpโ๐)) โ Fin) |
25 | 16 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐
โ Ring) |
26 | | zrhpsgnmhm 21004 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ Fin) โ
((โคRHomโ๐
)
โ (pmSgnโ๐))
โ ((SymGrpโ๐)
MndHom (mulGrpโ๐
))) |
27 | 16, 21, 26 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((โคRHomโ๐
) โ (pmSgnโ๐)) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
))) |
28 | 9, 12 | mgpbas 19907 |
. . . . . . 7
โข
(Baseโ๐
) =
(Baseโ(mulGrpโ๐
)) |
29 | 5, 28 | mhmf 18612 |
. . . . . 6
โข
(((โคRHomโ๐
) โ (pmSgnโ๐)) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
)) โ ((โคRHomโ๐
) โ (pmSgnโ๐)):(Baseโ(SymGrpโ๐))โถ(Baseโ๐
)) |
30 | 27, 29 | syl 17 |
. . . . 5
โข (๐ โ ((โคRHomโ๐
) โ (pmSgnโ๐)):(Baseโ(SymGrpโ๐))โถ(Baseโ๐
)) |
31 | 30 | ffvelcdmda 7036 |
. . . 4
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
(((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐) โ (Baseโ๐
)) |
32 | 9 | crngmgp 19977 |
. . . . . . 7
โข (๐
โ CRing โ
(mulGrpโ๐
) โ
CMnd) |
33 | 14, 32 | syl 17 |
. . . . . 6
โข (๐ โ (mulGrpโ๐
) โ CMnd) |
34 | 33 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (mulGrpโ๐
) โ CMnd) |
35 | 21 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐ โ Fin) |
36 | 3, 12, 4 | matbas2i 21787 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ ๐ โ ((Baseโ๐
) โm (๐ ร ๐))) |
37 | 1, 36 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ โ ((Baseโ๐
) โm (๐ ร ๐))) |
38 | | elmapi 8790 |
. . . . . . . . 9
โข (๐ โ ((Baseโ๐
) โm (๐ ร ๐)) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
40 | 39 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
41 | 22, 5 | symgbasf1o 19161 |
. . . . . . . . . 10
โข (๐ โ
(Baseโ(SymGrpโ๐)) โ ๐:๐โ1-1-ontoโ๐) |
42 | 41 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐:๐โ1-1-ontoโ๐) |
43 | | f1of 6785 |
. . . . . . . . 9
โข (๐:๐โ1-1-ontoโ๐ โ ๐:๐โถ๐) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐:๐โถ๐) |
45 | 44 | ffvelcdmda 7036 |
. . . . . . 7
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ (๐โ๐) โ ๐) |
46 | | simpr 486 |
. . . . . . 7
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ ๐ โ ๐) |
47 | 40, 45, 46 | fovcdmd 7527 |
. . . . . 6
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ ((๐โ๐)๐๐) โ (Baseโ๐
)) |
48 | 47 | ralrimiva 3140 |
. . . . 5
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ โ๐ โ ๐ ((๐โ๐)๐๐) โ (Baseโ๐
)) |
49 | 28, 34, 35, 48 | gsummptcl 19749 |
. . . 4
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) |
50 | 12, 8 | ringcl 19986 |
. . . 4
โข ((๐
โ Ring โง
(((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (Baseโ๐
)) |
51 | 25, 31, 49, 50 | syl3anc 1372 |
. . 3
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (Baseโ๐
)) |
52 | | disjdif 4432 |
. . . 4
โข
((pmEvenโ๐)
โฉ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) = โ
|
53 | 52 | a1i 11 |
. . 3
โข (๐ โ ((pmEvenโ๐) โฉ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) = โ
) |
54 | 22, 5 | evpmss 21006 |
. . . . . 6
โข
(pmEvenโ๐)
โ (Baseโ(SymGrpโ๐)) |
55 | | undif 4442 |
. . . . . 6
โข
((pmEvenโ๐)
โ (Baseโ(SymGrpโ๐)) โ ((pmEvenโ๐) โช ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) =
(Baseโ(SymGrpโ๐))) |
56 | 54, 55 | mpbi 229 |
. . . . 5
โข
((pmEvenโ๐)
โช ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) = (Baseโ(SymGrpโ๐)) |
57 | 56 | eqcomi 2742 |
. . . 4
โข
(Baseโ(SymGrpโ๐)) = ((pmEvenโ๐) โช ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
58 | 57 | a1i 11 |
. . 3
โข (๐ โ
(Baseโ(SymGrpโ๐)) = ((pmEvenโ๐) โช ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)))) |
59 | | eqid 2733 |
. . 3
โข (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) = (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
60 | 12, 13, 18, 24, 51, 53, 58, 59 | gsummptfidmsplitres 19713 |
. 2
โข (๐ โ (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) = ((๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ (pmEvenโ๐)))(+gโ๐
)(๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)))))) |
61 | | resmpt 5992 |
. . . . . . 7
โข
((pmEvenโ๐)
โ (Baseโ(SymGrpโ๐)) โ ((๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ (pmEvenโ๐)) = (๐ โ (pmEvenโ๐) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
62 | 54, 61 | ax-mp 5 |
. . . . . 6
โข ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ (pmEvenโ๐)) = (๐ โ (pmEvenโ๐) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
63 | 16 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ๐
โ Ring) |
64 | 21 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ๐ โ Fin) |
65 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ๐ โ (pmEvenโ๐)) |
66 | | eqid 2733 |
. . . . . . . . . . 11
โข
(1rโ๐
) = (1rโ๐
) |
67 | 6, 7, 66 | zrhpsgnevpm 21011 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ โ Fin โง ๐ โ (pmEvenโ๐)) โ
(((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐) = (1rโ๐
)) |
68 | 63, 64, 65, 67 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (((โคRHomโ๐
) โ (pmSgnโ๐))โ๐) = (1rโ๐
)) |
69 | 68 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = ((1rโ๐
)(.rโ๐
)((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
70 | 54 | sseli 3941 |
. . . . . . . . . 10
โข (๐ โ (pmEvenโ๐) โ ๐ โ (Baseโ(SymGrpโ๐))) |
71 | 70, 49 | sylan2 594 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) |
72 | 12, 8, 66 | ringlidm 19997 |
. . . . . . . . 9
โข ((๐
โ Ring โง
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) โ ((1rโ๐
)(.rโ๐
)((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) |
73 | 63, 71, 72 | syl2anc 585 |
. . . . . . . 8
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((1rโ๐
)(.rโ๐
)((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) |
74 | 69, 73 | eqtrd 2773 |
. . . . . . 7
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) |
75 | 74 | mpteq2dva 5206 |
. . . . . 6
โข (๐ โ (๐ โ (pmEvenโ๐) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) = (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
76 | 62, 75 | eqtrid 2785 |
. . . . 5
โข (๐ โ ((๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ (pmEvenโ๐)) = (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
77 | 76 | oveq2d 7374 |
. . . 4
โข (๐ โ (๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ (pmEvenโ๐))) = (๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
78 | | difss 4092 |
. . . . . . . 8
โข
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โ (Baseโ(SymGrpโ๐)) |
79 | | resmpt 5992 |
. . . . . . . 8
โข
(((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โ (Baseโ(SymGrpโ๐)) โ ((๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) = (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
80 | 78, 79 | ax-mp 5 |
. . . . . . 7
โข ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) = (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
81 | 16 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ ๐
โ Ring) |
82 | 21 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ ๐ โ Fin) |
83 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
84 | | eqid 2733 |
. . . . . . . . . . . . 13
โข
(invgโ๐
) = (invgโ๐
) |
85 | 6, 7, 66, 5, 84 | zrhpsgnodpm 21012 |
. . . . . . . . . . . 12
โข ((๐
โ Ring โง ๐ โ Fin โง ๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ (((โคRHomโ๐
) โ (pmSgnโ๐))โ๐) = ((invgโ๐
)โ(1rโ๐
))) |
86 | 81, 82, 83, 85 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ
(((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐) = ((invgโ๐
)โ(1rโ๐
))) |
87 | 86 | oveq1d 7373 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = (((invgโ๐
)โ(1rโ๐
))(.rโ๐
)((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
88 | | eldifi 4087 |
. . . . . . . . . . . 12
โข (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โ ๐ โ (Baseโ(SymGrpโ๐))) |
89 | 88, 49 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) |
90 | 12, 8, 66, 84, 81, 89 | ringnegl 20023 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ
(((invgโ๐
)โ(1rโ๐
))(.rโ๐
)((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = ((invgโ๐
)โ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
91 | 87, 90 | eqtrd 2773 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = ((invgโ๐
)โ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
92 | 91 | mpteq2dva 5206 |
. . . . . . . 8
โข (๐ โ (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) = (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ
((invgโ๐
)โ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
93 | | ringgrp 19974 |
. . . . . . . . . . 11
โข (๐
โ Ring โ ๐
โ Grp) |
94 | 16, 93 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐
โ Grp) |
95 | 12, 84 | grpinvf 18802 |
. . . . . . . . . 10
โข (๐
โ Grp โ
(invgโ๐
):(Baseโ๐
)โถ(Baseโ๐
)) |
96 | 94, 95 | syl 17 |
. . . . . . . . 9
โข (๐ โ
(invgโ๐
):(Baseโ๐
)โถ(Baseโ๐
)) |
97 | 96, 89 | cofmpt 7079 |
. . . . . . . 8
โข (๐ โ
((invgโ๐
)
โ (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) = (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ
((invgโ๐
)โ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
98 | 92, 97 | eqtr4d 2776 |
. . . . . . 7
โข (๐ โ (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) = ((invgโ๐
) โ (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
99 | 80, 98 | eqtrid 2785 |
. . . . . 6
โข (๐ โ ((๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) = ((invgโ๐
) โ (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
100 | 99 | oveq2d 7374 |
. . . . 5
โข (๐ โ (๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)))) = (๐
ฮฃg
((invgโ๐
)
โ (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) |
101 | | mdetralt.z |
. . . . . 6
โข 0 =
(0gโ๐
) |
102 | | ringabl 20007 |
. . . . . . 7
โข (๐
โ Ring โ ๐
โ Abel) |
103 | 16, 102 | syl 17 |
. . . . . 6
โข (๐ โ ๐
โ Abel) |
104 | | difssd 4093 |
. . . . . . 7
โข (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โ (Baseโ(SymGrpโ๐))) |
105 | 24, 104 | ssfid 9214 |
. . . . . 6
โข (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โ Fin) |
106 | | eqid 2733 |
. . . . . 6
โข (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))) |
107 | 12, 101, 84, 103, 105, 89, 106 | gsummptfidminv 19729 |
. . . . 5
โข (๐ โ (๐
ฮฃg
((invgโ๐
)
โ (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) = ((invgโ๐
)โ(๐
ฮฃg (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) |
108 | 89 | ralrimiva 3140 |
. . . . . . . 8
โข (๐ โ โ๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) |
109 | | mdetralt.i |
. . . . . . . . . . . 12
โข (๐ โ ๐ผ โ ๐) |
110 | | mdetralt.j |
. . . . . . . . . . . 12
โข (๐ โ ๐ฝ โ ๐) |
111 | 109, 110 | prssd 4783 |
. . . . . . . . . . 11
โข (๐ โ {๐ผ, ๐ฝ} โ ๐) |
112 | | mdetralt.ij |
. . . . . . . . . . . 12
โข (๐ โ ๐ผ โ ๐ฝ) |
113 | | enpr2 9943 |
. . . . . . . . . . . 12
โข ((๐ผ โ ๐ โง ๐ฝ โ ๐ โง ๐ผ โ ๐ฝ) โ {๐ผ, ๐ฝ} โ 2o) |
114 | 109, 110,
112, 113 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ {๐ผ, ๐ฝ} โ 2o) |
115 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(pmTrspโ๐) =
(pmTrspโ๐) |
116 | | eqid 2733 |
. . . . . . . . . . . 12
โข ran
(pmTrspโ๐) = ran
(pmTrspโ๐) |
117 | 115, 116 | pmtrrn 19244 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง {๐ผ, ๐ฝ} โ ๐ โง {๐ผ, ๐ฝ} โ 2o) โ
((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ran (pmTrspโ๐)) |
118 | 21, 111, 114, 117 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ran (pmTrspโ๐)) |
119 | 22, 5, 116 | pmtrodpm 21017 |
. . . . . . . . . 10
โข ((๐ โ Fin โง
((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ran (pmTrspโ๐)) โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
120 | 21, 118, 119 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
121 | 22, 5 | evpmodpmf1o 21016 |
. . . . . . . . 9
โข ((๐ โ Fin โง
((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ (๐ โ (pmEvenโ๐) โฆ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)):(pmEvenโ๐)โ1-1-ontoโ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
122 | 21, 120, 121 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (๐ โ (pmEvenโ๐) โฆ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)):(pmEvenโ๐)โ1-1-ontoโ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
123 | 12, 18, 105, 108, 106, 122 | gsummptfif1o 19750 |
. . . . . . 7
โข (๐ โ (๐
ฮฃg (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) = (๐
ฮฃg ((๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (๐ โ (pmEvenโ๐) โฆ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐))))) |
124 | | eleq1w 2817 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ โ (pmEvenโ๐) โ ๐ โ (pmEvenโ๐))) |
125 | 124 | anbi2d 630 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ โง ๐ โ (pmEvenโ๐)) โ (๐ โง ๐ โ (pmEvenโ๐)))) |
126 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)) |
127 | 126 | eleq1d 2819 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)))) |
128 | 125, 127 | imbi12d 345 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (((๐ โง ๐ โ (pmEvenโ๐)) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) โ ((๐ โง ๐ โ (pmEvenโ๐)) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))))) |
129 | 22 | symggrp 19187 |
. . . . . . . . . . . . . . 15
โข (๐ โ Fin โ
(SymGrpโ๐) โ
Grp) |
130 | 21, 129 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (SymGrpโ๐) โ Grp) |
131 | 130 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (SymGrpโ๐) โ Grp) |
132 | 116, 22, 5 | symgtrf 19256 |
. . . . . . . . . . . . . 14
โข ran
(pmTrspโ๐) โ
(Baseโ(SymGrpโ๐)) |
133 | 118 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ran (pmTrspโ๐)) |
134 | 132, 133 | sselid 3943 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ (Baseโ(SymGrpโ๐))) |
135 | 70 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ๐ โ (Baseโ(SymGrpโ๐))) |
136 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข
(+gโ(SymGrpโ๐)) =
(+gโ(SymGrpโ๐)) |
137 | 5, 136 | grpcl 18761 |
. . . . . . . . . . . . 13
โข
(((SymGrpโ๐)
โ Grp โง ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ (Baseโ(SymGrpโ๐)) โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ (Baseโ(SymGrpโ๐))) |
138 | 131, 134,
135, 137 | syl3anc 1372 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ (Baseโ(SymGrpโ๐))) |
139 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข
((mulGrpโโfld) โพs {1, -1}) =
((mulGrpโโfld) โพs {1,
-1}) |
140 | 22, 7, 139 | psgnghm2 21001 |
. . . . . . . . . . . . . . . 16
โข (๐ โ Fin โ
(pmSgnโ๐) โ
((SymGrpโ๐) GrpHom
((mulGrpโโfld) โพs {1,
-1}))) |
141 | 21, 140 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (pmSgnโ๐) โ ((SymGrpโ๐) GrpHom
((mulGrpโโfld) โพs {1,
-1}))) |
142 | 141 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (pmSgnโ๐) โ ((SymGrpโ๐) GrpHom
((mulGrpโโfld) โพs {1,
-1}))) |
143 | | prex 5390 |
. . . . . . . . . . . . . . . 16
โข {1, -1}
โ V |
144 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
โข
(mulGrpโโfld) =
(mulGrpโโfld) |
145 | | cnfldmul 20818 |
. . . . . . . . . . . . . . . . . 18
โข ยท
= (.rโโfld) |
146 | 144, 145 | mgpplusg 19905 |
. . . . . . . . . . . . . . . . 17
โข ยท
= (+gโ(mulGrpโโfld)) |
147 | 139, 146 | ressplusg 17176 |
. . . . . . . . . . . . . . . 16
โข ({1, -1}
โ V โ ยท =
(+gโ((mulGrpโโfld) โพs
{1, -1}))) |
148 | 143, 147 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข ยท
= (+gโ((mulGrpโโfld)
โพs {1, -1})) |
149 | 5, 136, 148 | ghmlin 19018 |
. . . . . . . . . . . . . 14
โข
(((pmSgnโ๐)
โ ((SymGrpโ๐)
GrpHom ((mulGrpโโfld) โพs {1, -1}))
โง ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ (Baseโ(SymGrpโ๐)) โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((pmSgnโ๐)โ(((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)) = (((pmSgnโ๐)โ((pmTrspโ๐)โ{๐ผ, ๐ฝ})) ยท ((pmSgnโ๐)โ๐))) |
150 | 142, 134,
135, 149 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((pmSgnโ๐)โ(((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)) = (((pmSgnโ๐)โ((pmTrspโ๐)โ{๐ผ, ๐ฝ})) ยท ((pmSgnโ๐)โ๐))) |
151 | 22, 116, 7 | psgnpmtr 19297 |
. . . . . . . . . . . . . . . 16
โข
(((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ran (pmTrspโ๐) โ ((pmSgnโ๐)โ((pmTrspโ๐)โ{๐ผ, ๐ฝ})) = -1) |
152 | 133, 151 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((pmSgnโ๐)โ((pmTrspโ๐)โ{๐ผ, ๐ฝ})) = -1) |
153 | 22, 5, 7 | psgnevpm 21009 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ Fin โง ๐ โ (pmEvenโ๐)) โ ((pmSgnโ๐)โ๐) = 1) |
154 | 21, 153 | sylan 581 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((pmSgnโ๐)โ๐) = 1) |
155 | 152, 154 | oveq12d 7376 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (((pmSgnโ๐)โ((pmTrspโ๐)โ{๐ผ, ๐ฝ})) ยท ((pmSgnโ๐)โ๐)) = (-1 ยท 1)) |
156 | | neg1cn 12272 |
. . . . . . . . . . . . . . 15
โข -1 โ
โ |
157 | 156 | mulid1i 11164 |
. . . . . . . . . . . . . 14
โข (-1
ยท 1) = -1 |
158 | 155, 157 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (((pmSgnโ๐)โ((pmTrspโ๐)โ{๐ผ, ๐ฝ})) ยท ((pmSgnโ๐)โ๐)) = -1) |
159 | 150, 158 | eqtrd 2773 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((pmSgnโ๐)โ(((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)) = -1) |
160 | 22, 5, 7 | psgnodpmr 21010 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง
(((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ (Baseโ(SymGrpโ๐)) โง ((pmSgnโ๐)โ(((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)) = -1) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
161 | 64, 138, 159, 160 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
162 | 128, 161 | chvarvv 2003 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))) |
163 | | eqidd 2734 |
. . . . . . . . . 10
โข (๐ โ (๐ โ (pmEvenโ๐) โฆ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)) = (๐ โ (pmEvenโ๐) โฆ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐))) |
164 | | eqidd 2734 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = (๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
165 | | fveq1 6842 |
. . . . . . . . . . . . 13
โข (๐ = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ (๐โ๐) = ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)) |
166 | 165 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((๐โ๐)๐๐) = (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)) |
167 | 166 | mpteq2dv 5208 |
. . . . . . . . . . 11
โข (๐ = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ (๐ โ ๐ โฆ ((๐โ๐)๐๐)) = (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐))) |
168 | 167 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)))) |
169 | 162, 163,
164, 168 | fmptco 7076 |
. . . . . . . . 9
โข (๐ โ ((๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (๐ โ (pmEvenโ๐) โฆ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐))) = (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐))))) |
170 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)) |
171 | 170 | fveq1d 6845 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐) = ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)) |
172 | 171 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐) = (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)) |
173 | 172 | mpteq2dv 5208 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)) = (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐))) |
174 | 173 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)))) |
175 | 174 | cbvmptv 5219 |
. . . . . . . . . 10
โข (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)))) = (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)))) |
176 | 175 | a1i 11 |
. . . . . . . . 9
โข (๐ โ (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)))) = (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐))))) |
177 | 134 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ (Baseโ(SymGrpโ๐))) |
178 | 135 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ๐ โ (Baseโ(SymGrpโ๐))) |
179 | 22, 5, 136 | symgov 19170 |
. . . . . . . . . . . . . . . . 17
โข
((((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ (Baseโ(SymGrpโ๐)) โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ๐)) |
180 | 177, 178,
179 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ๐)) |
181 | 180 | fveq1d 6845 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐) = ((((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ๐)โ๐)) |
182 | 70, 44 | sylan2 594 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ๐:๐โถ๐) |
183 | | fvco3 6941 |
. . . . . . . . . . . . . . . 16
โข ((๐:๐โถ๐ โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ๐)โ๐) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))) |
184 | 182, 183 | sylan 581 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ ๐)โ๐) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))) |
185 | 181, 184 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))) |
186 | 185 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐) = ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐)) |
187 | 115 | pmtrprfv 19240 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ Fin โง (๐ผ โ ๐ โง ๐ฝ โ ๐ โง ๐ผ โ ๐ฝ)) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ผ) = ๐ฝ) |
188 | 21, 109, 110, 112, 187 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ผ) = ๐ฝ) |
189 | 188 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ผ) = ๐ฝ) |
190 | 189 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ผ)๐๐) = (๐ฝ๐๐)) |
191 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (๐ผ๐๐) = (๐ผ๐๐)) |
192 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (๐ฝ๐๐) = (๐ฝ๐๐)) |
193 | 191, 192 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((๐ผ๐๐) = (๐ฝ๐๐) โ (๐ผ๐๐) = (๐ฝ๐๐))) |
194 | | mdetralt.eq |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ๐ โ ๐ (๐ผ๐๐) = (๐ฝ๐๐)) |
195 | 194 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ โ๐ โ ๐ (๐ผ๐๐) = (๐ฝ๐๐)) |
196 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ๐ โ ๐) |
197 | 193, 195,
196 | rspcdva 3581 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ (๐ผ๐๐) = (๐ฝ๐๐)) |
198 | 190, 197 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ผ)๐๐) = (๐ผ๐๐)) |
199 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
โข ((๐โ๐) = ๐ผ โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐)) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ผ)) |
200 | 199 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข ((๐โ๐) = ๐ผ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ผ)๐๐)) |
201 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
โข ((๐โ๐) = ๐ผ โ ((๐โ๐)๐๐) = (๐ผ๐๐)) |
202 | 200, 201 | eqeq12d 2749 |
. . . . . . . . . . . . . . 15
โข ((๐โ๐) = ๐ผ โ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ผ)๐๐) = (๐ผ๐๐))) |
203 | 198, 202 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((๐โ๐) = ๐ผ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐))) |
204 | | prcom 4694 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข {๐ผ, ๐ฝ} = {๐ฝ, ๐ผ} |
205 | 204 | fveq2i 6846 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((pmTrspโ๐)โ{๐ผ, ๐ฝ}) = ((pmTrspโ๐)โ{๐ฝ, ๐ผ}) |
206 | 205 | fveq1i 6844 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ฝ) = (((pmTrspโ๐)โ{๐ฝ, ๐ผ})โ๐ฝ) |
207 | 112 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ฝ โ ๐ผ) |
208 | 115 | pmtrprfv 19240 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ Fin โง (๐ฝ โ ๐ โง ๐ผ โ ๐ โง ๐ฝ โ ๐ผ)) โ (((pmTrspโ๐)โ{๐ฝ, ๐ผ})โ๐ฝ) = ๐ผ) |
209 | 21, 110, 109, 207, 208 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (((pmTrspโ๐)โ{๐ฝ, ๐ผ})โ๐ฝ) = ๐ผ) |
210 | 206, 209 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ฝ) = ๐ผ) |
211 | 210 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ฝ)๐๐) = (๐ผ๐๐)) |
212 | 211 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ฝ)๐๐) = (๐ผ๐๐)) |
213 | 212, 197 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ฝ)๐๐) = (๐ฝ๐๐)) |
214 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐โ๐) = ๐ฝ โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐)) = (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ฝ)) |
215 | 214 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
โข ((๐โ๐) = ๐ฝ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ฝ)๐๐)) |
216 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
โข ((๐โ๐) = ๐ฝ โ ((๐โ๐)๐๐) = (๐ฝ๐๐)) |
217 | 215, 216 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . 17
โข ((๐โ๐) = ๐ฝ โ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ๐ฝ)๐๐) = (๐ฝ๐๐))) |
218 | 213, 217 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((๐โ๐) = ๐ฝ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐))) |
219 | 218 | a1dd 50 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((๐โ๐) = ๐ฝ โ ((๐โ๐) โ ๐ผ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐)))) |
220 | | neanior 3034 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ ยฌ ((๐โ๐) = ๐ฝ โจ (๐โ๐) = ๐ผ)) |
221 | | elpri 4609 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐โ๐) โ {๐ผ, ๐ฝ} โ ((๐โ๐) = ๐ผ โจ (๐โ๐) = ๐ฝ)) |
222 | 221 | orcomd 870 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐โ๐) โ {๐ผ, ๐ฝ} โ ((๐โ๐) = ๐ฝ โจ (๐โ๐) = ๐ผ)) |
223 | 222 | con3i 154 |
. . . . . . . . . . . . . . . . . . . . 21
โข (ยฌ
((๐โ๐) = ๐ฝ โจ (๐โ๐) = ๐ผ) โ ยฌ (๐โ๐) โ {๐ผ, ๐ฝ}) |
224 | 220, 223 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ ยฌ (๐โ๐) โ {๐ผ, ๐ฝ}) |
225 | 224 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โง (๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ ยฌ (๐โ๐) โ {๐ผ, ๐ฝ}) |
226 | 115 | pmtrmvd 19243 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ Fin โง {๐ผ, ๐ฝ} โ ๐ โง {๐ผ, ๐ฝ} โ 2o) โ dom
(((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I ) = {๐ผ, ๐ฝ}) |
227 | 21, 111, 114, 226 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ dom (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I ) = {๐ผ, ๐ฝ}) |
228 | 227 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ dom (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I ) = {๐ผ, ๐ฝ}) |
229 | 228 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โง (๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ dom (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I ) = {๐ผ, ๐ฝ}) |
230 | 225, 229 | neleqtrrd 2857 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โง (๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ ยฌ (๐โ๐) โ dom (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I )) |
231 | 115 | pmtrf 19242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โ Fin โง {๐ผ, ๐ฝ} โ ๐ โง {๐ผ, ๐ฝ} โ 2o) โ
((pmTrspโ๐)โ{๐ผ, ๐ฝ}):๐โถ๐) |
232 | 21, 111, 114, 231 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}):๐โถ๐) |
233 | 232 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) Fn ๐) |
234 | 233 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((pmTrspโ๐)โ{๐ผ, ๐ฝ}) Fn ๐) |
235 | 182 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ (๐โ๐) โ ๐) |
236 | | fnelnfp 7124 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((pmTrspโ๐)โ{๐ผ, ๐ฝ}) Fn ๐ โง (๐โ๐) โ ๐) โ ((๐โ๐) โ dom (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I ) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐)) โ (๐โ๐))) |
237 | 234, 235,
236 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((๐โ๐) โ dom (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I ) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐)) โ (๐โ๐))) |
238 | 237 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โง (๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ ((๐โ๐) โ dom (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I ) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐)) โ (๐โ๐))) |
239 | 238 | necon2bbid 2984 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โง (๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐)) = (๐โ๐) โ ยฌ (๐โ๐) โ dom (((pmTrspโ๐)โ{๐ผ, ๐ฝ}) โ I ))) |
240 | 230, 239 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โง (๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐)) = (๐โ๐)) |
241 | 240 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โง (๐โ๐) โ ๐ฝ โง (๐โ๐) โ ๐ผ) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐)) |
242 | 241 | 3exp 1120 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((๐โ๐) โ ๐ฝ โ ((๐โ๐) โ ๐ผ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐)))) |
243 | 219, 242 | pm2.61dne 3028 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((๐โ๐) โ ๐ผ โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐))) |
244 | 203, 243 | pm2.61dne 3028 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ ((((pmTrspโ๐)โ{๐ผ, ๐ฝ})โ(๐โ๐))๐๐) = ((๐โ๐)๐๐)) |
245 | 186, 244 | eqtrd 2773 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (pmEvenโ๐)) โง ๐ โ ๐) โ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐) = ((๐โ๐)๐๐)) |
246 | 245 | mpteq2dva 5206 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)) = (๐ โ ๐ โฆ ((๐โ๐)๐๐))) |
247 | 246 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (pmEvenโ๐)) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) |
248 | 247 | mpteq2dva 5206 |
. . . . . . . . 9
โข (๐ โ (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (((((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)โ๐)๐๐)))) = (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
249 | 169, 176,
248 | 3eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((๐ โ ((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (๐ โ (pmEvenโ๐) โฆ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐))) = (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) |
250 | 249 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ (๐
ฮฃg ((๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (๐ โ (pmEvenโ๐) โฆ (((pmTrspโ๐)โ{๐ผ, ๐ฝ})(+gโ(SymGrpโ๐))๐)))) = (๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
251 | 123, 250 | eqtrd 2773 |
. . . . . 6
โข (๐ โ (๐
ฮฃg (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) = (๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) |
252 | 251 | fveq2d 6847 |
. . . . 5
โข (๐ โ
((invgโ๐
)โ(๐
ฮฃg (๐ โ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)) โฆ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) = ((invgโ๐
)โ(๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) |
253 | 100, 107,
252 | 3eqtrd 2777 |
. . . 4
โข (๐ โ (๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐)))) = ((invgโ๐
)โ(๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) |
254 | 77, 253 | oveq12d 7376 |
. . 3
โข (๐ โ ((๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ (pmEvenโ๐)))(+gโ๐
)(๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))))) = ((๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))(+gโ๐
)((invgโ๐
)โ(๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))))) |
255 | 54 | a1i 11 |
. . . . . 6
โข (๐ โ (pmEvenโ๐) โ
(Baseโ(SymGrpโ๐))) |
256 | 24, 255 | ssfid 9214 |
. . . . 5
โข (๐ โ (pmEvenโ๐) โ Fin) |
257 | 71 | ralrimiva 3140 |
. . . . 5
โข (๐ โ โ๐ โ (pmEvenโ๐)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) |
258 | 12, 18, 256, 257 | gsummptcl 19749 |
. . . 4
โข (๐ โ (๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โ (Baseโ๐
)) |
259 | 12, 13, 101, 84 | grprinv 18806 |
. . . 4
โข ((๐
โ Grp โง (๐
ฮฃg
(๐ โ
(pmEvenโ๐) โฆ
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โ (Baseโ๐
)) โ ((๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))(+gโ๐
)((invgโ๐
)โ(๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) = 0 ) |
260 | 94, 258, 259 | syl2anc 585 |
. . 3
โข (๐ โ ((๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐)))))(+gโ๐
)((invgโ๐
)โ(๐
ฮฃg (๐ โ (pmEvenโ๐) โฆ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) = 0 ) |
261 | 254, 260 | eqtrd 2773 |
. 2
โข (๐ โ ((๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ (pmEvenโ๐)))(+gโ๐
)(๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))) โพ
((Baseโ(SymGrpโ๐)) โ (pmEvenโ๐))))) = 0 ) |
262 | 11, 60, 261 | 3eqtrd 2777 |
1
โข (๐ โ (๐ทโ๐) = 0 ) |