Step | Hyp | Ref
| Expression |
1 | | scmate.k |
. . 3
โข ๐พ = (Baseโ๐
) |
2 | | scmatmat.a |
. . 3
โข ๐ด = (๐ Mat ๐
) |
3 | | scmatmat.b |
. . 3
โข ๐ต = (Baseโ๐ด) |
4 | | eqid 2733 |
. . 3
โข
(1rโ๐ด) = (1rโ๐ด) |
5 | | eqid 2733 |
. . 3
โข (
ยท๐ โ๐ด) = ( ยท๐
โ๐ด) |
6 | | scmatmat.s |
. . 3
โข ๐ = (๐ ScMat ๐
) |
7 | 1, 2, 3, 4, 5, 6 | scmatval 21876 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ = {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐( ยท๐
โ๐ด)(1rโ๐ด))}) |
8 | | simpr 486 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
9 | 8 | adantr 482 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ ๐ โ ๐ต) |
10 | | simpll 766 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ (๐ โ Fin โง ๐
โ Ring)) |
11 | 2 | matring 21815 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
12 | 3, 4 | ringidcl 19997 |
. . . . . . . . . 10
โข (๐ด โ Ring โ
(1rโ๐ด)
โ ๐ต) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ Ring) โ
(1rโ๐ด)
โ ๐ต) |
14 | 13 | adantr 482 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โ (1rโ๐ด) โ ๐ต) |
15 | 14 | anim1ci 617 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ (๐ โ ๐พ โง (1rโ๐ด) โ ๐ต)) |
16 | 1, 2, 3, 5 | matvscl 21803 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐พ โง (1rโ๐ด) โ ๐ต)) โ (๐( ยท๐
โ๐ด)(1rโ๐ด)) โ ๐ต) |
17 | 10, 15, 16 | syl2anc 585 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ (๐( ยท๐
โ๐ด)(1rโ๐ด)) โ ๐ต) |
18 | 2, 3 | eqmat 21796 |
. . . . . 6
โข ((๐ โ ๐ต โง (๐( ยท๐
โ๐ด)(1rโ๐ด)) โ ๐ต) โ (๐ = (๐( ยท๐
โ๐ด)(1rโ๐ด)) โ โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = (๐(๐( ยท๐
โ๐ด)(1rโ๐ด))๐))) |
19 | 9, 17, 18 | syl2anc 585 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ (๐ = (๐( ยท๐
โ๐ด)(1rโ๐ด)) โ โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = (๐(๐( ยท๐
โ๐ด)(1rโ๐ด))๐))) |
20 | | simplll 774 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ ๐ โ Fin) |
21 | | simpllr 775 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ ๐
โ Ring) |
22 | | simpr 486 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ ๐ โ ๐พ) |
23 | 20, 21, 22 | 3jca 1129 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐พ)) |
24 | | scmate.0 |
. . . . . . . . 9
โข 0 =
(0gโ๐
) |
25 | 2, 1, 24, 4, 5 | scmatscmide 21879 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐พ) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐( ยท๐
โ๐ด)(1rโ๐ด))๐) = if(๐ = ๐, ๐, 0 )) |
26 | 23, 25 | sylan 581 |
. . . . . . 7
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ โ ๐ต) โง ๐ โ ๐พ) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐( ยท๐
โ๐ด)(1rโ๐ด))๐) = if(๐ = ๐, ๐, 0 )) |
27 | 26 | eqeq2d 2744 |
. . . . . 6
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ โ ๐ต) โง ๐ โ ๐พ) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐๐๐) = (๐(๐( ยท๐
โ๐ด)(1rโ๐ด))๐) โ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
28 | 27 | 2ralbidva 3207 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ (โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = (๐(๐( ยท๐
โ๐ด)(1rโ๐ด))๐) โ โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
29 | 19, 28 | bitrd 279 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง ๐ โ ๐พ) โ (๐ = (๐( ยท๐
โ๐ด)(1rโ๐ด)) โ โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
30 | 29 | rexbidva 3170 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โ (โ๐ โ ๐พ ๐ = (๐( ยท๐
โ๐ด)(1rโ๐ด)) โ โ๐ โ ๐พ โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
31 | 30 | rabbidva 3413 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring) โ {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐( ยท๐
โ๐ด)(1rโ๐ด))} = {๐ โ ๐ต โฃ โ๐ โ ๐พ โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )}) |
32 | 7, 31 | eqtrd 2773 |
1
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ = {๐ โ ๐ต โฃ โ๐ โ ๐พ โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )}) |