Step | Hyp | Ref
| Expression |
1 | | marep01ma.a |
. . . . . . 7
โข ๐ด = (๐ Mat ๐
) |
2 | | marep01ma.b |
. . . . . . 7
โข ๐ต = (Baseโ๐ด) |
3 | | marep01ma.r |
. . . . . . 7
โข ๐
โ CRing |
4 | | marep01ma.0 |
. . . . . . 7
โข 0 =
(0gโ๐
) |
5 | | marep01ma.1 |
. . . . . . 7
โข 1 =
(1rโ๐
) |
6 | | smadiadetlem.p |
. . . . . . 7
โข ๐ =
(Baseโ(SymGrpโ๐)) |
7 | | smadiadetlem.g |
. . . . . . 7
โข ๐บ = (mulGrpโ๐
) |
8 | 1, 2, 3, 4, 5, 6, 7 | smadiadetlem0 22033 |
. . . . . 6
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โ (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐)))) = 0 )) |
9 | 8 | imp 408 |
. . . . 5
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โง ๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ})) โ (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐)))) = 0 ) |
10 | 9 | oveq2d 7377 |
. . . 4
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โง ๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ})) โ (((๐ โ ๐)โ๐) ยท (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐))))) = (((๐ โ ๐)โ๐) ยท 0 )) |
11 | 10 | mpteq2dva 5209 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ (((๐ โ ๐)โ๐) ยท (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐)))))) = (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ (((๐ โ ๐)โ๐) ยท 0 ))) |
12 | 11 | oveq2d 7377 |
. 2
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐
ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ (((๐ โ ๐)โ๐) ยท (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐))))))) = (๐
ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ (((๐ โ ๐)โ๐) ยท 0 )))) |
13 | | crngring 19984 |
. . . . . 6
โข (๐
โ CRing โ ๐
โ Ring) |
14 | 3, 13 | mp1i 13 |
. . . . 5
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โง ๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ})) โ ๐
โ Ring) |
15 | 1, 2 | matrcl 21782 |
. . . . . . . . 9
โข (๐ โ ๐ต โ (๐ โ Fin โง ๐
โ V)) |
16 | 15 | simpld 496 |
. . . . . . . 8
โข (๐ โ ๐ต โ ๐ โ Fin) |
17 | 16 | 3ad2ant1 1134 |
. . . . . . 7
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ ๐ โ Fin) |
18 | 17 | adantr 482 |
. . . . . 6
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โง ๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ})) โ ๐ โ Fin) |
19 | | eldifi 4090 |
. . . . . . 7
โข (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โ ๐ โ ๐) |
20 | 19 | adantl 483 |
. . . . . 6
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โง ๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ})) โ ๐ โ ๐) |
21 | | madetminlem.s |
. . . . . . 7
โข ๐ = (pmSgnโ๐) |
22 | | madetminlem.y |
. . . . . . 7
โข ๐ = (โคRHomโ๐
) |
23 | 6, 21, 22 | zrhcopsgnelbas 21022 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ Fin โง ๐ โ ๐) โ ((๐ โ ๐)โ๐) โ (Baseโ๐
)) |
24 | 14, 18, 20, 23 | syl3anc 1372 |
. . . . 5
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โง ๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ})) โ ((๐ โ ๐)โ๐) โ (Baseโ๐
)) |
25 | | eqid 2733 |
. . . . . 6
โข
(Baseโ๐
) =
(Baseโ๐
) |
26 | | madetminlem.t |
. . . . . 6
โข ยท =
(.rโ๐
) |
27 | 25, 26, 4 | ringrz 20020 |
. . . . 5
โข ((๐
โ Ring โง ((๐ โ ๐)โ๐) โ (Baseโ๐
)) โ (((๐ โ ๐)โ๐) ยท 0 ) = 0 ) |
28 | 14, 24, 27 | syl2anc 585 |
. . . 4
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โง ๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ})) โ (((๐ โ ๐)โ๐) ยท 0 ) = 0 ) |
29 | 28 | mpteq2dva 5209 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ (((๐ โ ๐)โ๐) ยท 0 )) = (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ 0 )) |
30 | 29 | oveq2d 7377 |
. 2
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐
ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ (((๐ โ ๐)โ๐) ยท 0 ))) = (๐
ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ 0 ))) |
31 | | ringmnd 19982 |
. . . 4
โข (๐
โ Ring โ ๐
โ Mnd) |
32 | 3, 13, 31 | mp2b 10 |
. . 3
โข ๐
โ Mnd |
33 | 6 | fvexi 6860 |
. . . 4
โข ๐ โ V |
34 | | difexg 5288 |
. . . 4
โข (๐ โ V โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โ V) |
35 | 33, 34 | mp1i 13 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โ V) |
36 | 4 | gsumz 18654 |
. . 3
โข ((๐
โ Mnd โง (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โ V) โ (๐
ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ 0 )) = 0 ) |
37 | 32, 35, 36 | sylancr 588 |
. 2
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐
ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ 0 )) = 0 ) |
38 | 12, 30, 37 | 3eqtrd 2777 |
1
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐
ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ (((๐ โ ๐)โ๐) ยท (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐))))))) = 0 ) |