Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
โข ((๐ โ ๐ต โง ๐
โ CRing) โ ๐
โ CRing) |
2 | | madurid.a |
. . . . . . . 8
โข ๐ด = (๐ Mat ๐
) |
3 | | madurid.j |
. . . . . . . 8
โข ๐ฝ = (๐ maAdju ๐
) |
4 | | madurid.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐ด) |
5 | 2, 3, 4 | maduf 22013 |
. . . . . . 7
โข (๐
โ CRing โ ๐ฝ:๐ตโถ๐ต) |
6 | 5 | ffvelcdmda 7039 |
. . . . . 6
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ฝโ๐) โ ๐ต) |
7 | 6 | ancoms 460 |
. . . . 5
โข ((๐ โ ๐ต โง ๐
โ CRing) โ (๐ฝโ๐) โ ๐ต) |
8 | | simpl 484 |
. . . . 5
โข ((๐ โ ๐ต โง ๐
โ CRing) โ ๐ โ ๐ต) |
9 | | madurid.t |
. . . . . 6
โข ยท =
(.rโ๐ด) |
10 | 2, 4, 9 | mattposm 21831 |
. . . . 5
โข ((๐
โ CRing โง (๐ฝโ๐) โ ๐ต โง ๐ โ ๐ต) โ tpos ((๐ฝโ๐) ยท ๐) = (tpos ๐ ยท tpos (๐ฝโ๐))) |
11 | 1, 7, 8, 10 | syl3anc 1372 |
. . . 4
โข ((๐ โ ๐ต โง ๐
โ CRing) โ tpos ((๐ฝโ๐) ยท ๐) = (tpos ๐ ยท tpos (๐ฝโ๐))) |
12 | 2, 3, 4 | madutpos 22014 |
. . . . . 6
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ฝโtpos ๐) = tpos (๐ฝโ๐)) |
13 | 12 | ancoms 460 |
. . . . 5
โข ((๐ โ ๐ต โง ๐
โ CRing) โ (๐ฝโtpos ๐) = tpos (๐ฝโ๐)) |
14 | 13 | oveq2d 7377 |
. . . 4
โข ((๐ โ ๐ต โง ๐
โ CRing) โ (tpos ๐ ยท (๐ฝโtpos ๐)) = (tpos ๐ ยท tpos (๐ฝโ๐))) |
15 | 2, 4 | mattposcl 21825 |
. . . . 5
โข (๐ โ ๐ต โ tpos ๐ โ ๐ต) |
16 | | madurid.d |
. . . . . 6
โข ๐ท = (๐ maDet ๐
) |
17 | | madurid.i |
. . . . . 6
โข 1 =
(1rโ๐ด) |
18 | | madurid.s |
. . . . . 6
โข โ = (
ยท๐ โ๐ด) |
19 | 2, 4, 3, 16, 17, 9, 18 | madurid 22016 |
. . . . 5
โข ((tpos
๐ โ ๐ต โง ๐
โ CRing) โ (tpos ๐ ยท (๐ฝโtpos ๐)) = ((๐ทโtpos ๐) โ 1 )) |
20 | 15, 19 | sylan 581 |
. . . 4
โข ((๐ โ ๐ต โง ๐
โ CRing) โ (tpos ๐ ยท (๐ฝโtpos ๐)) = ((๐ทโtpos ๐) โ 1 )) |
21 | 11, 14, 20 | 3eqtr2d 2779 |
. . 3
โข ((๐ โ ๐ต โง ๐
โ CRing) โ tpos ((๐ฝโ๐) ยท ๐) = ((๐ทโtpos ๐) โ 1 )) |
22 | 21 | tposeqd 8164 |
. 2
โข ((๐ โ ๐ต โง ๐
โ CRing) โ tpos tpos ((๐ฝโ๐) ยท ๐) = tpos ((๐ทโtpos ๐) โ 1 )) |
23 | 2, 4 | matrcl 21782 |
. . . . . 6
โข (๐ โ ๐ต โ (๐ โ Fin โง ๐
โ V)) |
24 | 23 | simpld 496 |
. . . . 5
โข (๐ โ ๐ต โ ๐ โ Fin) |
25 | | crngring 19984 |
. . . . 5
โข (๐
โ CRing โ ๐
โ Ring) |
26 | 2 | matring 21815 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
27 | 24, 25, 26 | syl2an 597 |
. . . 4
โข ((๐ โ ๐ต โง ๐
โ CRing) โ ๐ด โ Ring) |
28 | 4, 9 | ringcl 19989 |
. . . 4
โข ((๐ด โ Ring โง (๐ฝโ๐) โ ๐ต โง ๐ โ ๐ต) โ ((๐ฝโ๐) ยท ๐) โ ๐ต) |
29 | 27, 7, 8, 28 | syl3anc 1372 |
. . 3
โข ((๐ โ ๐ต โง ๐
โ CRing) โ ((๐ฝโ๐) ยท ๐) โ ๐ต) |
30 | 2, 4 | mattpostpos 21826 |
. . 3
โข (((๐ฝโ๐) ยท ๐) โ ๐ต โ tpos tpos ((๐ฝโ๐) ยท ๐) = ((๐ฝโ๐) ยท ๐)) |
31 | 29, 30 | syl 17 |
. 2
โข ((๐ โ ๐ต โง ๐
โ CRing) โ tpos tpos ((๐ฝโ๐) ยท ๐) = ((๐ฝโ๐) ยท ๐)) |
32 | | eqid 2733 |
. . . . . . 7
โข
(Baseโ๐
) =
(Baseโ๐
) |
33 | 16, 2, 4, 32 | mdetf 21967 |
. . . . . 6
โข (๐
โ CRing โ ๐ท:๐ตโถ(Baseโ๐
)) |
34 | 33 | adantl 483 |
. . . . 5
โข ((๐ โ ๐ต โง ๐
โ CRing) โ ๐ท:๐ตโถ(Baseโ๐
)) |
35 | 15 | adantr 482 |
. . . . 5
โข ((๐ โ ๐ต โง ๐
โ CRing) โ tpos ๐ โ ๐ต) |
36 | 34, 35 | ffvelcdmd 7040 |
. . . 4
โข ((๐ โ ๐ต โง ๐
โ CRing) โ (๐ทโtpos ๐) โ (Baseโ๐
)) |
37 | 4, 17 | ringidcl 19997 |
. . . . 5
โข (๐ด โ Ring โ 1 โ ๐ต) |
38 | 27, 37 | syl 17 |
. . . 4
โข ((๐ โ ๐ต โง ๐
โ CRing) โ 1 โ ๐ต) |
39 | 2, 4, 32, 18 | mattposvs 21827 |
. . . 4
โข (((๐ทโtpos ๐) โ (Baseโ๐
) โง 1 โ ๐ต) โ tpos ((๐ทโtpos ๐) โ 1 ) = ((๐ทโtpos ๐) โ tpos 1
)) |
40 | 36, 38, 39 | syl2anc 585 |
. . 3
โข ((๐ โ ๐ต โง ๐
โ CRing) โ tpos ((๐ทโtpos ๐) โ 1 ) = ((๐ทโtpos ๐) โ tpos 1
)) |
41 | 16, 2, 4 | mdettpos 21983 |
. . . . 5
โข ((๐
โ CRing โง ๐ โ ๐ต) โ (๐ทโtpos ๐) = (๐ทโ๐)) |
42 | 41 | ancoms 460 |
. . . 4
โข ((๐ โ ๐ต โง ๐
โ CRing) โ (๐ทโtpos ๐) = (๐ทโ๐)) |
43 | 2, 17 | mattpos1 21828 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring) โ tpos 1 = 1
) |
44 | 24, 25, 43 | syl2an 597 |
. . . 4
โข ((๐ โ ๐ต โง ๐
โ CRing) โ tpos 1 = 1
) |
45 | 42, 44 | oveq12d 7379 |
. . 3
โข ((๐ โ ๐ต โง ๐
โ CRing) โ ((๐ทโtpos ๐) โ tpos 1 ) = ((๐ทโ๐) โ 1 )) |
46 | 40, 45 | eqtrd 2773 |
. 2
โข ((๐ โ ๐ต โง ๐
โ CRing) โ tpos ((๐ทโtpos ๐) โ 1 ) = ((๐ทโ๐) โ 1 )) |
47 | 22, 31, 46 | 3eqtr3d 2781 |
1
โข ((๐ โ ๐ต โง ๐
โ CRing) โ ((๐ฝโ๐) ยท ๐) = ((๐ทโ๐) โ 1 )) |