Step | Hyp | Ref
| Expression |
1 | | m2detleib.d |
. . . 4
โข ๐ท = (๐ maDet ๐
) |
2 | | m2detleib.a |
. . . 4
โข ๐ด = (๐ Mat ๐
) |
3 | | m2detleib.b |
. . . 4
โข ๐ต = (Baseโ๐ด) |
4 | | eqid 2733 |
. . . 4
โข
(Baseโ(SymGrpโ๐)) = (Baseโ(SymGrpโ๐)) |
5 | | eqid 2733 |
. . . 4
โข
(โคRHomโ๐
) = (โคRHomโ๐
) |
6 | | eqid 2733 |
. . . 4
โข
(pmSgnโ๐) =
(pmSgnโ๐) |
7 | | m2detleib.t |
. . . 4
โข ยท =
(.rโ๐
) |
8 | | eqid 2733 |
. . . 4
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib1 21956 |
. . 3
โข (๐ โ ๐ต โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) |
10 | 9 | adantl 483 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) |
11 | | eqid 2733 |
. . 3
โข
(Baseโ๐
) =
(Baseโ๐
) |
12 | | eqid 2733 |
. . 3
โข
(+gโ๐
) = (+gโ๐
) |
13 | | ringcmn 20008 |
. . . 4
โข (๐
โ Ring โ ๐
โ CMnd) |
14 | 13 | adantr 482 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐
โ CMnd) |
15 | | m2detleib.n |
. . . . . 6
โข ๐ = {1, 2} |
16 | | prfi 9269 |
. . . . . 6
โข {1, 2}
โ Fin |
17 | 15, 16 | eqeltri 2830 |
. . . . 5
โข ๐ โ Fin |
18 | | eqid 2733 |
. . . . . 6
โข
(SymGrpโ๐) =
(SymGrpโ๐) |
19 | 18, 4 | symgbasfi 19165 |
. . . . 5
โข (๐ โ Fin โ
(Baseโ(SymGrpโ๐)) โ Fin) |
20 | 17, 19 | ax-mp 5 |
. . . 4
โข
(Baseโ(SymGrpโ๐)) โ Fin |
21 | 20 | a1i 11 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (Baseโ(SymGrpโ๐)) โ Fin) |
22 | | simpl 484 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐
โ Ring) |
23 | 22 | adantr 482 |
. . . 4
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐
โ Ring) |
24 | 4, 6, 5 | zrhpsgnelbas 21014 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ Fin โง ๐ โ
(Baseโ(SymGrpโ๐))) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) โ (Baseโ๐
)) |
25 | 17, 24 | mp3an2 1450 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ
(Baseโ(SymGrpโ๐))) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) โ (Baseโ๐
)) |
26 | 25 | adantlr 714 |
. . . 4
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ (Baseโ(SymGrpโ๐))) โ
((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) โ (Baseโ๐
)) |
27 | | simpr 486 |
. . . . 5
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐ โ (Baseโ(SymGrpโ๐))) |
28 | | simpr 486 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
29 | 28 | adantr 482 |
. . . . 5
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐ โ ๐ต) |
30 | 15, 4, 2, 3, 8 | m2detleiblem2 21993 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ
(Baseโ(SymGrpโ๐)) โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) |
31 | 23, 27, 29, 30 | syl3anc 1372 |
. . . 4
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) |
32 | 11, 7 | ringcl 19986 |
. . . 4
โข ((๐
โ Ring โง
((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) โ (Baseโ๐
)) โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (Baseโ๐
)) |
33 | 23, 26, 31, 32 | syl3anc 1372 |
. . 3
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ (Baseโ(SymGrpโ๐))) โ
(((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) โ (Baseโ๐
)) |
34 | | opex 5422 |
. . . . . . . 8
โข โจ1,
1โฉ โ V |
35 | | opex 5422 |
. . . . . . . 8
โข โจ2,
2โฉ โ V |
36 | 34, 35 | pm3.2i 472 |
. . . . . . 7
โข (โจ1,
1โฉ โ V โง โจ2, 2โฉ โ V) |
37 | | opex 5422 |
. . . . . . . 8
โข โจ1,
2โฉ โ V |
38 | | opex 5422 |
. . . . . . . 8
โข โจ2,
1โฉ โ V |
39 | 37, 38 | pm3.2i 472 |
. . . . . . 7
โข (โจ1,
2โฉ โ V โง โจ2, 1โฉ โ V) |
40 | 36, 39 | pm3.2i 472 |
. . . . . 6
โข
((โจ1, 1โฉ โ V โง โจ2, 2โฉ โ V) โง
(โจ1, 2โฉ โ V โง โจ2, 1โฉ โ V)) |
41 | | 1ne2 12366 |
. . . . . . . . . 10
โข 1 โ
2 |
42 | 41 | olci 865 |
. . . . . . . . 9
โข (1 โ 1
โจ 1 โ 2) |
43 | | 1ex 11156 |
. . . . . . . . . 10
โข 1 โ
V |
44 | 43, 43 | opthne 5440 |
. . . . . . . . 9
โข (โจ1,
1โฉ โ โจ1, 2โฉ โ (1 โ 1 โจ 1 โ 2)) |
45 | 42, 44 | mpbir 230 |
. . . . . . . 8
โข โจ1,
1โฉ โ โจ1, 2โฉ |
46 | 41 | orci 864 |
. . . . . . . . 9
โข (1 โ 2
โจ 1 โ 1) |
47 | 43, 43 | opthne 5440 |
. . . . . . . . 9
โข (โจ1,
1โฉ โ โจ2, 1โฉ โ (1 โ 2 โจ 1 โ 1)) |
48 | 46, 47 | mpbir 230 |
. . . . . . . 8
โข โจ1,
1โฉ โ โจ2, 1โฉ |
49 | 45, 48 | pm3.2i 472 |
. . . . . . 7
โข (โจ1,
1โฉ โ โจ1, 2โฉ โง โจ1, 1โฉ โ โจ2,
1โฉ) |
50 | 49 | orci 864 |
. . . . . 6
โข
((โจ1, 1โฉ โ โจ1, 2โฉ โง โจ1, 1โฉ โ
โจ2, 1โฉ) โจ (โจ2, 2โฉ โ โจ1, 2โฉ โง โจ2,
2โฉ โ โจ2, 1โฉ)) |
51 | 40, 50 | pm3.2i 472 |
. . . . 5
โข
(((โจ1, 1โฉ โ V โง โจ2, 2โฉ โ V) โง
(โจ1, 2โฉ โ V โง โจ2, 1โฉ โ V)) โง ((โจ1,
1โฉ โ โจ1, 2โฉ โง โจ1, 1โฉ โ โจ2, 1โฉ)
โจ (โจ2, 2โฉ โ โจ1, 2โฉ โง โจ2, 2โฉ โ
โจ2, 1โฉ))) |
52 | 51 | a1i 11 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (((โจ1, 1โฉ โ V โง
โจ2, 2โฉ โ V) โง (โจ1, 2โฉ โ V โง โจ2,
1โฉ โ V)) โง ((โจ1, 1โฉ โ โจ1, 2โฉ โง
โจ1, 1โฉ โ โจ2, 1โฉ) โจ (โจ2, 2โฉ โ โจ1,
2โฉ โง โจ2, 2โฉ โ โจ2, 1โฉ)))) |
53 | | prneimg 4813 |
. . . . 5
โข
(((โจ1, 1โฉ โ V โง โจ2, 2โฉ โ V) โง
(โจ1, 2โฉ โ V โง โจ2, 1โฉ โ V)) โ (((โจ1,
1โฉ โ โจ1, 2โฉ โง โจ1, 1โฉ โ โจ2, 1โฉ)
โจ (โจ2, 2โฉ โ โจ1, 2โฉ โง โจ2, 2โฉ โ
โจ2, 1โฉ)) โ {โจ1, 1โฉ, โจ2, 2โฉ} โ {โจ1,
2โฉ, โจ2, 1โฉ})) |
54 | 53 | imp 408 |
. . . 4
โข
((((โจ1, 1โฉ โ V โง โจ2, 2โฉ โ V) โง
(โจ1, 2โฉ โ V โง โจ2, 1โฉ โ V)) โง ((โจ1,
1โฉ โ โจ1, 2โฉ โง โจ1, 1โฉ โ โจ2, 1โฉ)
โจ (โจ2, 2โฉ โ โจ1, 2โฉ โง โจ2, 2โฉ โ
โจ2, 1โฉ))) โ {โจ1, 1โฉ, โจ2, 2โฉ} โ {โจ1,
2โฉ, โจ2, 1โฉ}) |
55 | | disjsn2 4674 |
. . . 4
โข
({โจ1, 1โฉ, โจ2, 2โฉ} โ {โจ1, 2โฉ, โจ2,
1โฉ} โ ({{โจ1, 1โฉ, โจ2, 2โฉ}} โฉ {{โจ1,
2โฉ, โจ2, 1โฉ}}) = โ
) |
56 | 52, 54, 55 | 3syl 18 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ({{โจ1, 1โฉ, โจ2,
2โฉ}} โฉ {{โจ1, 2โฉ, โจ2, 1โฉ}}) =
โ
) |
57 | | 2nn 12231 |
. . . . . 6
โข 2 โ
โ |
58 | 18, 4, 15 | symg2bas 19179 |
. . . . . 6
โข ((1
โ V โง 2 โ โ) โ (Baseโ(SymGrpโ๐)) = {{โจ1, 1โฉ,
โจ2, 2โฉ}, {โจ1, 2โฉ, โจ2, 1โฉ}}) |
59 | 43, 57, 58 | mp2an 691 |
. . . . 5
โข
(Baseโ(SymGrpโ๐)) = {{โจ1, 1โฉ, โจ2, 2โฉ},
{โจ1, 2โฉ, โจ2, 1โฉ}} |
60 | | df-pr 4590 |
. . . . 5
โข
{{โจ1, 1โฉ, โจ2, 2โฉ}, {โจ1, 2โฉ, โจ2,
1โฉ}} = ({{โจ1, 1โฉ, โจ2, 2โฉ}} โช {{โจ1, 2โฉ,
โจ2, 1โฉ}}) |
61 | 59, 60 | eqtri 2761 |
. . . 4
โข
(Baseโ(SymGrpโ๐)) = ({{โจ1, 1โฉ, โจ2, 2โฉ}}
โช {{โจ1, 2โฉ, โจ2, 1โฉ}}) |
62 | 61 | a1i 11 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (Baseโ(SymGrpโ๐)) = ({{โจ1, 1โฉ,
โจ2, 2โฉ}} โช {{โจ1, 2โฉ, โจ2,
1โฉ}})) |
63 | 11, 12, 14, 21, 33, 56, 62 | gsummptfidmsplit 19712 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) = ((๐
ฮฃg (๐ โ {{โจ1, 1โฉ,
โจ2, 2โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))(+gโ๐
)(๐
ฮฃg (๐ โ {{โจ1, 2โฉ,
โจ2, 1โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))))) |
64 | | ringmnd 19979 |
. . . . . 6
โข (๐
โ Ring โ ๐
โ Mnd) |
65 | 64 | adantr 482 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐
โ Mnd) |
66 | | prex 5390 |
. . . . . 6
โข {โจ1,
1โฉ, โจ2, 2โฉ} โ V |
67 | 66 | a1i 11 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ {โจ1, 1โฉ, โจ2,
2โฉ} โ V) |
68 | 66 | prid1 4724 |
. . . . . . . . 9
โข {โจ1,
1โฉ, โจ2, 2โฉ} โ {{โจ1, 1โฉ, โจ2, 2โฉ},
{โจ1, 2โฉ, โจ2, 1โฉ}} |
69 | 68, 59 | eleqtrri 2833 |
. . . . . . . 8
โข {โจ1,
1โฉ, โจ2, 2โฉ} โ (Baseโ(SymGrpโ๐)) |
70 | 69 | a1i 11 |
. . . . . . 7
โข (๐ โ ๐ต โ {โจ1, 1โฉ, โจ2, 2โฉ}
โ (Baseโ(SymGrpโ๐))) |
71 | 4, 6, 5 | zrhpsgnelbas 21014 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ Fin โง {โจ1,
1โฉ, โจ2, 2โฉ} โ (Baseโ(SymGrpโ๐))) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) โ (Baseโ๐
)) |
72 | 17, 71 | mp3an2 1450 |
. . . . . . 7
โข ((๐
โ Ring โง {โจ1,
1โฉ, โจ2, 2โฉ} โ (Baseโ(SymGrpโ๐))) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) โ (Baseโ๐
)) |
73 | 70, 72 | sylan2 594 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) โ (Baseโ๐
)) |
74 | 15, 4, 2, 3, 8 | m2detleiblem2 21993 |
. . . . . . 7
โข ((๐
โ Ring โง {โจ1,
1โฉ, โจ2, 2โฉ} โ (Baseโ(SymGrpโ๐)) โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))) โ (Baseโ๐
)) |
75 | 69, 74 | mp3an2 1450 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))) โ (Baseโ๐
)) |
76 | 11, 7 | ringcl 19986 |
. . . . . 6
โข ((๐
โ Ring โง
((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ, โจ2,
2โฉ})) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))) โ (Baseโ๐
)) โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐)))) โ (Baseโ๐
)) |
77 | 22, 73, 75, 76 | syl3anc 1372 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐)))) โ (Baseโ๐
)) |
78 | | 2fveq3 6848 |
. . . . . . 7
โข (๐ = {โจ1, 1โฉ, โจ2,
2โฉ} โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) = ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ, โจ2,
2โฉ}))) |
79 | | fveq1 6842 |
. . . . . . . . . 10
โข (๐ = {โจ1, 1โฉ, โจ2,
2โฉ} โ (๐โ๐) = ({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)) |
80 | 79 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = {โจ1, 1โฉ, โจ2,
2โฉ} โ ((๐โ๐)๐๐) = (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐)) |
81 | 80 | mpteq2dv 5208 |
. . . . . . . 8
โข (๐ = {โจ1, 1โฉ, โจ2,
2โฉ} โ (๐ โ
๐ โฆ ((๐โ๐)๐๐)) = (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))) |
82 | 81 | oveq2d 7374 |
. . . . . . 7
โข (๐ = {โจ1, 1โฉ, โจ2,
2โฉ} โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐)))) |
83 | 78, 82 | oveq12d 7376 |
. . . . . 6
โข (๐ = {โจ1, 1โฉ, โจ2,
2โฉ} โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ, โจ2,
2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))))) |
84 | 11, 83 | gsumsn 19736 |
. . . . 5
โข ((๐
โ Mnd โง {โจ1,
1โฉ, โจ2, 2โฉ} โ V โง (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐)))) โ (Baseโ๐
)) โ (๐
ฮฃg (๐ โ {{โจ1, 1โฉ,
โจ2, 2โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) = (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))))) |
85 | 65, 67, 77, 84 | syl3anc 1372 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐
ฮฃg (๐ โ {{โจ1, 1โฉ,
โจ2, 2โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) = (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))))) |
86 | | prex 5390 |
. . . . . 6
โข {โจ1,
2โฉ, โจ2, 1โฉ} โ V |
87 | 86 | a1i 11 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ {โจ1, 2โฉ, โจ2,
1โฉ} โ V) |
88 | 86 | prid2 4725 |
. . . . . . . . 9
โข {โจ1,
2โฉ, โจ2, 1โฉ} โ {{โจ1, 1โฉ, โจ2, 2โฉ},
{โจ1, 2โฉ, โจ2, 1โฉ}} |
89 | 88, 59 | eleqtrri 2833 |
. . . . . . . 8
โข {โจ1,
2โฉ, โจ2, 1โฉ} โ (Baseโ(SymGrpโ๐)) |
90 | 89 | a1i 11 |
. . . . . . 7
โข (๐ โ ๐ต โ {โจ1, 2โฉ, โจ2, 1โฉ}
โ (Baseโ(SymGrpโ๐))) |
91 | 4, 6, 5 | zrhpsgnelbas 21014 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ Fin โง {โจ1,
2โฉ, โจ2, 1โฉ} โ (Baseโ(SymGrpโ๐))) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) โ (Baseโ๐
)) |
92 | 17, 91 | mp3an2 1450 |
. . . . . . 7
โข ((๐
โ Ring โง {โจ1,
2โฉ, โจ2, 1โฉ} โ (Baseโ(SymGrpโ๐))) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) โ (Baseโ๐
)) |
93 | 90, 92 | sylan2 594 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) โ (Baseโ๐
)) |
94 | 15, 4, 2, 3, 8 | m2detleiblem2 21993 |
. . . . . . 7
โข ((๐
โ Ring โง {โจ1,
2โฉ, โจ2, 1โฉ} โ (Baseโ(SymGrpโ๐)) โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))) โ (Baseโ๐
)) |
95 | 89, 94 | mp3an2 1450 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))) โ (Baseโ๐
)) |
96 | 11, 7 | ringcl 19986 |
. . . . . 6
โข ((๐
โ Ring โง
((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ, โจ2,
1โฉ})) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))) โ (Baseโ๐
)) โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐)))) โ (Baseโ๐
)) |
97 | 22, 93, 95, 96 | syl3anc 1372 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐)))) โ (Baseโ๐
)) |
98 | | 2fveq3 6848 |
. . . . . . 7
โข (๐ = {โจ1, 2โฉ, โจ2,
1โฉ} โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) = ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ, โจ2,
1โฉ}))) |
99 | | fveq1 6842 |
. . . . . . . . . 10
โข (๐ = {โจ1, 2โฉ, โจ2,
1โฉ} โ (๐โ๐) = ({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)) |
100 | 99 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = {โจ1, 2โฉ, โจ2,
1โฉ} โ ((๐โ๐)๐๐) = (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐)) |
101 | 100 | mpteq2dv 5208 |
. . . . . . . 8
โข (๐ = {โจ1, 2โฉ, โจ2,
1โฉ} โ (๐ โ
๐ โฆ ((๐โ๐)๐๐)) = (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))) |
102 | 101 | oveq2d 7374 |
. . . . . . 7
โข (๐ = {โจ1, 2โฉ, โจ2,
1โฉ} โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐)))) |
103 | 98, 102 | oveq12d 7376 |
. . . . . 6
โข (๐ = {โจ1, 2โฉ, โจ2,
1โฉ} โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))) = (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ, โจ2,
1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))))) |
104 | 11, 103 | gsumsn 19736 |
. . . . 5
โข ((๐
โ Mnd โง {โจ1,
2โฉ, โจ2, 1โฉ} โ V โง (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐)))) โ (Baseโ๐
)) โ (๐
ฮฃg (๐ โ {{โจ1, 2โฉ,
โจ2, 1โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) = (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))))) |
105 | 65, 87, 97, 104 | syl3anc 1372 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐
ฮฃg (๐ โ {{โจ1, 2โฉ,
โจ2, 1โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐)))))) = (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))))) |
106 | 85, 105 | oveq12d 7376 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((๐
ฮฃg (๐ โ {{โจ1, 1โฉ,
โจ2, 2โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))(+gโ๐
)(๐
ฮฃg (๐ โ {{โจ1, 2โฉ,
โจ2, 1โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) = ((((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))))(+gโ๐
)(((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ, โจ2,
1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐)))))) |
107 | | eqidd 2734 |
. . . . . . 7
โข (๐ โ ๐ต โ {โจ1, 1โฉ, โจ2, 2โฉ}
= {โจ1, 1โฉ, โจ2, 2โฉ}) |
108 | | eqid 2733 |
. . . . . . . 8
โข
(1rโ๐
) = (1rโ๐
) |
109 | 15, 4, 5, 6, 108 | m2detleiblem5 21990 |
. . . . . . 7
โข ((๐
โ Ring โง {โจ1,
1โฉ, โจ2, 2โฉ} = {โจ1, 1โฉ, โจ2, 2โฉ}) โ
((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ, โจ2,
2โฉ})) = (1rโ๐
)) |
110 | 107, 109 | sylan2 594 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) = (1rโ๐
)) |
111 | | eqidd 2734 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ ๐ต) โ {โจ1, 1โฉ, โจ2,
2โฉ} = {โจ1, 1โฉ, โจ2, 2โฉ}) |
112 | 8, 7 | mgpplusg 19905 |
. . . . . . . 8
โข ยท =
(+gโ(mulGrpโ๐
)) |
113 | 15, 4, 2, 3, 8, 112 | m2detleiblem3 21994 |
. . . . . . 7
โข ((๐
โ Ring โง {โจ1,
1โฉ, โจ2, 2โฉ} = {โจ1, 1โฉ, โจ2, 2โฉ} โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))) = ((1๐1) ยท (2๐2))) |
114 | 22, 111, 28, 113 | syl3anc 1372 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))) = ((1๐1) ยท (2๐2))) |
115 | 110, 114 | oveq12d 7376 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐)))) = ((1rโ๐
) ยท ((1๐1) ยท (2๐2)))) |
116 | 43 | prid1 4724 |
. . . . . . . . . 10
โข 1 โ
{1, 2} |
117 | 116, 15 | eleqtrri 2833 |
. . . . . . . . 9
โข 1 โ
๐ |
118 | 117 | a1i 11 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ ๐ต) โ 1 โ ๐) |
119 | 3 | eleq2i 2826 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐ด)) |
120 | 119 | biimpi 215 |
. . . . . . . . 9
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐ด)) |
121 | 120 | adantl 483 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ (Baseโ๐ด)) |
122 | 2, 11 | matecl 21790 |
. . . . . . . 8
โข ((1
โ ๐ โง 1 โ
๐ โง ๐ โ (Baseโ๐ด)) โ (1๐1) โ (Baseโ๐
)) |
123 | 118, 118,
121, 122 | syl3anc 1372 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (1๐1) โ (Baseโ๐
)) |
124 | | prid2g 4723 |
. . . . . . . . . . 11
โข (2 โ
โ โ 2 โ {1, 2}) |
125 | 57, 124 | ax-mp 5 |
. . . . . . . . . 10
โข 2 โ
{1, 2} |
126 | 125, 15 | eleqtrri 2833 |
. . . . . . . . 9
โข 2 โ
๐ |
127 | 126 | a1i 11 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ ๐ต) โ 2 โ ๐) |
128 | 2, 11 | matecl 21790 |
. . . . . . . 8
โข ((2
โ ๐ โง 2 โ
๐ โง ๐ โ (Baseโ๐ด)) โ (2๐2) โ (Baseโ๐
)) |
129 | 127, 127,
121, 128 | syl3anc 1372 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (2๐2) โ (Baseโ๐
)) |
130 | 11, 7 | ringcl 19986 |
. . . . . . 7
โข ((๐
โ Ring โง (1๐1) โ (Baseโ๐
) โง (2๐2) โ (Baseโ๐
)) โ ((1๐1) ยท (2๐2)) โ (Baseโ๐
)) |
131 | 22, 123, 129, 130 | syl3anc 1372 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((1๐1) ยท (2๐2)) โ (Baseโ๐
)) |
132 | 11, 7, 108 | ringlidm 19997 |
. . . . . 6
โข ((๐
โ Ring โง ((1๐1) ยท (2๐2)) โ (Baseโ๐
)) โ ((1rโ๐
) ยท ((1๐1) ยท (2๐2))) = ((1๐1) ยท (2๐2))) |
133 | 131, 132 | syldan 592 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((1rโ๐
) ยท ((1๐1) ยท (2๐2))) = ((1๐1) ยท (2๐2))) |
134 | 115, 133 | eqtrd 2773 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐)))) = ((1๐1) ยท (2๐2))) |
135 | | eqidd 2734 |
. . . . . 6
โข (๐ โ ๐ต โ {โจ1, 2โฉ, โจ2, 1โฉ}
= {โจ1, 2โฉ, โจ2, 1โฉ}) |
136 | | eqid 2733 |
. . . . . . 7
โข
(invgโ๐
) = (invgโ๐
) |
137 | 15, 4, 5, 6, 108, 136 | m2detleiblem6 21991 |
. . . . . 6
โข ((๐
โ Ring โง {โจ1,
2โฉ, โจ2, 1โฉ} = {โจ1, 2โฉ, โจ2, 1โฉ}) โ
((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ, โจ2,
1โฉ})) = ((invgโ๐
)โ(1rโ๐
))) |
138 | 135, 137 | sylan2 594 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) = ((invgโ๐
)โ(1rโ๐
))) |
139 | | eqidd 2734 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ {โจ1, 2โฉ, โจ2,
1โฉ} = {โจ1, 2โฉ, โจ2, 1โฉ}) |
140 | 15, 4, 2, 3, 8, 112 | m2detleiblem4 21995 |
. . . . . 6
โข ((๐
โ Ring โง {โจ1,
2โฉ, โจ2, 1โฉ} = {โจ1, 2โฉ, โจ2, 1โฉ} โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))) = ((2๐1) ยท (1๐2))) |
141 | 22, 139, 28, 140 | syl3anc 1372 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))) = ((2๐1) ยท (1๐2))) |
142 | 138, 141 | oveq12d 7376 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ,
โจ2, 1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐)))) = (((invgโ๐
)โ(1rโ๐
)) ยท ((2๐1) ยท (1๐2)))) |
143 | 134, 142 | oveq12d 7376 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 1โฉ,
โจ2, 2โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 1โฉ, โจ2,
2โฉ}โ๐)๐๐))))(+gโ๐
)(((โคRHomโ๐
)โ((pmSgnโ๐)โ{โจ1, 2โฉ, โจ2,
1โฉ})) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ (({โจ1, 2โฉ, โจ2,
1โฉ}โ๐)๐๐))))) = (((1๐1) ยท (2๐2))(+gโ๐
)(((invgโ๐
)โ(1rโ๐
)) ยท ((2๐1) ยท (1๐2))))) |
144 | 2, 11 | matecl 21790 |
. . . . . 6
โข ((2
โ ๐ โง 1 โ
๐ โง ๐ โ (Baseโ๐ด)) โ (2๐1) โ (Baseโ๐
)) |
145 | 127, 118,
121, 144 | syl3anc 1372 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (2๐1) โ (Baseโ๐
)) |
146 | 2, 11 | matecl 21790 |
. . . . . 6
โข ((1
โ ๐ โง 2 โ
๐ โง ๐ โ (Baseโ๐ด)) โ (1๐2) โ (Baseโ๐
)) |
147 | 118, 127,
121, 146 | syl3anc 1372 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (1๐2) โ (Baseโ๐
)) |
148 | 11, 7 | ringcl 19986 |
. . . . 5
โข ((๐
โ Ring โง (2๐1) โ (Baseโ๐
) โง (1๐2) โ (Baseโ๐
)) โ ((2๐1) ยท (1๐2)) โ (Baseโ๐
)) |
149 | 22, 145, 147, 148 | syl3anc 1372 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((2๐1) ยท (1๐2)) โ (Baseโ๐
)) |
150 | | m2detleib.m |
. . . . 5
โข โ =
(-gโ๐
) |
151 | 15, 4, 5, 6, 108, 136, 7, 150 | m2detleiblem7 21992 |
. . . 4
โข ((๐
โ Ring โง ((1๐1) ยท (2๐2)) โ (Baseโ๐
) โง ((2๐1) ยท (1๐2)) โ (Baseโ๐
)) โ (((1๐1) ยท (2๐2))(+gโ๐
)(((invgโ๐
)โ(1rโ๐
)) ยท ((2๐1) ยท (1๐2)))) = (((1๐1) ยท (2๐2)) โ ((2๐1) ยท (1๐2)))) |
152 | 22, 131, 149, 151 | syl3anc 1372 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (((1๐1) ยท (2๐2))(+gโ๐
)(((invgโ๐
)โ(1rโ๐
)) ยท ((2๐1) ยท (1๐2)))) = (((1๐1) ยท (2๐2)) โ ((2๐1) ยท (1๐2)))) |
153 | 106, 143,
152 | 3eqtrd 2777 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((๐
ฮฃg (๐ โ {{โจ1, 1โฉ,
โจ2, 2โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))(+gโ๐
)(๐
ฮฃg (๐ โ {{โจ1, 2โฉ,
โจ2, 1โฉ}} โฆ (((โคRHomโ๐
)โ((pmSgnโ๐)โ๐)) ยท
((mulGrpโ๐
)
ฮฃg (๐ โ ๐ โฆ ((๐โ๐)๐๐))))))) = (((1๐1) ยท (2๐2)) โ ((2๐1) ยท (1๐2)))) |
154 | 10, 63, 153 | 3eqtrd 2777 |
1
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ทโ๐) = (((1๐1) ยท (2๐2)) โ ((2๐1) ยท (1๐2)))) |