Step | Hyp | Ref
| Expression |
1 | | simprl 769 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ท)) โ ๐ถ โ ๐พ) |
2 | | dmatscmcl.a |
. . . . . . . 8
โข ๐ด = (๐ Mat ๐
) |
3 | | dmatscmcl.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐ด) |
4 | | eqid 2732 |
. . . . . . . 8
โข
(0gโ๐
) = (0gโ๐
) |
5 | | dmatscmcl.d |
. . . . . . . 8
โข ๐ท = (๐ DMat ๐
) |
6 | 2, 3, 4, 5 | dmatmat 21995 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐ โ ๐ท โ ๐ โ ๐ต)) |
7 | 6 | com12 32 |
. . . . . 6
โข (๐ โ ๐ท โ ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ ๐ต)) |
8 | 7 | adantl 482 |
. . . . 5
โข ((๐ถ โ ๐พ โง ๐ โ ๐ท) โ ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ ๐ต)) |
9 | 8 | impcom 408 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ท)) โ ๐ โ ๐ต) |
10 | 1, 9 | jca 512 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ท)) โ (๐ถ โ ๐พ โง ๐ โ ๐ต)) |
11 | | dmatscmcl.k |
. . . 4
โข ๐พ = (Baseโ๐
) |
12 | | dmatscmcl.s |
. . . 4
โข โ = (
ยท๐ โ๐ด) |
13 | 11, 2, 3, 12 | matvscl 21932 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ต)) โ (๐ถ โ ๐) โ ๐ต) |
14 | 10, 13 | syldan 591 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ท)) โ (๐ถ โ ๐) โ ๐ต) |
15 | 2, 3, 4, 5 | dmatel 21994 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐ โ ๐ท โ (๐ โ ๐ต โง โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐๐๐) = (0gโ๐
))))) |
16 | 15 | adantr 481 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐พ) โ (๐ โ ๐ท โ (๐ โ ๐ต โง โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐๐๐) = (0gโ๐
))))) |
17 | | simp-4r 782 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐
โ Ring) |
18 | | simpr 485 |
. . . . . . . . . . . . . 14
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐พ) โ ๐ถ โ ๐พ) |
19 | 18 | anim1i 615 |
. . . . . . . . . . . . 13
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐พ) โง ๐ โ ๐ต) โ (๐ถ โ ๐พ โง ๐ โ ๐ต)) |
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ถ โ ๐พ โง ๐ โ ๐ต)) |
21 | | simpr 485 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ โ ๐ โง ๐ โ ๐)) |
22 | 17, 20, 21 | 3jca 1128 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐
โ Ring โง (๐ถ โ ๐พ โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐))) |
23 | 22 | adantr 481 |
. . . . . . . . . 10
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง (๐๐๐) = (0gโ๐
)) โ (๐
โ Ring โง (๐ถ โ ๐พ โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐))) |
24 | | eqid 2732 |
. . . . . . . . . . 11
โข
(.rโ๐
) = (.rโ๐
) |
25 | 2, 3, 11, 12, 24 | matvscacell 21937 |
. . . . . . . . . 10
โข ((๐
โ Ring โง (๐ถ โ ๐พ โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ถ โ ๐)๐) = (๐ถ(.rโ๐
)(๐๐๐))) |
26 | 23, 25 | syl 17 |
. . . . . . . . 9
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง (๐๐๐) = (0gโ๐
)) โ (๐(๐ถ โ ๐)๐) = (๐ถ(.rโ๐
)(๐๐๐))) |
27 | | oveq2 7416 |
. . . . . . . . . 10
โข ((๐๐๐) = (0gโ๐
) โ (๐ถ(.rโ๐
)(๐๐๐)) = (๐ถ(.rโ๐
)(0gโ๐
))) |
28 | 27 | adantl 482 |
. . . . . . . . 9
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง (๐๐๐) = (0gโ๐
)) โ (๐ถ(.rโ๐
)(๐๐๐)) = (๐ถ(.rโ๐
)(0gโ๐
))) |
29 | 11, 24, 4 | ringrz 20107 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ๐ถ โ ๐พ) โ (๐ถ(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
30 | 29 | ad5ant23 758 |
. . . . . . . . . 10
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ถ(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
31 | 30 | adantr 481 |
. . . . . . . . 9
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง (๐๐๐) = (0gโ๐
)) โ (๐ถ(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
32 | 26, 28, 31 | 3eqtrd 2776 |
. . . . . . . 8
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง (๐๐๐) = (0gโ๐
)) โ (๐(๐ถ โ ๐)๐) = (0gโ๐
)) |
33 | 32 | ex 413 |
. . . . . . 7
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐๐๐) = (0gโ๐
) โ (๐(๐ถ โ ๐)๐) = (0gโ๐
))) |
34 | 33 | imim2d 57 |
. . . . . 6
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐ โ ๐ โ (๐๐๐) = (0gโ๐
)) โ (๐ โ ๐ โ (๐(๐ถ โ ๐)๐) = (0gโ๐
)))) |
35 | 34 | ralimdvva 3204 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐พ) โง ๐ โ ๐ต) โ (โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐๐๐) = (0gโ๐
)) โ โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐(๐ถ โ ๐)๐) = (0gโ๐
)))) |
36 | 35 | expimpd 454 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐พ) โ ((๐ โ ๐ต โง โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐๐๐) = (0gโ๐
))) โ โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐(๐ถ โ ๐)๐) = (0gโ๐
)))) |
37 | 16, 36 | sylbid 239 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐พ) โ (๐ โ ๐ท โ โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐(๐ถ โ ๐)๐) = (0gโ๐
)))) |
38 | 37 | impr 455 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ท)) โ โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐(๐ถ โ ๐)๐) = (0gโ๐
))) |
39 | 2, 3, 4, 5 | dmatel 21994 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring) โ ((๐ถ โ ๐) โ ๐ท โ ((๐ถ โ ๐) โ ๐ต โง โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐(๐ถ โ ๐)๐) = (0gโ๐
))))) |
40 | 39 | adantr 481 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ท)) โ ((๐ถ โ ๐) โ ๐ท โ ((๐ถ โ ๐) โ ๐ต โง โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐(๐ถ โ ๐)๐) = (0gโ๐
))))) |
41 | 14, 38, 40 | mpbir2and 711 |
1
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ถ โ ๐พ โง ๐ โ ๐ท)) โ (๐ถ โ ๐) โ ๐ท) |