Step | Hyp | Ref
| Expression |
1 | | fvex 6860 |
. . . . . 6
โข
(Baseโ(SymGrpโ๐)) โ V |
2 | | ovex 7395 |
. . . . . . 7
โข
((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) โ V |
3 | | eqid 2737 |
. . . . . . 7
โข (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) = (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) |
4 | 2, 3 | fnmpti 6649 |
. . . . . 6
โข (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) Fn (Baseโ(SymGrpโ๐)) |
5 | | ovex 7395 |
. . . . . . 7
โข
((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) โ V |
6 | | eqid 2737 |
. . . . . . 7
โข (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) = (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) |
7 | 5, 6 | fnmpti 6649 |
. . . . . 6
โข (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) Fn (Baseโ(SymGrpโ๐)) |
8 | | ofmpteq 7644 |
. . . . . 6
โข
(((Baseโ(SymGrpโ๐)) โ V โง (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) Fn (Baseโ(SymGrpโ๐)) โง (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) Fn (Baseโ(SymGrpโ๐))) โ ((๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) โf + (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) = (๐ โ (Baseโ(SymGrpโ๐)) โฆ
(((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) +
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) |
9 | 1, 4, 7, 8 | mp3an 1462 |
. . . . 5
โข ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) โf + (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) = (๐ โ (Baseโ(SymGrpโ๐)) โฆ
(((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) +
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) |
10 | | mdetrlin.r |
. . . . . . . . . 10
โข (๐ โ ๐
โ CRing) |
11 | | crngring 19983 |
. . . . . . . . . 10
โข (๐
โ CRing โ ๐
โ Ring) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐
โ Ring) |
13 | 12 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐
โ Ring) |
14 | | mdetrlin.y |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ ๐ต) |
15 | | mdetrlin.a |
. . . . . . . . . . . . . 14
โข ๐ด = (๐ Mat ๐
) |
16 | | mdetrlin.b |
. . . . . . . . . . . . . 14
โข ๐ต = (Baseโ๐ด) |
17 | 15, 16 | matrcl 21775 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ (๐ โ Fin โง ๐
โ V)) |
18 | 14, 17 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ Fin โง ๐
โ V)) |
19 | 18 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ Fin) |
20 | | zrhpsgnmhm 21004 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ๐ โ Fin) โ
((โคRHomโ๐
)
โ (pmSgnโ๐))
โ ((SymGrpโ๐)
MndHom (mulGrpโ๐
))) |
21 | 12, 19, 20 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((โคRHomโ๐
) โ (pmSgnโ๐)) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
))) |
22 | | eqid 2737 |
. . . . . . . . . . 11
โข
(Baseโ(SymGrpโ๐)) = (Baseโ(SymGrpโ๐)) |
23 | | eqid 2737 |
. . . . . . . . . . . 12
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
24 | | eqid 2737 |
. . . . . . . . . . . 12
โข
(Baseโ๐
) =
(Baseโ๐
) |
25 | 23, 24 | mgpbas 19909 |
. . . . . . . . . . 11
โข
(Baseโ๐
) =
(Baseโ(mulGrpโ๐
)) |
26 | 22, 25 | mhmf 18614 |
. . . . . . . . . 10
โข
(((โคRHomโ๐
) โ (pmSgnโ๐)) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
)) โ ((โคRHomโ๐
) โ (pmSgnโ๐)):(Baseโ(SymGrpโ๐))โถ(Baseโ๐
)) |
27 | 21, 26 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((โคRHomโ๐
) โ (pmSgnโ๐)):(Baseโ(SymGrpโ๐))โถ(Baseโ๐
)) |
28 | 27 | ffvelcdmda 7040 |
. . . . . . . 8
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
(((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐) โ (Baseโ๐
)) |
29 | 23 | crngmgp 19979 |
. . . . . . . . . . 11
โข (๐
โ CRing โ
(mulGrpโ๐
) โ
CMnd) |
30 | 10, 29 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (mulGrpโ๐
) โ CMnd) |
31 | 30 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (mulGrpโ๐
) โ CMnd) |
32 | 19 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐ โ Fin) |
33 | 15, 24, 16 | matbas2i 21787 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ ๐ โ ((Baseโ๐
) โm (๐ ร ๐))) |
34 | | elmapi 8794 |
. . . . . . . . . . . . 13
โข (๐ โ ((Baseโ๐
) โm (๐ ร ๐)) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
35 | 14, 33, 34 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
36 | 35 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
37 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ ๐ โ ๐) |
38 | | eqid 2737 |
. . . . . . . . . . . . . 14
โข
(SymGrpโ๐) =
(SymGrpโ๐) |
39 | 38, 22 | symgbasf 19164 |
. . . . . . . . . . . . 13
โข (๐ โ
(Baseโ(SymGrpโ๐)) โ ๐:๐โถ๐) |
40 | 39 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐:๐โถ๐) |
41 | 40 | ffvelcdmda 7040 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ (๐โ๐) โ ๐) |
42 | 36, 37, 41 | fovcdmd 7531 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ (๐๐(๐โ๐)) โ (Baseโ๐
)) |
43 | 42 | ralrimiva 3144 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ โ๐ โ ๐ (๐๐(๐โ๐)) โ (Baseโ๐
)) |
44 | 25, 31, 32, 43 | gsummptcl 19751 |
. . . . . . . 8
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
)) |
45 | | mdetrlin.z |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ ๐ต) |
46 | 15, 24, 16 | matbas2i 21787 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ ๐ โ ((Baseโ๐
) โm (๐ ร ๐))) |
47 | | elmapi 8794 |
. . . . . . . . . . . . 13
โข (๐ โ ((Baseโ๐
) โm (๐ ร ๐)) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
49 | 48 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
50 | 49, 37, 41 | fovcdmd 7531 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ (๐๐(๐โ๐)) โ (Baseโ๐
)) |
51 | 50 | ralrimiva 3144 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ โ๐ โ ๐ (๐๐(๐โ๐)) โ (Baseโ๐
)) |
52 | 25, 31, 32, 51 | gsummptcl 19751 |
. . . . . . . 8
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
)) |
53 | | mdetrlin.p |
. . . . . . . . 9
โข + =
(+gโ๐
) |
54 | | eqid 2737 |
. . . . . . . . 9
โข
(.rโ๐
) = (.rโ๐
) |
55 | 24, 53, 54 | ringdi 19994 |
. . . . . . . 8
โข ((๐
โ Ring โง
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
))) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)(((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))))) = (((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) +
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) |
56 | 13, 28, 44, 52, 55 | syl13anc 1373 |
. . . . . . 7
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)(((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))))) = (((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) +
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) |
57 | | cmnmnd 19586 |
. . . . . . . . . . . . 13
โข
((mulGrpโ๐
)
โ CMnd โ (mulGrpโ๐
) โ Mnd) |
58 | 31, 57 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (mulGrpโ๐
) โ Mnd) |
59 | | mdetrlin.i |
. . . . . . . . . . . . 13
โข (๐ โ ๐ผ โ ๐) |
60 | 59 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐ผ โ ๐) |
61 | 35 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
62 | 40, 60 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐โ๐ผ) โ ๐) |
63 | 61, 60, 62 | fovcdmd 7531 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ๐(๐โ๐ผ)) โ (Baseโ๐
)) |
64 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ผ โ ๐ = ๐ผ) |
65 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ผ โ (๐โ๐) = (๐โ๐ผ)) |
66 | 64, 65 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ = ๐ผ โ (๐๐(๐โ๐)) = (๐ผ๐(๐โ๐ผ))) |
67 | 25, 66 | gsumsn 19738 |
. . . . . . . . . . . 12
โข
(((mulGrpโ๐
)
โ Mnd โง ๐ผ โ
๐ โง (๐ผ๐(๐โ๐ผ)) โ (Baseโ๐
)) โ ((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) = (๐ผ๐(๐โ๐ผ))) |
68 | 58, 60, 63, 67 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) = (๐ผ๐(๐โ๐ผ))) |
69 | 68, 63 | eqeltrd 2838 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
)) |
70 | 48 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
71 | 70, 60, 62 | fovcdmd 7531 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ๐(๐โ๐ผ)) โ (Baseโ๐
)) |
72 | 64, 65 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ = ๐ผ โ (๐๐(๐โ๐)) = (๐ผ๐(๐โ๐ผ))) |
73 | 25, 72 | gsumsn 19738 |
. . . . . . . . . . . 12
โข
(((mulGrpโ๐
)
โ Mnd โง ๐ผ โ
๐ โง (๐ผ๐(๐โ๐ผ)) โ (Baseโ๐
)) โ ((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) = (๐ผ๐(๐โ๐ผ))) |
74 | 58, 60, 71, 73 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) = (๐ผ๐(๐โ๐ผ))) |
75 | 74, 71 | eqeltrd 2838 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
)) |
76 | | difssd 4097 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โ {๐ผ}) โ ๐) |
77 | 32, 76 | ssfid 9218 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โ {๐ผ}) โ Fin) |
78 | | eldifi 4091 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ {๐ผ}) โ ๐ โ ๐) |
79 | | mdetrlin.x |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ ๐ต) |
80 | 15, 24, 16 | matbas2i 21787 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ ๐ โ ((Baseโ๐
) โm (๐ ร ๐))) |
81 | | elmapi 8794 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((Baseโ๐
) โm (๐ ร ๐)) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
82 | 79, 80, 81 | 3syl 18 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
83 | 82 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
84 | 83, 37, 41 | fovcdmd 7531 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ ๐) โ (๐๐(๐โ๐)) โ (Baseโ๐
)) |
85 | 78, 84 | sylan2 594 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐๐(๐โ๐)) โ (Baseโ๐
)) |
86 | 85 | ralrimiva 3144 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ โ๐ โ (๐ โ {๐ผ})(๐๐(๐โ๐)) โ (Baseโ๐
)) |
87 | 25, 31, 77, 86 | gsummptcl 19751 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
)) |
88 | 24, 53, 54 | ringdir 19995 |
. . . . . . . . . 10
โข ((๐
โ Ring โง
(((mulGrpโ๐
)
ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
))) โ ((((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) = ((((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) + (((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))))) |
89 | 13, 69, 75, 87, 88 | syl13anc 1373 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
((((mulGrpโ๐
)
ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) = ((((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) + (((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))))) |
90 | 23, 54 | mgpplusg 19907 |
. . . . . . . . . . 11
โข
(.rโ๐
) = (+gโ(mulGrpโ๐
)) |
91 | | disjdif 4436 |
. . . . . . . . . . . 12
โข ({๐ผ} โฉ (๐ โ {๐ผ})) = โ
|
92 | 91 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ({๐ผ} โฉ (๐ โ {๐ผ})) = โ
) |
93 | 59 | snssd 4774 |
. . . . . . . . . . . . . 14
โข (๐ โ {๐ผ} โ ๐) |
94 | 93 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ {๐ผ} โ ๐) |
95 | | undif 4446 |
. . . . . . . . . . . . 13
โข ({๐ผ} โ ๐ โ ({๐ผ} โช (๐ โ {๐ผ})) = ๐) |
96 | 94, 95 | sylib 217 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ({๐ผ} โช (๐ โ {๐ผ})) = ๐) |
97 | 96 | eqcomd 2743 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐ = ({๐ผ} โช (๐ โ {๐ผ}))) |
98 | 25, 90, 31, 32, 84, 92, 97 | gsummptfidmsplit 19714 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) = (((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
99 | | mdetrlin.eq |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โพ ({๐ผ} ร ๐)) = ((๐ โพ ({๐ผ} ร ๐)) โf + (๐ โพ ({๐ผ} ร ๐)))) |
100 | 99 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โพ ({๐ผ} ร ๐)) = ((๐ โพ ({๐ผ} ร ๐)) โf + (๐ โพ ({๐ผ} ร ๐)))) |
101 | 100 | oveqd 7379 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = (๐ผ((๐ โพ ({๐ผ} ร ๐)) โf + (๐ โพ ({๐ผ} ร ๐)))(๐โ๐ผ))) |
102 | | xpss1 5657 |
. . . . . . . . . . . . . . . . . . 19
โข ({๐ผ} โ ๐ โ ({๐ผ} ร ๐) โ (๐ ร ๐)) |
103 | 94, 102 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ({๐ผ} ร ๐) โ (๐ ร ๐)) |
104 | 61, 103 | fssresd 6714 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โพ ({๐ผ} ร ๐)):({๐ผ} ร ๐)โถ(Baseโ๐
)) |
105 | 104 | ffnd 6674 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โพ ({๐ผ} ร ๐)) Fn ({๐ผ} ร ๐)) |
106 | 70, 103 | fssresd 6714 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โพ ({๐ผ} ร ๐)):({๐ผ} ร ๐)โถ(Baseโ๐
)) |
107 | 106 | ffnd 6674 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โพ ({๐ผ} ร ๐)) Fn ({๐ผ} ร ๐)) |
108 | | snex 5393 |
. . . . . . . . . . . . . . . . 17
โข {๐ผ} โ V |
109 | | xpexg 7689 |
. . . . . . . . . . . . . . . . 17
โข (({๐ผ} โ V โง ๐ โ Fin) โ ({๐ผ} ร ๐) โ V) |
110 | 108, 32, 109 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ({๐ผ} ร ๐) โ V) |
111 | | snidg 4625 |
. . . . . . . . . . . . . . . . . 18
โข (๐ผ โ ๐ โ ๐ผ โ {๐ผ}) |
112 | 60, 111 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐ผ โ {๐ผ}) |
113 | 112, 62 | opelxpd 5676 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ โจ๐ผ, (๐โ๐ผ)โฉ โ ({๐ผ} ร ๐)) |
114 | | fnfvof 7639 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โพ ({๐ผ} ร ๐)) Fn ({๐ผ} ร ๐) โง (๐ โพ ({๐ผ} ร ๐)) Fn ({๐ผ} ร ๐)) โง (({๐ผ} ร ๐) โ V โง โจ๐ผ, (๐โ๐ผ)โฉ โ ({๐ผ} ร ๐))) โ (((๐ โพ ({๐ผ} ร ๐)) โf + (๐ โพ ({๐ผ} ร ๐)))โโจ๐ผ, (๐โ๐ผ)โฉ) = (((๐ โพ ({๐ผ} ร ๐))โโจ๐ผ, (๐โ๐ผ)โฉ) + ((๐ โพ ({๐ผ} ร ๐))โโจ๐ผ, (๐โ๐ผ)โฉ))) |
115 | 105, 107,
110, 113, 114 | syl22anc 838 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((๐ โพ ({๐ผ} ร ๐)) โf + (๐ โพ ({๐ผ} ร ๐)))โโจ๐ผ, (๐โ๐ผ)โฉ) = (((๐ โพ ({๐ผ} ร ๐))โโจ๐ผ, (๐โ๐ผ)โฉ) + ((๐ โพ ({๐ผ} ร ๐))โโจ๐ผ, (๐โ๐ผ)โฉ))) |
116 | | df-ov 7365 |
. . . . . . . . . . . . . . 15
โข (๐ผ((๐ โพ ({๐ผ} ร ๐)) โf + (๐ โพ ({๐ผ} ร ๐)))(๐โ๐ผ)) = (((๐ โพ ({๐ผ} ร ๐)) โf + (๐ โพ ({๐ผ} ร ๐)))โโจ๐ผ, (๐โ๐ผ)โฉ) |
117 | | df-ov 7365 |
. . . . . . . . . . . . . . . 16
โข (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = ((๐ โพ ({๐ผ} ร ๐))โโจ๐ผ, (๐โ๐ผ)โฉ) |
118 | | df-ov 7365 |
. . . . . . . . . . . . . . . 16
โข (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = ((๐ โพ ({๐ผ} ร ๐))โโจ๐ผ, (๐โ๐ผ)โฉ) |
119 | 117, 118 | oveq12i 7374 |
. . . . . . . . . . . . . . 15
โข ((๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) + (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ))) = (((๐ โพ ({๐ผ} ร ๐))โโจ๐ผ, (๐โ๐ผ)โฉ) + ((๐ โพ ({๐ผ} ร ๐))โโจ๐ผ, (๐โ๐ผ)โฉ)) |
120 | 115, 116,
119 | 3eqtr4g 2802 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ((๐ โพ ({๐ผ} ร ๐)) โf + (๐ โพ ({๐ผ} ร ๐)))(๐โ๐ผ)) = ((๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) + (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)))) |
121 | 101, 120 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = ((๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) + (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)))) |
122 | | ovres 7525 |
. . . . . . . . . . . . . 14
โข ((๐ผ โ {๐ผ} โง (๐โ๐ผ) โ ๐) โ (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = (๐ผ๐(๐โ๐ผ))) |
123 | 112, 62, 122 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = (๐ผ๐(๐โ๐ผ))) |
124 | | ovres 7525 |
. . . . . . . . . . . . . . 15
โข ((๐ผ โ {๐ผ} โง (๐โ๐ผ) โ ๐) โ (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = (๐ผ๐(๐โ๐ผ))) |
125 | 112, 62, 124 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = (๐ผ๐(๐โ๐ผ))) |
126 | | ovres 7525 |
. . . . . . . . . . . . . . 15
โข ((๐ผ โ {๐ผ} โง (๐โ๐ผ) โ ๐) โ (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = (๐ผ๐(๐โ๐ผ))) |
127 | 112, 62, 126 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) = (๐ผ๐(๐โ๐ผ))) |
128 | 125, 127 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ)) + (๐ผ(๐ โพ ({๐ผ} ร ๐))(๐โ๐ผ))) = ((๐ผ๐(๐โ๐ผ)) + (๐ผ๐(๐โ๐ผ)))) |
129 | 121, 123,
128 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ๐(๐โ๐ผ)) = ((๐ผ๐(๐โ๐ผ)) + (๐ผ๐(๐โ๐ผ)))) |
130 | 82 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
131 | 130, 60, 62 | fovcdmd 7531 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ผ๐(๐โ๐ผ)) โ (Baseโ๐
)) |
132 | 64, 65 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ผ โ (๐๐(๐โ๐)) = (๐ผ๐(๐โ๐ผ))) |
133 | 25, 132 | gsumsn 19738 |
. . . . . . . . . . . . 13
โข
(((mulGrpโ๐
)
โ Mnd โง ๐ผ โ
๐ โง (๐ผ๐(๐โ๐ผ)) โ (Baseโ๐
)) โ ((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) = (๐ผ๐(๐โ๐ผ))) |
134 | 58, 60, 131, 133 | syl3anc 1372 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) = (๐ผ๐(๐โ๐ผ))) |
135 | 68, 74 | oveq12d 7380 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))) = ((๐ผ๐(๐โ๐ผ)) + (๐ผ๐(๐โ๐ผ)))) |
136 | 129, 134,
135 | 3eqtr4d 2787 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) = (((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))))) |
137 | 136 | oveq1d 7377 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) = ((((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
138 | 98, 137 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) = ((((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐)))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
139 | 25, 90, 31, 32, 42, 92, 97 | gsummptfidmsplit 19714 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) = (((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
140 | | mdetrlin.ne1 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ โพ ((๐ โ {๐ผ}) ร ๐)) = (๐ โพ ((๐ โ {๐ผ}) ร ๐))) |
141 | 140 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐ โพ ((๐ โ {๐ผ}) ร ๐)) = (๐ โพ ((๐ โ {๐ผ}) ร ๐))) |
142 | 141 | oveqd 7379 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐)) = (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐))) |
143 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ ๐ โ (๐ โ {๐ผ})) |
144 | 78, 41 | sylan2 594 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐โ๐) โ ๐) |
145 | | ovres 7525 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (๐ โ {๐ผ}) โง (๐โ๐) โ ๐) โ (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐)) = (๐๐(๐โ๐))) |
146 | 143, 144,
145 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐)) = (๐๐(๐โ๐))) |
147 | | ovres 7525 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (๐ โ {๐ผ}) โง (๐โ๐) โ ๐) โ (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐)) = (๐๐(๐โ๐))) |
148 | 143, 144,
147 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐)) = (๐๐(๐โ๐))) |
149 | 142, 146,
148 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐๐(๐โ๐)) = (๐๐(๐โ๐))) |
150 | 149 | mpteq2dva 5210 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))) = (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))) |
151 | 150 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))) = ((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) |
152 | 151 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) = (((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
153 | 139, 152 | eqtrd 2777 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) = (((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
154 | 25, 90, 31, 32, 50, 92, 97 | gsummptfidmsplit 19714 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) = (((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
155 | | mdetrlin.ne2 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ โพ ((๐ โ {๐ผ}) ร ๐)) = (๐ โพ ((๐ โ {๐ผ}) ร ๐))) |
156 | 155 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐ โพ ((๐ โ {๐ผ}) ร ๐)) = (๐ โพ ((๐ โ {๐ผ}) ร ๐))) |
157 | 156 | oveqd 7379 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐)) = (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐))) |
158 | | ovres 7525 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (๐ โ {๐ผ}) โง (๐โ๐) โ ๐) โ (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐)) = (๐๐(๐โ๐))) |
159 | 143, 144,
158 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐(๐ โพ ((๐ โ {๐ผ}) ร ๐))(๐โ๐)) = (๐๐(๐โ๐))) |
160 | 157, 146,
159 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โง ๐ โ (๐ โ {๐ผ})) โ (๐๐(๐โ๐)) = (๐๐(๐โ๐))) |
161 | 160 | mpteq2dva 5210 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))) = (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))) |
162 | 161 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))) = ((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) |
163 | 162 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) = (((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
164 | 154, 163 | eqtrd 2777 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) = (((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐)))))) |
165 | 153, 164 | oveq12d 7380 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐))))) = ((((mulGrpโ๐
) ฮฃg (๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))) + (((mulGrpโ๐
) ฮฃg
(๐ โ {๐ผ} โฆ (๐๐(๐โ๐))))(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ (๐ โ {๐ผ}) โฆ (๐๐(๐โ๐))))))) |
166 | 89, 138, 165 | 3eqtr4rd 2788 |
. . . . . . . 8
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ (((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐))))) = ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) |
167 | 166 | oveq2d 7378 |
. . . . . . 7
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)(((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))) + ((mulGrpโ๐
) ฮฃg
(๐ โ ๐ โฆ (๐๐(๐โ๐)))))) = ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) |
168 | 56, 167 | eqtr3d 2779 |
. . . . . 6
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
(((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) +
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) = ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) |
169 | 168 | mpteq2dva 5210 |
. . . . 5
โข (๐ โ (๐ โ (Baseโ(SymGrpโ๐)) โฆ
(((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) +
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) = (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) |
170 | 9, 169 | eqtrid 2789 |
. . . 4
โข (๐ โ ((๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) โf + (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) = (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) |
171 | 170 | oveq2d 7378 |
. . 3
โข (๐ โ (๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) โf + (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) |
172 | | ringcmn 20010 |
. . . . 5
โข (๐
โ Ring โ ๐
โ CMnd) |
173 | 10, 11, 172 | 3syl 18 |
. . . 4
โข (๐ โ ๐
โ CMnd) |
174 | 38, 22 | symgbasfi 19167 |
. . . . 5
โข (๐ โ Fin โ
(Baseโ(SymGrpโ๐)) โ Fin) |
175 | 19, 174 | syl 17 |
. . . 4
โข (๐ โ
(Baseโ(SymGrpโ๐)) โ Fin) |
176 | 24, 54 | ringcl 19988 |
. . . . 5
โข ((๐
โ Ring โง
(((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
)) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) โ (Baseโ๐
)) |
177 | 13, 28, 44, 176 | syl3anc 1372 |
. . . 4
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) โ (Baseโ๐
)) |
178 | 24, 54 | ringcl 19988 |
. . . . 5
โข ((๐
โ Ring โง
(((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐) โ (Baseโ๐
) โง ((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))) โ (Baseโ๐
)) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) โ (Baseโ๐
)) |
179 | 13, 28, 52, 178 | syl3anc 1372 |
. . . 4
โข ((๐ โง ๐ โ (Baseโ(SymGrpโ๐))) โ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))) โ (Baseโ๐
)) |
180 | 24, 53, 173, 175, 177, 179, 3, 6 | gsummptfidmadd2 19710 |
. . 3
โข (๐ โ (๐
ฮฃg ((๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))) โf + (๐ โ (Baseโ(SymGrpโ๐)) โฆ
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) = ((๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) + (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))))) |
181 | 171, 180 | eqtr3d 2779 |
. 2
โข (๐ โ (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) = ((๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) + (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))))) |
182 | | mdetrlin.d |
. . . 4
โข ๐ท = (๐ maDet ๐
) |
183 | | eqid 2737 |
. . . 4
โข
(โคRHomโ๐
) = (โคRHomโ๐
) |
184 | | eqid 2737 |
. . . 4
โข
(pmSgnโ๐) =
(pmSgnโ๐) |
185 | 182, 15, 16, 22, 183, 184, 54, 23 | mdetleib2 21953 |
. . 3
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) |
186 | 10, 79, 185 | syl2anc 585 |
. 2
โข (๐ โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) |
187 | 182, 15, 16, 22, 183, 184, 54, 23 | mdetleib2 21953 |
. . . 4
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) |
188 | 10, 14, 187 | syl2anc 585 |
. . 3
โข (๐ โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) |
189 | 182, 15, 16, 22, 183, 184, 54, 23 | mdetleib2 21953 |
. . . 4
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) |
190 | 10, 45, 189 | syl2anc 585 |
. . 3
โข (๐ โ (๐ทโ๐) = (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐)))))))) |
191 | 188, 190 | oveq12d 7380 |
. 2
โข (๐ โ ((๐ทโ๐) + (๐ทโ๐)) = ((๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))) + (๐
ฮฃg (๐ โ
(Baseโ(SymGrpโ๐)) โฆ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐)(.rโ๐
)((mulGrpโ๐
) ฮฃg (๐ โ ๐ โฆ (๐๐(๐โ๐))))))))) |
192 | 181, 186,
191 | 3eqtr4d 2787 |
1
โข (๐ โ (๐ทโ๐) = ((๐ทโ๐) + (๐ทโ๐))) |