Step | Hyp | Ref
| Expression |
1 | | mdetunilem2.ph |
. 2
โข (๐ โ ๐) |
2 | | mdetuni.a |
. . 3
โข ๐ด = (๐ Mat ๐
) |
3 | | mdetuni.k |
. . 3
โข ๐พ = (Baseโ๐
) |
4 | | mdetuni.b |
. . 3
โข ๐ต = (Baseโ๐ด) |
5 | | mdetuni.n |
. . . 4
โข (๐ โ ๐ โ Fin) |
6 | 1, 5 | syl 17 |
. . 3
โข (๐ โ ๐ โ Fin) |
7 | | mdetuni.r |
. . . 4
โข (๐ โ ๐
โ Ring) |
8 | 1, 7 | syl 17 |
. . 3
โข (๐ โ ๐
โ Ring) |
9 | | mdetunilem2.f |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ๐น โ ๐พ) |
10 | 9 | 3adant2 1132 |
. . . 4
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐น โ ๐พ) |
11 | | mdetunilem2.h |
. . . . 5
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ป โ ๐พ) |
12 | 10, 11 | ifcld 4536 |
. . . 4
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐บ, ๐น, ๐ป) โ ๐พ) |
13 | 10, 12 | ifcld 4536 |
. . 3
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)) โ ๐พ) |
14 | 2, 3, 4, 6, 8, 13 | matbas2d 21795 |
. 2
โข (๐ โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป))) โ ๐ต) |
15 | | eqidd 2734 |
. . . . 5
โข ((๐ โง ๐ค โ ๐) โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป))) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))) |
16 | | iftrue 4496 |
. . . . . . 7
โข (๐ = ๐ธ โ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)) = ๐น) |
17 | | csbeq1a 3873 |
. . . . . . 7
โข (๐ = ๐ค โ ๐น = โฆ๐ค / ๐โฆ๐น) |
18 | 16, 17 | sylan9eq 2793 |
. . . . . 6
โข ((๐ = ๐ธ โง ๐ = ๐ค) โ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)) = โฆ๐ค / ๐โฆ๐น) |
19 | 18 | adantl 483 |
. . . . 5
โข (((๐ โง ๐ค โ ๐) โง (๐ = ๐ธ โง ๐ = ๐ค)) โ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)) = โฆ๐ค / ๐โฆ๐น) |
20 | | eqidd 2734 |
. . . . 5
โข (((๐ โง ๐ค โ ๐) โง ๐ = ๐ธ) โ ๐ = ๐) |
21 | | mdetunilem2.eg |
. . . . . . 7
โข (๐ โ (๐ธ โ ๐ โง ๐บ โ ๐ โง ๐ธ โ ๐บ)) |
22 | 21 | simp1d 1143 |
. . . . . 6
โข (๐ โ ๐ธ โ ๐) |
23 | 22 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ค โ ๐) โ ๐ธ โ ๐) |
24 | | simpr 486 |
. . . . 5
โข ((๐ โง ๐ค โ ๐) โ ๐ค โ ๐) |
25 | | nfv 1918 |
. . . . . . 7
โข
โฒ๐(๐ โง ๐ค โ ๐) |
26 | | nfcsb1v 3884 |
. . . . . . . 8
โข
โฒ๐โฆ๐ค / ๐โฆ๐น |
27 | 26 | nfel1 2920 |
. . . . . . 7
โข
โฒ๐โฆ๐ค / ๐โฆ๐น โ ๐พ |
28 | 25, 27 | nfim 1900 |
. . . . . 6
โข
โฒ๐((๐ โง ๐ค โ ๐) โ โฆ๐ค / ๐โฆ๐น โ ๐พ) |
29 | | eleq1w 2817 |
. . . . . . . 8
โข (๐ = ๐ค โ (๐ โ ๐ โ ๐ค โ ๐)) |
30 | 29 | anbi2d 630 |
. . . . . . 7
โข (๐ = ๐ค โ ((๐ โง ๐ โ ๐) โ (๐ โง ๐ค โ ๐))) |
31 | 17 | eleq1d 2819 |
. . . . . . 7
โข (๐ = ๐ค โ (๐น โ ๐พ โ โฆ๐ค / ๐โฆ๐น โ ๐พ)) |
32 | 30, 31 | imbi12d 345 |
. . . . . 6
โข (๐ = ๐ค โ (((๐ โง ๐ โ ๐) โ ๐น โ ๐พ) โ ((๐ โง ๐ค โ ๐) โ โฆ๐ค / ๐โฆ๐น โ ๐พ))) |
33 | 28, 32, 9 | chvarfv 2234 |
. . . . 5
โข ((๐ โง ๐ค โ ๐) โ โฆ๐ค / ๐โฆ๐น โ ๐พ) |
34 | | nfv 1918 |
. . . . 5
โข
โฒ๐(๐ โง ๐ค โ ๐) |
35 | | nfcv 2904 |
. . . . 5
โข
โฒ๐๐ธ |
36 | | nfcv 2904 |
. . . . 5
โข
โฒ๐๐ค |
37 | | nfcv 2904 |
. . . . 5
โข
โฒ๐โฆ๐ค / ๐โฆ๐น |
38 | 15, 19, 20, 23, 24, 33, 34, 25, 35, 36, 37, 26 | ovmpodxf 7509 |
. . . 4
โข ((๐ โง ๐ค โ ๐) โ (๐ธ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))๐ค) = โฆ๐ค / ๐โฆ๐น) |
39 | 21 | simp3d 1145 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ธ โ ๐บ) |
40 | 39 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ ๐ธ โ ๐บ) |
41 | | neeq2 3004 |
. . . . . . . . . . . 12
โข (๐ = ๐บ โ (๐ธ โ ๐ โ ๐ธ โ ๐บ)) |
42 | 40, 41 | syl5ibrcom 247 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ (๐ = ๐บ โ ๐ธ โ ๐)) |
43 | 42 | imp 408 |
. . . . . . . . . 10
โข (((๐ โง ๐ค โ ๐) โง ๐ = ๐บ) โ ๐ธ โ ๐) |
44 | 43 | necomd 2996 |
. . . . . . . . 9
โข (((๐ โง ๐ค โ ๐) โง ๐ = ๐บ) โ ๐ โ ๐ธ) |
45 | 44 | neneqd 2945 |
. . . . . . . 8
โข (((๐ โง ๐ค โ ๐) โง ๐ = ๐บ) โ ยฌ ๐ = ๐ธ) |
46 | 45 | adantrr 716 |
. . . . . . 7
โข (((๐ โง ๐ค โ ๐) โง (๐ = ๐บ โง ๐ = ๐ค)) โ ยฌ ๐ = ๐ธ) |
47 | 46 | iffalsed 4501 |
. . . . . 6
โข (((๐ โง ๐ค โ ๐) โง (๐ = ๐บ โง ๐ = ๐ค)) โ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)) = if(๐ = ๐บ, ๐น, ๐ป)) |
48 | | iftrue 4496 |
. . . . . . . 8
โข (๐ = ๐บ โ if(๐ = ๐บ, ๐น, ๐ป) = ๐น) |
49 | 48, 17 | sylan9eq 2793 |
. . . . . . 7
โข ((๐ = ๐บ โง ๐ = ๐ค) โ if(๐ = ๐บ, ๐น, ๐ป) = โฆ๐ค / ๐โฆ๐น) |
50 | 49 | adantl 483 |
. . . . . 6
โข (((๐ โง ๐ค โ ๐) โง (๐ = ๐บ โง ๐ = ๐ค)) โ if(๐ = ๐บ, ๐น, ๐ป) = โฆ๐ค / ๐โฆ๐น) |
51 | 47, 50 | eqtrd 2773 |
. . . . 5
โข (((๐ โง ๐ค โ ๐) โง (๐ = ๐บ โง ๐ = ๐ค)) โ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)) = โฆ๐ค / ๐โฆ๐น) |
52 | | eqidd 2734 |
. . . . 5
โข (((๐ โง ๐ค โ ๐) โง ๐ = ๐บ) โ ๐ = ๐) |
53 | 21 | simp2d 1144 |
. . . . . 6
โข (๐ โ ๐บ โ ๐) |
54 | 53 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ค โ ๐) โ ๐บ โ ๐) |
55 | | nfcv 2904 |
. . . . 5
โข
โฒ๐๐บ |
56 | 15, 51, 52, 54, 24, 33, 34, 25, 55, 36, 37, 26 | ovmpodxf 7509 |
. . . 4
โข ((๐ โง ๐ค โ ๐) โ (๐บ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))๐ค) = โฆ๐ค / ๐โฆ๐น) |
57 | 38, 56 | eqtr4d 2776 |
. . 3
โข ((๐ โง ๐ค โ ๐) โ (๐ธ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))๐ค) = (๐บ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))๐ค)) |
58 | 57 | ralrimiva 3140 |
. 2
โข (๐ โ โ๐ค โ ๐ (๐ธ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))๐ค) = (๐บ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))๐ค)) |
59 | | mdetuni.0g |
. . 3
โข 0 =
(0gโ๐
) |
60 | | mdetuni.1r |
. . 3
โข 1 =
(1rโ๐
) |
61 | | mdetuni.pg |
. . 3
โข + =
(+gโ๐
) |
62 | | mdetuni.tg |
. . 3
โข ยท =
(.rโ๐
) |
63 | | mdetuni.ff |
. . 3
โข (๐ โ ๐ท:๐ตโถ๐พ) |
64 | | mdetuni.al |
. . 3
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) |
65 | | mdetuni.li |
. . 3
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) |
66 | | mdetuni.sc |
. . 3
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) |
67 | 2, 4, 3, 59, 60, 61, 62, 5, 7, 63, 64, 65, 66 | mdetunilem1 21984 |
. 2
โข (((๐ โง (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป))) โ ๐ต โง โ๐ค โ ๐ (๐ธ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))๐ค) = (๐บ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))๐ค)) โง (๐ธ โ ๐ โง ๐บ โ ๐ โง ๐ธ โ ๐บ)) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))) = 0 ) |
68 | 1, 14, 58, 21, 67 | syl31anc 1374 |
1
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐น, if(๐ = ๐บ, ๐น, ๐ป)))) = 0 ) |