Step | Hyp | Ref
| Expression |
1 | | mdetfval.d |
. . . 4
โข ๐ท = (๐ maDet ๐
) |
2 | | mdetfval.a |
. . . 4
โข ๐ด = (๐ Mat ๐
) |
3 | | mdetfval.b |
. . . 4
โข ๐ต = (Baseโ๐ด) |
4 | | mdetfval.p |
. . . 4
โข ๐ =
(Baseโ(SymGrpโ๐)) |
5 | | mdetfval.y |
. . . 4
โข ๐ = (โคRHomโ๐
) |
6 | | mdetfval.s |
. . . 4
โข ๐ = (pmSgnโ๐) |
7 | | mdetfval.t |
. . . 4
โข ยท =
(.rโ๐
) |
8 | | mdetfval.u |
. . . 4
โข ๐ = (mulGrpโ๐
) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib 21959 |
. . 3
โข (๐ โ ๐ต โ (๐ทโ๐) = (๐
ฮฃg (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))))) |
10 | 9 | adantl 483 |
. 2
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐
ฮฃg (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))))) |
11 | | eqid 2733 |
. . 3
โข
(Baseโ๐
) =
(Baseโ๐
) |
12 | | crngring 19984 |
. . . . 5
โข (๐
โ CRing โ ๐
โ Ring) |
13 | | ringcmn 20011 |
. . . . 5
โข (๐
โ Ring โ ๐
โ CMnd) |
14 | 12, 13 | syl 17 |
. . . 4
โข (๐
โ CRing โ ๐
โ CMnd) |
15 | 14 | adantr 482 |
. . 3
โข ((๐
โ CRing โง ๐ โ ๐ต) โ ๐
โ CMnd) |
16 | 2, 3 | matrcl 21782 |
. . . . . 6
โข (๐ โ ๐ต โ (๐ โ Fin โง ๐
โ V)) |
17 | 16 | adantl 483 |
. . . . 5
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ Fin โง ๐
โ V)) |
18 | 17 | simpld 496 |
. . . 4
โข ((๐
โ CRing โง ๐ โ ๐ต) โ ๐ โ Fin) |
19 | | eqid 2733 |
. . . . 5
โข
(SymGrpโ๐) =
(SymGrpโ๐) |
20 | 19, 4 | symgbasfi 19168 |
. . . 4
โข (๐ โ Fin โ ๐ โ Fin) |
21 | 18, 20 | syl 17 |
. . 3
โข ((๐
โ CRing โง ๐ โ ๐ต) โ ๐ โ Fin) |
22 | 12 | ad2antrr 725 |
. . . . 5
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐
โ Ring) |
23 | 5, 6 | coeq12i 5823 |
. . . . . . . . 9
โข (๐ โ ๐) = ((โคRHomโ๐
) โ (pmSgnโ๐)) |
24 | | zrhpsgnmhm 21011 |
. . . . . . . . 9
โข ((๐
โ Ring โง ๐ โ Fin) โ
((โคRHomโ๐
)
โ (pmSgnโ๐))
โ ((SymGrpโ๐)
MndHom (mulGrpโ๐
))) |
25 | 23, 24 | eqeltrid 2838 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ Fin) โ (๐ โ ๐) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
))) |
26 | 12, 18, 25 | syl2an2r 684 |
. . . . . . 7
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ ๐) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
))) |
27 | | eqid 2733 |
. . . . . . . . 9
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
28 | 27, 11 | mgpbas 19910 |
. . . . . . . 8
โข
(Baseโ๐
) =
(Baseโ(mulGrpโ๐
)) |
29 | 4, 28 | mhmf 18615 |
. . . . . . 7
โข ((๐ โ ๐) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
)) โ (๐ โ ๐):๐โถ(Baseโ๐
)) |
30 | 26, 29 | syl 17 |
. . . . . 6
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ ๐):๐โถ(Baseโ๐
)) |
31 | 30 | ffvelcdmda 7039 |
. . . . 5
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ((๐ โ ๐)โ๐) โ (Baseโ๐
)) |
32 | 8, 11 | mgpbas 19910 |
. . . . . 6
โข
(Baseโ๐
) =
(Baseโ๐) |
33 | 8 | crngmgp 19980 |
. . . . . . 7
โข (๐
โ CRing โ ๐ โ CMnd) |
34 | 33 | ad2antrr 725 |
. . . . . 6
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐ โ CMnd) |
35 | 18 | adantr 482 |
. . . . . 6
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐ โ Fin) |
36 | | simpr 486 |
. . . . . . . . . 10
โข ((๐
โ CRing โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
37 | 2, 11, 3 | matbas2i 21794 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ ๐ โ ((Baseโ๐
) โm (๐ ร ๐))) |
38 | | elmapi 8793 |
. . . . . . . . . 10
โข (๐ โ ((Baseโ๐
) โm (๐ ร ๐)) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . . 9
โข ((๐
โ CRing โง ๐ โ ๐ต) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
40 | 39 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
41 | 19, 4 | symgbasf1o 19164 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ ๐:๐โ1-1-ontoโ๐) |
42 | 41 | adantl 483 |
. . . . . . . . . 10
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐:๐โ1-1-ontoโ๐) |
43 | | f1of 6788 |
. . . . . . . . . 10
โข (๐:๐โ1-1-ontoโ๐ โ ๐:๐โถ๐) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐:๐โถ๐) |
45 | 44 | ffvelcdmda 7039 |
. . . . . . . 8
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ (๐โ๐ฆ) โ ๐) |
46 | | simpr 486 |
. . . . . . . 8
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ ๐ฆ โ ๐) |
47 | 40, 45, 46 | fovcdmd 7530 |
. . . . . . 7
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ ((๐โ๐ฆ)๐๐ฆ) โ (Baseโ๐
)) |
48 | 47 | ralrimiva 3140 |
. . . . . 6
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ โ๐ฆ โ ๐ ((๐โ๐ฆ)๐๐ฆ) โ (Baseโ๐
)) |
49 | 32, 34, 35, 48 | gsummptcl 19752 |
. . . . 5
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))) โ (Baseโ๐
)) |
50 | 11, 7 | ringcl 19989 |
. . . . 5
โข ((๐
โ Ring โง ((๐ โ ๐)โ๐) โ (Baseโ๐
) โง (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))) โ (Baseโ๐
)) โ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ)))) โ (Baseโ๐
)) |
51 | 22, 31, 49, 50 | syl3anc 1372 |
. . . 4
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ)))) โ (Baseโ๐
)) |
52 | 51 | ralrimiva 3140 |
. . 3
โข ((๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ ๐ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ)))) โ (Baseโ๐
)) |
53 | | eqid 2733 |
. . 3
โข (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))) = (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))) |
54 | | eqid 2733 |
. . . 4
โข
(invgโ(SymGrpโ๐)) =
(invgโ(SymGrpโ๐)) |
55 | 19 | symggrp 19190 |
. . . . 5
โข (๐ โ Fin โ
(SymGrpโ๐) โ
Grp) |
56 | 18, 55 | syl 17 |
. . . 4
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (SymGrpโ๐) โ Grp) |
57 | 4, 54, 56 | grpinvf1o 18825 |
. . 3
โข ((๐
โ CRing โง ๐ โ ๐ต) โ
(invgโ(SymGrpโ๐)):๐โ1-1-ontoโ๐) |
58 | 11, 15, 21, 52, 53, 57 | gsummptfif1o 19753 |
. 2
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐
ฮฃg (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ)))))) = (๐
ฮฃg ((๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))) โ
(invgโ(SymGrpโ๐))))) |
59 | | f1of 6788 |
. . . . . . 7
โข
((invgโ(SymGrpโ๐)):๐โ1-1-ontoโ๐ โ
(invgโ(SymGrpโ๐)):๐โถ๐) |
60 | 57, 59 | syl 17 |
. . . . . 6
โข ((๐
โ CRing โง ๐ โ ๐ต) โ
(invgโ(SymGrpโ๐)):๐โถ๐) |
61 | 60 | ffvelcdmda 7039 |
. . . . 5
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ
((invgโ(SymGrpโ๐))โ๐) โ ๐) |
62 | 60 | feqmptd 6914 |
. . . . 5
โข ((๐
โ CRing โง ๐ โ ๐ต) โ
(invgโ(SymGrpโ๐)) = (๐ โ ๐ โฆ
((invgโ(SymGrpโ๐))โ๐))) |
63 | | eqidd 2734 |
. . . . 5
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))) = (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ)))))) |
64 | | fveq2 6846 |
. . . . . 6
โข (๐ =
((invgโ(SymGrpโ๐))โ๐) โ ((๐ โ ๐)โ๐) = ((๐ โ ๐)โ((invgโ(SymGrpโ๐))โ๐))) |
65 | | fveq1 6845 |
. . . . . . . . 9
โข (๐ =
((invgโ(SymGrpโ๐))โ๐) โ (๐โ๐ฆ) =
(((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)) |
66 | 65 | oveq1d 7376 |
. . . . . . . 8
โข (๐ =
((invgโ(SymGrpโ๐))โ๐) โ ((๐โ๐ฆ)๐๐ฆ) =
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)) |
67 | 66 | mpteq2dv 5211 |
. . . . . . 7
โข (๐ =
((invgโ(SymGrpโ๐))โ๐) โ (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ)) = (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ))) |
68 | 67 | oveq2d 7377 |
. . . . . 6
โข (๐ =
((invgโ(SymGrpโ๐))โ๐) โ (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))) = (๐ ฮฃg (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)))) |
69 | 64, 68 | oveq12d 7379 |
. . . . 5
โข (๐ =
((invgโ(SymGrpโ๐))โ๐) โ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ)))) = (((๐ โ ๐)โ((invgโ(SymGrpโ๐))โ๐)) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ))))) |
70 | 61, 62, 63, 69 | fmptco 7079 |
. . . 4
โข ((๐
โ CRing โง ๐ โ ๐ต) โ ((๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))) โ
(invgโ(SymGrpโ๐))) = (๐ โ ๐ โฆ (((๐ โ ๐)โ((invgโ(SymGrpโ๐))โ๐)) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)))))) |
71 | 19, 4, 54 | symginv 19192 |
. . . . . . . . 9
โข (๐ โ ๐ โ
((invgโ(SymGrpโ๐))โ๐) = โก๐) |
72 | 71 | adantl 483 |
. . . . . . . 8
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ
((invgโ(SymGrpโ๐))โ๐) = โก๐) |
73 | 72 | fveq2d 6850 |
. . . . . . 7
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ((๐ โ ๐)โ((invgโ(SymGrpโ๐))โ๐)) = ((๐ โ ๐)โโก๐)) |
74 | 12 | ad2antrr 725 |
. . . . . . . 8
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐
โ Ring) |
75 | 18 | adantr 482 |
. . . . . . . 8
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐ โ Fin) |
76 | | simpr 486 |
. . . . . . . 8
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐ โ ๐) |
77 | 4, 5, 6 | zrhpsgninv 21012 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ Fin โง ๐ โ ๐) โ ((๐ โ ๐)โโก๐) = ((๐ โ ๐)โ๐)) |
78 | 74, 75, 76, 77 | syl3anc 1372 |
. . . . . . 7
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ((๐ โ ๐)โโก๐) = ((๐ โ ๐)โ๐)) |
79 | 73, 78 | eqtrd 2773 |
. . . . . 6
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ((๐ โ ๐)โ((invgโ(SymGrpโ๐))โ๐)) = ((๐ โ ๐)โ๐)) |
80 | | eqid 2733 |
. . . . . . . 8
โข
(Baseโ๐) =
(Baseโ๐) |
81 | 33 | ad2antrr 725 |
. . . . . . . 8
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐ โ CMnd) |
82 | 39 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ ๐:(๐ ร ๐)โถ(Baseโ๐
)) |
83 | 71 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ
((invgโ(SymGrpโ๐))โ๐) = โก๐) |
84 | 83 | fveq1d 6848 |
. . . . . . . . . . . 12
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ
(((invgโ(SymGrpโ๐))โ๐)โ๐ฆ) = (โก๐โ๐ฆ)) |
85 | 19, 4 | symgbasf1o 19164 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ ๐:๐โ1-1-ontoโ๐) |
86 | 85 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐:๐โ1-1-ontoโ๐) |
87 | | f1ocnv 6800 |
. . . . . . . . . . . . . 14
โข (๐:๐โ1-1-ontoโ๐ โ โก๐:๐โ1-1-ontoโ๐) |
88 | | f1of 6788 |
. . . . . . . . . . . . . 14
โข (โก๐:๐โ1-1-ontoโ๐ โ โก๐:๐โถ๐) |
89 | 86, 87, 88 | 3syl 18 |
. . . . . . . . . . . . 13
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ โก๐:๐โถ๐) |
90 | 89 | ffvelcdmda 7039 |
. . . . . . . . . . . 12
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ (โก๐โ๐ฆ) โ ๐) |
91 | 84, 90 | eqeltrd 2834 |
. . . . . . . . . . 11
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ
(((invgโ(SymGrpโ๐))โ๐)โ๐ฆ) โ ๐) |
92 | | simpr 486 |
. . . . . . . . . . 11
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ ๐ฆ โ ๐) |
93 | 82, 91, 92 | fovcdmd 7530 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ) โ (Baseโ๐
)) |
94 | 93, 32 | eleqtrdi 2844 |
. . . . . . . . 9
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฆ โ ๐) โ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ) โ (Baseโ๐)) |
95 | 94 | ralrimiva 3140 |
. . . . . . . 8
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ โ๐ฆ โ ๐
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ) โ (Baseโ๐)) |
96 | | eqid 2733 |
. . . . . . . 8
โข (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)) = (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)) |
97 | 80, 81, 75, 95, 96, 86 | gsummptfif1o 19753 |
. . . . . . 7
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ (๐ ฮฃg (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ))) = (๐ ฮฃg ((๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)) โ ๐))) |
98 | | f1of 6788 |
. . . . . . . . . . . 12
โข (๐:๐โ1-1-ontoโ๐ โ ๐:๐โถ๐) |
99 | 86, 98 | syl 17 |
. . . . . . . . . . 11
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐:๐โถ๐) |
100 | 99 | ffvelcdmda 7039 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฅ โ ๐) โ (๐โ๐ฅ) โ ๐) |
101 | 99 | feqmptd 6914 |
. . . . . . . . . 10
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ๐ = (๐ฅ โ ๐ โฆ (๐โ๐ฅ))) |
102 | | eqidd 2734 |
. . . . . . . . . 10
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)) = (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ))) |
103 | | fveq2 6846 |
. . . . . . . . . . 11
โข (๐ฆ = (๐โ๐ฅ) โ
(((invgโ(SymGrpโ๐))โ๐)โ๐ฆ) =
(((invgโ(SymGrpโ๐))โ๐)โ(๐โ๐ฅ))) |
104 | | id 22 |
. . . . . . . . . . 11
โข (๐ฆ = (๐โ๐ฅ) โ ๐ฆ = (๐โ๐ฅ)) |
105 | 103, 104 | oveq12d 7379 |
. . . . . . . . . 10
โข (๐ฆ = (๐โ๐ฅ) โ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ) =
((((invgโ(SymGrpโ๐))โ๐)โ(๐โ๐ฅ))๐(๐โ๐ฅ))) |
106 | 100, 101,
102, 105 | fmptco 7079 |
. . . . . . . . 9
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ((๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)) โ ๐) = (๐ฅ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ(๐โ๐ฅ))๐(๐โ๐ฅ)))) |
107 | 71 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฅ โ ๐) โ
((invgโ(SymGrpโ๐))โ๐) = โก๐) |
108 | 107 | fveq1d 6848 |
. . . . . . . . . . . 12
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฅ โ ๐) โ
(((invgโ(SymGrpโ๐))โ๐)โ(๐โ๐ฅ)) = (โก๐โ(๐โ๐ฅ))) |
109 | | f1ocnvfv1 7226 |
. . . . . . . . . . . . 13
โข ((๐:๐โ1-1-ontoโ๐ โง ๐ฅ โ ๐) โ (โก๐โ(๐โ๐ฅ)) = ๐ฅ) |
110 | 86, 109 | sylan 581 |
. . . . . . . . . . . 12
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฅ โ ๐) โ (โก๐โ(๐โ๐ฅ)) = ๐ฅ) |
111 | 108, 110 | eqtrd 2773 |
. . . . . . . . . . 11
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฅ โ ๐) โ
(((invgโ(SymGrpโ๐))โ๐)โ(๐โ๐ฅ)) = ๐ฅ) |
112 | 111 | oveq1d 7376 |
. . . . . . . . . 10
โข ((((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โง ๐ฅ โ ๐) โ
((((invgโ(SymGrpโ๐))โ๐)โ(๐โ๐ฅ))๐(๐โ๐ฅ)) = (๐ฅ๐(๐โ๐ฅ))) |
113 | 112 | mpteq2dva 5209 |
. . . . . . . . 9
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ (๐ฅ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ(๐โ๐ฅ))๐(๐โ๐ฅ))) = (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ)))) |
114 | 106, 113 | eqtrd 2773 |
. . . . . . . 8
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ ((๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)) โ ๐) = (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ)))) |
115 | 114 | oveq2d 7377 |
. . . . . . 7
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ (๐ ฮฃg ((๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)) โ ๐)) = (๐ ฮฃg (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ))))) |
116 | 97, 115 | eqtrd 2773 |
. . . . . 6
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ (๐ ฮฃg (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ))) = (๐ ฮฃg (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ))))) |
117 | 79, 116 | oveq12d 7379 |
. . . . 5
โข (((๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ ๐) โ (((๐ โ ๐)โ((invgโ(SymGrpโ๐))โ๐)) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ)))) = (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ)))))) |
118 | 117 | mpteq2dva 5209 |
. . . 4
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ ๐ โฆ (((๐ โ ๐)โ((invgโ(SymGrpโ๐))โ๐)) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ
((((invgโ(SymGrpโ๐))โ๐)โ๐ฆ)๐๐ฆ))))) = (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ))))))) |
119 | 70, 118 | eqtrd 2773 |
. . 3
โข ((๐
โ CRing โง ๐ โ ๐ต) โ ((๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))) โ
(invgโ(SymGrpโ๐))) = (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ))))))) |
120 | 119 | oveq2d 7377 |
. 2
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐
ฮฃg ((๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฆ โ ๐ โฆ ((๐โ๐ฆ)๐๐ฆ))))) โ
(invgโ(SymGrpโ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ)))))))) |
121 | 10, 58, 120 | 3eqtrd 2777 |
1
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐
ฮฃg (๐ โ ๐ โฆ (((๐ โ ๐)โ๐) ยท (๐ ฮฃg (๐ฅ โ ๐ โฆ (๐ฅ๐(๐โ๐ฅ)))))))) |