Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | marep01ma.0 |
. . 3
β’ 0 =
(0gβπ
) |
3 | | eqid 2733 |
. . 3
β’
(Cntzβπ
) =
(Cntzβπ
) |
4 | | marep01ma.r |
. . . . 5
β’ π
β CRing |
5 | | crngring 19984 |
. . . . 5
β’ (π
β CRing β π
β Ring) |
6 | | ringmnd 19982 |
. . . . 5
β’ (π
β Ring β π
β Mnd) |
7 | 4, 5, 6 | mp2b 10 |
. . . 4
β’ π
β Mnd |
8 | 7 | a1i 11 |
. . 3
β’ ((π β π΅ β§ πΎ β π) β π
β Mnd) |
9 | | smadiadetlem.w |
. . . 4
β’ π =
(Baseβ(SymGrpβ(π β {πΎ}))) |
10 | | fvexd 6861 |
. . . 4
β’ ((π β π΅ β§ πΎ β π) β (Baseβ(SymGrpβ(π β {πΎ}))) β V) |
11 | 9, 10 | eqeltrid 2838 |
. . 3
β’ ((π β π΅ β§ πΎ β π) β π β V) |
12 | | marep01ma.a |
. . . 4
β’ π΄ = (π Mat π
) |
13 | | marep01ma.b |
. . . 4
β’ π΅ = (Baseβπ΄) |
14 | | marep01ma.1 |
. . . 4
β’ 1 =
(1rβπ
) |
15 | | smadiadetlem.p |
. . . 4
β’ π =
(Baseβ(SymGrpβπ)) |
16 | | smadiadetlem.g |
. . . 4
β’ πΊ = (mulGrpβπ
) |
17 | | madetminlem.y |
. . . 4
β’ π = (β€RHomβπ
) |
18 | | madetminlem.s |
. . . 4
β’ π = (pmSgnβπ) |
19 | | madetminlem.t |
. . . 4
β’ Β· =
(.rβπ
) |
20 | | smadiadetlem.z |
. . . 4
β’ π = (pmSgnβ(π β {πΎ})) |
21 | 12, 13, 4, 2, 14, 15, 16, 17, 18, 19, 9, 20 | smadiadetlem3lem1 22038 |
. . 3
β’ ((π β π΅ β§ πΎ β π) β (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))):πβΆ(Baseβπ
)) |
22 | 12, 13, 4, 2, 14, 15, 16, 17, 18, 19, 9, 20 | smadiadetlem3lem2 22039 |
. . 3
β’ ((π β π΅ β§ πΎ β π) β ran (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) β ((Cntzβπ
)βran (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))))) |
23 | | eqid 2733 |
. . . 4
β’ (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) = (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) |
24 | 12, 13 | matrcl 21782 |
. . . . . . . 8
β’ (π β π΅ β (π β Fin β§ π
β V)) |
25 | 24 | simpld 496 |
. . . . . . 7
β’ (π β π΅ β π β Fin) |
26 | 25 | adantr 482 |
. . . . . 6
β’ ((π β π΅ β§ πΎ β π) β π β Fin) |
27 | | diffi 9129 |
. . . . . 6
β’ (π β Fin β (π β {πΎ}) β Fin) |
28 | | eqid 2733 |
. . . . . . 7
β’
(SymGrpβ(π
β {πΎ})) =
(SymGrpβ(π β
{πΎ})) |
29 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(SymGrpβ(π β {πΎ}))) = (Baseβ(SymGrpβ(π β {πΎ}))) |
30 | 28, 29 | symgbasfi 19168 |
. . . . . 6
β’ ((π β {πΎ}) β Fin β
(Baseβ(SymGrpβ(π β {πΎ}))) β Fin) |
31 | 26, 27, 30 | 3syl 18 |
. . . . 5
β’ ((π β π΅ β§ πΎ β π) β (Baseβ(SymGrpβ(π β {πΎ}))) β Fin) |
32 | 9, 31 | eqeltrid 2838 |
. . . 4
β’ ((π β π΅ β§ πΎ β π) β π β Fin) |
33 | | ovexd 7396 |
. . . 4
β’ (((π β π΅ β§ πΎ β π) β§ π β π) β (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))) β V) |
34 | 2 | fvexi 6860 |
. . . . 5
β’ 0 β
V |
35 | 34 | a1i 11 |
. . . 4
β’ ((π β π΅ β§ πΎ β π) β 0 β V) |
36 | 23, 32, 33, 35 | fsuppmptdm 9324 |
. . 3
β’ ((π β π΅ β§ πΎ β π) β (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) finSupp 0 ) |
37 | | fveq1 6845 |
. . . . . . 7
β’ (π = π β (πβπΎ) = (πβπΎ)) |
38 | 37 | eqeq1d 2735 |
. . . . . 6
β’ (π = π β ((πβπΎ) = πΎ β (πβπΎ) = πΎ)) |
39 | 38 | cbvrabv 3416 |
. . . . 5
β’ {π β π β£ (πβπΎ) = πΎ} = {π β π β£ (πβπΎ) = πΎ} |
40 | | eqid 2733 |
. . . . 5
β’ (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ}))) = (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ}))) |
41 | 15, 39, 9, 40 | symgfixf1o 19230 |
. . . 4
β’ ((π β Fin β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ}))):{π β π β£ (πβπΎ) = πΎ}β1-1-ontoβπ) |
42 | 25, 41 | sylan 581 |
. . 3
β’ ((π β π΅ β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ}))):{π β π β£ (πβπΎ) = πΎ}β1-1-ontoβπ) |
43 | 1, 2, 3, 8, 11, 21, 22, 36, 42 | gsumzf1o 19697 |
. 2
β’ ((π β π΅ β§ πΎ β π) β (π
Ξ£g (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))))) = (π
Ξ£g ((π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) β (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ})))))) |
44 | | eqid 2733 |
. . . . . . 7
β’ {π β π β£ (πβπΎ) = πΎ} = {π β π β£ (πβπΎ) = πΎ} |
45 | | eqid 2733 |
. . . . . . 7
β’ (π β {πΎ}) = (π β {πΎ}) |
46 | 15, 44, 9, 45 | symgfixelsi 19225 |
. . . . . 6
β’ ((πΎ β π β§ π β {π β π β£ (πβπΎ) = πΎ}) β (π βΎ (π β {πΎ})) β π) |
47 | 46 | adantll 713 |
. . . . 5
β’ (((π β π΅ β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β (π βΎ (π β {πΎ})) β π) |
48 | | eqidd 2734 |
. . . . 5
β’ ((π β π΅ β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ}))) = (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ})))) |
49 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π¦ β ((π β π)βπ) = ((π β π)βπ¦)) |
50 | | fveq1 6845 |
. . . . . . . . . . 11
β’ (π = π¦ β (πβπ) = (π¦βπ)) |
51 | 50 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π = π¦ β (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)) = (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ))) |
52 | 51 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π = π¦ β (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))) = (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ)))) |
53 | 52 | oveq2d 7377 |
. . . . . . . 8
β’ (π = π¦ β (πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))) = (πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ))))) |
54 | 49, 53 | oveq12d 7379 |
. . . . . . 7
β’ (π = π¦ β (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))) = (((π β π)βπ¦)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ)))))) |
55 | 54 | cbvmptv 5222 |
. . . . . 6
β’ (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) = (π¦ β π β¦ (((π β π)βπ¦)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ)))))) |
56 | 55 | a1i 11 |
. . . . 5
β’ ((π β π΅ β§ πΎ β π) β (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) = (π¦ β π β¦ (((π β π)βπ¦)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ))))))) |
57 | | fveq2 6846 |
. . . . . 6
β’ (π¦ = (π βΎ (π β {πΎ})) β ((π β π)βπ¦) = ((π β π)β(π βΎ (π β {πΎ})))) |
58 | | fveq1 6845 |
. . . . . . . . . 10
β’ (π¦ = (π βΎ (π β {πΎ})) β (π¦βπ) = ((π βΎ (π β {πΎ}))βπ)) |
59 | | fvres 6865 |
. . . . . . . . . 10
β’ (π β (π β {πΎ}) β ((π βΎ (π β {πΎ}))βπ) = (πβπ)) |
60 | 58, 59 | sylan9eq 2793 |
. . . . . . . . 9
β’ ((π¦ = (π βΎ (π β {πΎ})) β§ π β (π β {πΎ})) β (π¦βπ) = (πβπ)) |
61 | 60 | oveq2d 7377 |
. . . . . . . 8
β’ ((π¦ = (π βΎ (π β {πΎ})) β§ π β (π β {πΎ})) β (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ)) = (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))) |
62 | 61 | mpteq2dva 5209 |
. . . . . . 7
β’ (π¦ = (π βΎ (π β {πΎ})) β (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ))) = (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))) |
63 | 62 | oveq2d 7377 |
. . . . . 6
β’ (π¦ = (π βΎ (π β {πΎ})) β (πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ)))) = (πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))) |
64 | 57, 63 | oveq12d 7379 |
. . . . 5
β’ (π¦ = (π βΎ (π β {πΎ})) β (((π β π)βπ¦)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(π¦βπ))))) = (((π β π)β(π βΎ (π β {πΎ})))(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) |
65 | 47, 48, 56, 64 | fmptco 7079 |
. . . 4
β’ ((π β π΅ β§ πΎ β π) β ((π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) β (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ})))) = (π β {π β π β£ (πβπΎ) = πΎ} β¦ (((π β π)β(π βΎ (π β {πΎ})))(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))))) |
66 | 15, 18, 20 | copsgndif 21030 |
. . . . . . . 8
β’ ((π β Fin β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β ((π β π)β(π βΎ (π β {πΎ}))) = ((π β π)βπ))) |
67 | 25, 66 | sylan 581 |
. . . . . . 7
β’ ((π β π΅ β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β ((π β π)β(π βΎ (π β {πΎ}))) = ((π β π)βπ))) |
68 | 67 | imp 408 |
. . . . . 6
β’ (((π β π΅ β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β π)β(π βΎ (π β {πΎ}))) = ((π β π)βπ)) |
69 | 68 | oveq1d 7376 |
. . . . 5
β’ (((π β π΅ β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β (((π β π)β(π βΎ (π β {πΎ})))(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))) = (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) |
70 | 69 | mpteq2dva 5209 |
. . . 4
β’ ((π β π΅ β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β¦ (((π β π)β(π βΎ (π β {πΎ})))(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) = (π β {π β π β£ (πβπΎ) = πΎ} β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))))) |
71 | 65, 70 | eqtrd 2773 |
. . 3
β’ ((π β π΅ β§ πΎ β π) β ((π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) β (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ})))) = (π β {π β π β£ (πβπΎ) = πΎ} β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))))) |
72 | 71 | oveq2d 7377 |
. 2
β’ ((π β π΅ β§ πΎ β π) β (π
Ξ£g ((π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))) β (π β {π β π β£ (πβπΎ) = πΎ} β¦ (π βΎ (π β {πΎ}))))) = (π
Ξ£g (π β {π β π β£ (πβπΎ) = πΎ} β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))))) |
73 | 43, 72 | eqtr2d 2774 |
1
β’ ((π β π΅ β§ πΎ β π) β (π
Ξ£g (π β {π β π β£ (πβπΎ) = πΎ} β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ))))))) = (π
Ξ£g (π β π β¦ (((π β π)βπ)(.rβπ
)(πΊ Ξ£g (π β (π β {πΎ}) β¦ (π(π β (π β {πΎ}), π β (π β {πΎ}) β¦ (πππ))(πβπ)))))))) |