Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . 7
โข ((๐
โ CRing โง ๐ โ Fin) โ ๐
โ CRing) |
2 | 1 | adantr 482 |
. . . . . 6
โข (((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โ ๐
โ CRing) |
3 | | simpr 486 |
. . . . . . 7
โข ((๐
โ CRing โง ๐ โ Fin) โ ๐ โ Fin) |
4 | 3 | adantr 482 |
. . . . . 6
โข (((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โ ๐ โ Fin) |
5 | | simpl 484 |
. . . . . . 7
โข ((๐ โ ๐ต โง ๐ โ ๐ถ) โ ๐ โ ๐ต) |
6 | 5 | adantl 483 |
. . . . . 6
โข (((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โ ๐ โ ๐ต) |
7 | 2, 4, 6 | 3jca 1129 |
. . . . 5
โข (((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โ (๐
โ CRing โง ๐ โ Fin โง ๐ โ ๐ต)) |
8 | 7 | adantr 482 |
. . . 4
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐
โ CRing โง ๐ โ Fin โง ๐ โ ๐ต)) |
9 | | id 22 |
. . . . . . . . . 10
โข ((๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐๐๐) = if(๐ = ๐, ๐, 0 )) |
10 | | ifnefalse 4502 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ if(๐ = ๐, ๐, 0 ) = 0 ) |
11 | 10 | adantl 483 |
. . . . . . . . . 10
โข
((((((๐
โ CRing
โง ๐ โ Fin) โง
(๐ โ ๐ต โง ๐ โ ๐ถ)) โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ if(๐ = ๐, ๐, 0 ) = 0 ) |
12 | 9, 11 | sylan9eqr 2795 |
. . . . . . . . 9
โข
(((((((๐
โ
CRing โง ๐ โ Fin)
โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โง (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐๐๐) = 0 ) |
13 | 12 | exp31 421 |
. . . . . . . 8
โข
(((((๐
โ CRing
โง ๐ โ Fin) โง
(๐ โ ๐ต โง ๐ โ ๐ถ)) โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ โ ๐ โ ((๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐๐๐) = 0 ))) |
14 | 13 | com23 86 |
. . . . . . 7
โข
(((((๐
โ CRing
โง ๐ โ Fin) โง
(๐ โ ๐ต โง ๐ โ ๐ถ)) โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐ โ ๐ โ (๐๐๐) = 0 ))) |
15 | 14 | ralimdva 3161 |
. . . . . 6
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง ๐ โ ๐) โ (โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ) โ โ๐ โ ๐ (๐ โ ๐ โ (๐๐๐) = 0 ))) |
16 | 15 | ralimdva 3161 |
. . . . 5
โข (((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โ (โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ) โ โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐๐๐) = 0 ))) |
17 | 16 | imp 408 |
. . . 4
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐๐๐) = 0 )) |
18 | | mdetdiag.d |
. . . . 5
โข ๐ท = (๐ maDet ๐
) |
19 | | mdetdiag.a |
. . . . 5
โข ๐ด = (๐ Mat ๐
) |
20 | | mdetdiag.b |
. . . . 5
โข ๐ต = (Baseโ๐ด) |
21 | | mdetdiag.g |
. . . . 5
โข ๐บ = (mulGrpโ๐
) |
22 | | mdetdiag.0 |
. . . . 5
โข 0 =
(0gโ๐
) |
23 | 18, 19, 20, 21, 22 | mdetdiag 21971 |
. . . 4
โข ((๐
โ CRing โง ๐ โ Fin โง ๐ โ ๐ต) โ (โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โ (๐๐๐) = 0 ) โ (๐ทโ๐) = (๐บ ฮฃg (๐ โ ๐ โฆ (๐๐๐))))) |
24 | 8, 17, 23 | sylc 65 |
. . 3
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐ทโ๐) = (๐บ ฮฃg (๐ โ ๐ โฆ (๐๐๐)))) |
25 | | oveq1 7368 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐๐๐) = (๐๐๐)) |
26 | | equequ1 2029 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ = ๐ โ ๐ = ๐)) |
27 | 26 | ifbid 4513 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ if(๐ = ๐, ๐, 0 ) = if(๐ = ๐, ๐, 0 )) |
28 | 25, 27 | eqeq12d 2749 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
29 | | oveq2 7369 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐๐๐) = (๐๐๐)) |
30 | | equequ2 2030 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ = ๐ โ ๐ = ๐)) |
31 | 30 | ifbid 4513 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ if(๐ = ๐, ๐, 0 ) = if(๐ = ๐, ๐, 0 )) |
32 | 29, 31 | eqeq12d 2749 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
33 | 28, 32 | rspc2v 3592 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐) โ (โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
34 | 33 | anidms 568 |
. . . . . . . . 9
โข (๐ โ ๐ โ (โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
35 | 34 | adantl 483 |
. . . . . . . 8
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง ๐ โ ๐) โ (โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐๐๐) = if(๐ = ๐, ๐, 0 ))) |
36 | 35 | imp 408 |
. . . . . . 7
โข
(((((๐
โ CRing
โง ๐ โ Fin) โง
(๐ โ ๐ต โง ๐ โ ๐ถ)) โง ๐ โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐๐๐) = if(๐ = ๐, ๐, 0 )) |
37 | | equid 2016 |
. . . . . . . 8
โข ๐ = ๐ |
38 | 37 | iftruei 4497 |
. . . . . . 7
โข if(๐ = ๐, ๐, 0 ) = ๐ |
39 | 36, 38 | eqtrdi 2789 |
. . . . . 6
โข
(((((๐
โ CRing
โง ๐ โ Fin) โง
(๐ โ ๐ต โง ๐ โ ๐ถ)) โง ๐ โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐๐๐) = ๐) |
40 | 39 | an32s 651 |
. . . . 5
โข
(((((๐
โ CRing
โง ๐ โ Fin) โง
(๐ โ ๐ต โง ๐ โ ๐ถ)) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โง ๐ โ ๐) โ (๐๐๐) = ๐) |
41 | 40 | mpteq2dva 5209 |
. . . 4
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐ โ ๐ โฆ (๐๐๐)) = (๐ โ ๐ โฆ ๐)) |
42 | 41 | oveq2d 7377 |
. . 3
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐บ ฮฃg
(๐ โ ๐ โฆ (๐๐๐))) = (๐บ ฮฃg (๐ โ ๐ โฆ ๐))) |
43 | 21 | crngmgp 19980 |
. . . . . . 7
โข (๐
โ CRing โ ๐บ โ CMnd) |
44 | | cmnmnd 19587 |
. . . . . . 7
โข (๐บ โ CMnd โ ๐บ โ Mnd) |
45 | 43, 44 | syl 17 |
. . . . . 6
โข (๐
โ CRing โ ๐บ โ Mnd) |
46 | 45 | adantr 482 |
. . . . 5
โข ((๐
โ CRing โง ๐ โ Fin) โ ๐บ โ Mnd) |
47 | | simpr 486 |
. . . . 5
โข ((๐ โ ๐ต โง ๐ โ ๐ถ) โ ๐ โ ๐ถ) |
48 | | mdetdiagid.c |
. . . . . . 7
โข ๐ถ = (Baseโ๐
) |
49 | 21, 48 | mgpbas 19910 |
. . . . . 6
โข ๐ถ = (Baseโ๐บ) |
50 | | mdetdiagid.t |
. . . . . 6
โข ยท =
(.gโ๐บ) |
51 | 49, 50 | gsumconst 19719 |
. . . . 5
โข ((๐บ โ Mnd โง ๐ โ Fin โง ๐ โ ๐ถ) โ (๐บ ฮฃg (๐ โ ๐ โฆ ๐)) = ((โฏโ๐) ยท ๐)) |
52 | 46, 3, 47, 51 | syl2an3an 1423 |
. . . 4
โข (((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โ (๐บ ฮฃg (๐ โ ๐ โฆ ๐)) = ((โฏโ๐) ยท ๐)) |
53 | 52 | adantr 482 |
. . 3
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐บ ฮฃg
(๐ โ ๐ โฆ ๐)) = ((โฏโ๐) ยท ๐)) |
54 | 24, 42, 53 | 3eqtrd 2777 |
. 2
โข ((((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โง โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 )) โ (๐ทโ๐) = ((โฏโ๐) ยท ๐)) |
55 | 54 | ex 414 |
1
โข (((๐
โ CRing โง ๐ โ Fin) โง (๐ โ ๐ต โง ๐ โ ๐ถ)) โ (โ๐ โ ๐ โ๐ โ ๐ (๐๐๐) = if(๐ = ๐, ๐, 0 ) โ (๐ทโ๐) = ((โฏโ๐) ยท ๐))) |