Step | Hyp | Ref
| Expression |
1 | | mdetero.d |
. . 3
โข ๐ท = (๐ maDet ๐
) |
2 | | mdetero.k |
. . 3
โข ๐พ = (Baseโ๐
) |
3 | | mdetero.p |
. . 3
โข + =
(+gโ๐
) |
4 | | mdetero.r |
. . 3
โข (๐ โ ๐
โ CRing) |
5 | | mdetero.n |
. . 3
โข (๐ โ ๐ โ Fin) |
6 | | mdetero.x |
. . . 4
โข ((๐ โง ๐ โ ๐) โ ๐ โ ๐พ) |
7 | 6 | 3adant2 1132 |
. . 3
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐พ) |
8 | | crngring 19984 |
. . . . . 6
โข (๐
โ CRing โ ๐
โ Ring) |
9 | 4, 8 | syl 17 |
. . . . 5
โข (๐ โ ๐
โ Ring) |
10 | 9 | 3ad2ant1 1134 |
. . . 4
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐
โ Ring) |
11 | | mdetero.w |
. . . . 5
โข (๐ โ ๐ โ ๐พ) |
12 | 11 | 3ad2ant1 1134 |
. . . 4
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐พ) |
13 | | mdetero.y |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ๐ โ ๐พ) |
14 | 13 | 3adant2 1132 |
. . . 4
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐พ) |
15 | | mdetero.t |
. . . . 5
โข ยท =
(.rโ๐
) |
16 | 2, 15 | ringcl 19989 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐พ โง ๐ โ ๐พ) โ (๐ ยท ๐) โ ๐พ) |
17 | 10, 12, 14, 16 | syl3anc 1372 |
. . 3
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐พ) |
18 | | mdetero.z |
. . . 4
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐พ) |
19 | 14, 18 | ifcld 4536 |
. . 3
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ฝ, ๐, ๐) โ ๐พ) |
20 | | mdetero.i |
. . 3
โข (๐ โ ๐ผ โ ๐) |
21 | 1, 2, 3, 4, 5, 7, 17, 19, 20 | mdetrlin2 21979 |
. 2
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, (๐ + (๐ ยท ๐)), if(๐ = ๐ฝ, ๐, ๐)))) = ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, (๐ ยท ๐), if(๐ = ๐ฝ, ๐, ๐)))))) |
22 | 1, 2, 15, 4, 5, 14, 19, 11, 20 | mdetrsca2 21976 |
. . . 4
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, (๐ ยท ๐), if(๐ = ๐ฝ, ๐, ๐)))) = (๐ ยท (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))))) |
23 | | eqid 2733 |
. . . . . 6
โข
(0gโ๐
) = (0gโ๐
) |
24 | | mdetero.j |
. . . . . 6
โข (๐ โ ๐ฝ โ ๐) |
25 | | mdetero.ij |
. . . . . 6
โข (๐ โ ๐ผ โ ๐ฝ) |
26 | 1, 2, 23, 4, 5, 13, 18, 20, 24, 25 | mdetralt2 21981 |
. . . . 5
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))) = (0gโ๐
)) |
27 | 26 | oveq2d 7377 |
. . . 4
โข (๐ โ (๐ ยท (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐))))) = (๐ ยท
(0gโ๐
))) |
28 | 2, 15, 23 | ringrz 20020 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐พ) โ (๐ ยท
(0gโ๐
)) =
(0gโ๐
)) |
29 | 9, 11, 28 | syl2anc 585 |
. . . 4
โข (๐ โ (๐ ยท
(0gโ๐
)) =
(0gโ๐
)) |
30 | 22, 27, 29 | 3eqtrd 2777 |
. . 3
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, (๐ ยท ๐), if(๐ = ๐ฝ, ๐, ๐)))) = (0gโ๐
)) |
31 | 30 | oveq2d 7377 |
. 2
โข (๐ โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, (๐ ยท ๐), if(๐ = ๐ฝ, ๐, ๐))))) = ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))) + (0gโ๐
))) |
32 | | ringgrp 19977 |
. . . 4
โข (๐
โ Ring โ ๐
โ Grp) |
33 | 9, 32 | syl 17 |
. . 3
โข (๐ โ ๐
โ Grp) |
34 | | eqid 2733 |
. . . . . 6
โข (๐ Mat ๐
) = (๐ Mat ๐
) |
35 | | eqid 2733 |
. . . . . 6
โข
(Baseโ(๐ Mat
๐
)) = (Baseโ(๐ Mat ๐
)) |
36 | 1, 34, 35, 2 | mdetf 21967 |
. . . . 5
โข (๐
โ CRing โ ๐ท:(Baseโ(๐ Mat ๐
))โถ๐พ) |
37 | 4, 36 | syl 17 |
. . . 4
โข (๐ โ ๐ท:(Baseโ(๐ Mat ๐
))โถ๐พ) |
38 | 7, 19 | ifcld 4536 |
. . . . 5
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)) โ ๐พ) |
39 | 34, 2, 35, 5, 4, 38 | matbas2d 21795 |
. . . 4
โข (๐ โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐))) โ (Baseโ(๐ Mat ๐
))) |
40 | 37, 39 | ffvelcdmd 7040 |
. . 3
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))) โ ๐พ) |
41 | 2, 3, 23 | grprid 18789 |
. . 3
โข ((๐
โ Grp โง (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))) โ ๐พ) โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))) + (0gโ๐
)) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐))))) |
42 | 33, 40, 41 | syl2anc 585 |
. 2
โข (๐ โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐)))) + (0gโ๐
)) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐))))) |
43 | 21, 31, 42 | 3eqtrd 2777 |
1
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, (๐ + (๐ ยท ๐)), if(๐ = ๐ฝ, ๐, ๐)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ผ, ๐, if(๐ = ๐ฝ, ๐, ๐))))) |