Step | Hyp | Ref
| Expression |
1 | | mdetuni.a |
. . . . 5
โข ๐ด = (๐ Mat ๐
) |
2 | | mdetuni.b |
. . . . 5
โข ๐ต = (Baseโ๐ด) |
3 | | mdetuni.k |
. . . . 5
โข ๐พ = (Baseโ๐
) |
4 | | mdetuni.0g |
. . . . 5
โข 0 =
(0gโ๐
) |
5 | | mdetuni.1r |
. . . . 5
โข 1 =
(1rโ๐
) |
6 | | mdetuni.pg |
. . . . 5
โข + =
(+gโ๐
) |
7 | | mdetuni.tg |
. . . . 5
โข ยท =
(.rโ๐
) |
8 | | mdetuni.n |
. . . . 5
โข (๐ โ ๐ โ Fin) |
9 | | mdetuni.r |
. . . . 5
โข (๐ โ ๐
โ Ring) |
10 | | ringgrp 19977 |
. . . . . . . . 9
โข (๐
โ Ring โ ๐
โ Grp) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐
โ Grp) |
12 | 11 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ ๐
โ Grp) |
13 | | mdetuni.ff |
. . . . . . . 8
โข (๐ โ ๐ท:๐ตโถ๐พ) |
14 | 13 | ffvelcdmda 7039 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ (๐ทโ๐) โ ๐พ) |
15 | 9 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ ๐
โ Ring) |
16 | 8, 9 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ Fin โง ๐
โ Ring)) |
17 | 1 | matring 21815 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
18 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(1rโ๐ด) = (1rโ๐ด) |
19 | 2, 18 | ringidcl 19997 |
. . . . . . . . . . 11
โข (๐ด โ Ring โ
(1rโ๐ด)
โ ๐ต) |
20 | 16, 17, 19 | 3syl 18 |
. . . . . . . . . 10
โข (๐ โ (1rโ๐ด) โ ๐ต) |
21 | 13, 20 | ffvelcdmd 7040 |
. . . . . . . . 9
โข (๐ โ (๐ทโ(1rโ๐ด)) โ ๐พ) |
22 | 21 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ (๐ทโ(1rโ๐ด)) โ ๐พ) |
23 | | mdetuni.cr |
. . . . . . . . . 10
โข (๐ โ ๐
โ CRing) |
24 | | mdetuni.e |
. . . . . . . . . . 11
โข ๐ธ = (๐ maDet ๐
) |
25 | 24, 1, 2, 3 | mdetf 21967 |
. . . . . . . . . 10
โข (๐
โ CRing โ ๐ธ:๐ตโถ๐พ) |
26 | 23, 25 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ธ:๐ตโถ๐พ) |
27 | 26 | ffvelcdmda 7039 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ (๐ธโ๐) โ ๐พ) |
28 | 3, 7 | ringcl 19989 |
. . . . . . . 8
โข ((๐
โ Ring โง (๐ทโ(1rโ๐ด)) โ ๐พ โง (๐ธโ๐) โ ๐พ) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ) |
29 | 15, 22, 27, 28 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ) |
30 | | eqid 2733 |
. . . . . . . 8
โข
(-gโ๐
) = (-gโ๐
) |
31 | 3, 30 | grpsubcl 18835 |
. . . . . . 7
โข ((๐
โ Grp โง (๐ทโ๐) โ ๐พ โง ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ) โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) โ ๐พ) |
32 | 12, 14, 29, 31 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ต) โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) โ ๐พ) |
33 | 32 | fmpttd 7067 |
. . . . 5
โข (๐ โ (๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))):๐ตโถ๐พ) |
34 | | simpr1 1195 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐ต) |
35 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ทโ๐) = (๐ทโ๐)) |
36 | | fveq2 6846 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ธโ๐) = (๐ธโ๐)) |
37 | 36 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) = ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) |
38 | 35, 37 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
39 | | eqid 2733 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) = (๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
40 | | ovex 7394 |
. . . . . . . . . . 11
โข ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) โ V |
41 | 38, 39, 40 | fvmpt 6952 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
42 | 34, 41 | syl 17 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐)) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
43 | 42 | 3adant3 1133 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
44 | | simp1 1137 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ๐) |
45 | | simp21 1207 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ๐ โ ๐ต) |
46 | | simp3r 1203 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ โ๐ โ ๐ (๐๐๐) = (๐๐๐)) |
47 | | oveq2 7369 |
. . . . . . . . . . . . 13
โข (๐ = ๐ค โ (๐๐๐) = (๐๐๐ค)) |
48 | | oveq2 7369 |
. . . . . . . . . . . . 13
โข (๐ = ๐ค โ (๐๐๐) = (๐๐๐ค)) |
49 | 47, 48 | eqeq12d 2749 |
. . . . . . . . . . . 12
โข (๐ = ๐ค โ ((๐๐๐) = (๐๐๐) โ (๐๐๐ค) = (๐๐๐ค))) |
50 | 49 | cbvralvw 3224 |
. . . . . . . . . . 11
โข
(โ๐ โ
๐ (๐๐๐) = (๐๐๐) โ โ๐ค โ ๐ (๐๐๐ค) = (๐๐๐ค)) |
51 | 46, 50 | sylib 217 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ โ๐ค โ ๐ (๐๐๐ค) = (๐๐๐ค)) |
52 | | simp22 1208 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ๐ โ ๐) |
53 | | simp23 1209 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ๐ โ ๐) |
54 | | simp3l 1202 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ๐ โ ๐) |
55 | | mdetuni.al |
. . . . . . . . . . 11
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) |
56 | | mdetuni.li |
. . . . . . . . . . 11
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) |
57 | | mdetuni.sc |
. . . . . . . . . . 11
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) |
58 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 13,
55, 56, 57 | mdetunilem1 21984 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต โง โ๐ค โ ๐ (๐๐๐ค) = (๐๐๐ค)) โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ (๐ทโ๐) = 0 ) |
59 | 44, 45, 51, 52, 53, 54, 58 | syl33anc 1386 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ (๐ทโ๐) = 0 ) |
60 | 23 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ๐
โ CRing) |
61 | 24, 1, 2, 4, 60, 45, 52, 53, 54, 46 | mdetralt 21980 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ (๐ธโ๐) = 0 ) |
62 | 61 | oveq2d 7377 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) = ((๐ทโ(1rโ๐ด)) ยท 0 )) |
63 | 59, 62 | oveq12d 7379 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ( 0 (-gโ๐
)((๐ทโ(1rโ๐ด)) ยท 0 ))) |
64 | 3, 7, 4 | ringrz 20020 |
. . . . . . . . . . . 12
โข ((๐
โ Ring โง (๐ทโ(1rโ๐ด)) โ ๐พ) โ ((๐ทโ(1rโ๐ด)) ยท 0 ) = 0 ) |
65 | 9, 21, 64 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ ((๐ทโ(1rโ๐ด)) ยท 0 ) = 0 ) |
66 | 65 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ โ ( 0 (-gโ๐
)((๐ทโ(1rโ๐ด)) ยท 0 )) = ( 0 (-gโ๐
) 0 )) |
67 | 3, 4 | grpidcl 18786 |
. . . . . . . . . . 11
โข (๐
โ Grp โ 0 โ ๐พ) |
68 | 3, 4, 30 | grpsubid 18839 |
. . . . . . . . . . 11
โข ((๐
โ Grp โง 0 โ ๐พ) โ ( 0 (-gโ๐
) 0 ) = 0 ) |
69 | 11, 67, 68 | syl2anc2 586 |
. . . . . . . . . 10
โข (๐ โ ( 0 (-gโ๐
) 0 ) = 0 ) |
70 | 66, 69 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ ( 0 (-gโ๐
)((๐ทโ(1rโ๐ด)) ยท 0 )) = 0 ) |
71 | 70 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ( 0 (-gโ๐
)((๐ทโ(1rโ๐ด)) ยท 0 )) = 0 ) |
72 | 43, 63, 71 | 3eqtrd 2777 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = 0 ) |
73 | 72 | 3expia 1122 |
. . . . . 6
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ โง ๐ โ ๐)) โ ((๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐)) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = 0 )) |
74 | 73 | ralrimivvva 3197 |
. . . . 5
โข (๐ โ โ๐ โ ๐ต โ๐ โ ๐ โ๐ โ ๐ ((๐ โ ๐ โง โ๐ โ ๐ (๐๐๐) = (๐๐๐)) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = 0 )) |
75 | | simp1 1137 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐) |
76 | | simp2ll 1241 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐ โ ๐ต) |
77 | | simp2lr 1242 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐ โ ๐ต) |
78 | | simp2rl 1243 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐ โ ๐ต) |
79 | | simp2rr 1244 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐ โ ๐) |
80 | | simp31 1210 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐)))) |
81 | | simp32 1211 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) |
82 | | simp33 1212 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) |
83 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 13,
55, 56, 57 | mdetunilem3 21986 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ โง (๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐)))) โง ((๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ทโ๐) = ((๐ทโ๐) + (๐ทโ๐))) |
84 | 75, 76, 77, 78, 79, 80, 81, 82, 83 | syl332anc 1402 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ทโ๐) = ((๐ทโ๐) + (๐ทโ๐))) |
85 | 23 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐
โ CRing) |
86 | 24, 1, 2, 6, 85, 76, 77, 78, 79, 80, 81, 82 | mdetrlin 21974 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ธโ๐) = ((๐ธโ๐) + (๐ธโ๐))) |
87 | 86 | oveq2d 7377 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) = ((๐ทโ(1rโ๐ด)) ยท ((๐ธโ๐) + (๐ธโ๐)))) |
88 | 84, 87 | oveq12d 7379 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = (((๐ทโ๐) + (๐ทโ๐))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท ((๐ธโ๐) + (๐ธโ๐))))) |
89 | | simprll 778 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ โ ๐ต) |
90 | 89, 41 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
91 | 90 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
92 | | simprlr 779 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ โ ๐ต) |
93 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (๐ทโ๐) = (๐ทโ๐)) |
94 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐ธโ๐) = (๐ธโ๐)) |
95 | 94 | oveq2d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) = ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) |
96 | 93, 95 | oveq12d 7379 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
97 | | ovex 7394 |
. . . . . . . . . . . . . . 15
โข ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) โ V |
98 | 96, 39, 97 | fvmpt 6952 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ต โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
99 | 92, 98 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
100 | | simprrl 780 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ โ ๐ต) |
101 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (๐ทโ๐) = (๐ทโ๐)) |
102 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐ธโ๐) = (๐ธโ๐)) |
103 | 102 | oveq2d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) = ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) |
104 | 101, 103 | oveq12d 7379 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
105 | | ovex 7394 |
. . . . . . . . . . . . . . 15
โข ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) โ V |
106 | 104, 39, 105 | fvmpt 6952 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ต โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
107 | 100, 106 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
108 | 99, 107 | oveq12d 7379 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) + ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)) = (((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) + ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))) |
109 | | ringabl 20010 |
. . . . . . . . . . . . . . 15
โข (๐
โ Ring โ ๐
โ Abel) |
110 | 9, 109 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐
โ Abel) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐
โ Abel) |
112 | 13 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ท:๐ตโถ๐พ) |
113 | 112, 92 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ทโ๐) โ ๐พ) |
114 | 112, 100 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ทโ๐) โ ๐พ) |
115 | 9 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐
โ Ring) |
116 | 21 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ทโ(1rโ๐ด)) โ ๐พ) |
117 | 26 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ธ:๐ตโถ๐พ) |
118 | 117, 92 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ธโ๐) โ ๐พ) |
119 | 3, 7 | ringcl 19989 |
. . . . . . . . . . . . . 14
โข ((๐
โ Ring โง (๐ทโ(1rโ๐ด)) โ ๐พ โง (๐ธโ๐) โ ๐พ) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ) |
120 | 115, 116,
118, 119 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ) |
121 | 117, 100 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ธโ๐) โ ๐พ) |
122 | 3, 7 | ringcl 19989 |
. . . . . . . . . . . . . 14
โข ((๐
โ Ring โง (๐ทโ(1rโ๐ด)) โ ๐พ โง (๐ธโ๐) โ ๐พ) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ) |
123 | 115, 116,
121, 122 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ) |
124 | 3, 6, 30 | ablsub4 19599 |
. . . . . . . . . . . . 13
โข ((๐
โ Abel โง ((๐ทโ๐) โ ๐พ โง (๐ทโ๐) โ ๐พ) โง (((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ โง ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ)) โ (((๐ทโ๐) + (๐ทโ๐))(-gโ๐
)(((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) + ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) = (((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) + ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))) |
125 | 111, 113,
114, 120, 123, 124 | syl122anc 1380 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (((๐ทโ๐) + (๐ทโ๐))(-gโ๐
)(((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) + ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) = (((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) + ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))) |
126 | 3, 6, 7 | ringdi 19995 |
. . . . . . . . . . . . . . 15
โข ((๐
โ Ring โง ((๐ทโ(1rโ๐ด)) โ ๐พ โง (๐ธโ๐) โ ๐พ โง (๐ธโ๐) โ ๐พ)) โ ((๐ทโ(1rโ๐ด)) ยท ((๐ธโ๐) + (๐ธโ๐))) = (((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) + ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
127 | 115, 116,
118, 121, 126 | syl13anc 1373 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ทโ(1rโ๐ด)) ยท ((๐ธโ๐) + (๐ธโ๐))) = (((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) + ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
128 | 127 | eqcomd 2739 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) + ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ(1rโ๐ด)) ยท ((๐ธโ๐) + (๐ธโ๐)))) |
129 | 128 | oveq2d 7377 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (((๐ทโ๐) + (๐ทโ๐))(-gโ๐
)(((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) + ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) = (((๐ทโ๐) + (๐ทโ๐))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท ((๐ธโ๐) + (๐ธโ๐))))) |
130 | 108, 125,
129 | 3eqtr2d 2779 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) + ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)) = (((๐ทโ๐) + (๐ทโ๐))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท ((๐ธโ๐) + (๐ธโ๐))))) |
131 | 130 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) + ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)) = (((๐ทโ๐) + (๐ทโ๐))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท ((๐ธโ๐) + (๐ธโ๐))))) |
132 | 88, 91, 131 | 3eqtr4d 2783 |
. . . . . . . . 9
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) + ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐))) |
133 | 132 | 3expia 1122 |
. . . . . . . 8
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) + ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)))) |
134 | 133 | anassrs 469 |
. . . . . . 7
โข (((๐ โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ โ ๐ต โง ๐ โ ๐)) โ (((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) + ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)))) |
135 | 134 | ralrimivva 3194 |
. . . . . 6
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ โ๐ โ ๐ต โ๐ โ ๐ (((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) + ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)))) |
136 | 135 | ralrimivva 3194 |
. . . . 5
โข (๐ โ โ๐ โ ๐ต โ๐ โ ๐ต โ๐ โ ๐ต โ๐ โ ๐ (((๐ โพ ({๐} ร ๐)) = ((๐ โพ ({๐} ร ๐)) โf + (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) + ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)))) |
137 | | simp1 1137 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐) |
138 | | simp2ll 1241 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐ โ ๐ต) |
139 | | simp2lr 1242 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐ โ ๐พ) |
140 | | simp2rl 1243 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐ โ ๐ต) |
141 | | simp2rr 1244 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐ โ ๐) |
142 | | simp3l 1202 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐)))) |
143 | | simp3r 1203 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) |
144 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 13,
55, 56, 57 | mdetunilem4 21987 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ โ ๐ โง (๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ทโ๐) = (๐ ยท (๐ทโ๐))) |
145 | 137, 138,
139, 140, 141, 142, 143, 144 | syl133anc 1394 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ทโ๐) = (๐ ยท (๐ทโ๐))) |
146 | 23 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ๐
โ CRing) |
147 | 24, 1, 2, 3, 7, 146, 138, 139, 140, 141, 142, 143 | mdetrsca 21975 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ธโ๐) = (๐ ยท (๐ธโ๐))) |
148 | 147 | oveq2d 7377 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) = ((๐ทโ(1rโ๐ด)) ยท (๐ ยท (๐ธโ๐)))) |
149 | 145, 148 | oveq12d 7379 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ ยท (๐ทโ๐))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ ยท (๐ธโ๐))))) |
150 | | simprll 778 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ โ ๐ต) |
151 | 150, 41 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
152 | 151 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
153 | | simprrl 780 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ โ ๐ต) |
154 | 153, 106 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) |
155 | 154 | oveq2d 7377 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ ยท ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)) = (๐ ยท ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))) |
156 | 9 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐
โ Ring) |
157 | | simprlr 779 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ โ ๐พ) |
158 | 13 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ท:๐ตโถ๐พ) |
159 | 158, 153 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ทโ๐) โ ๐พ) |
160 | 21 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ทโ(1rโ๐ด)) โ ๐พ) |
161 | 26 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ๐ธ:๐ตโถ๐พ) |
162 | 161, 153 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ธโ๐) โ ๐พ) |
163 | 156, 160,
162, 122 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) โ ๐พ) |
164 | 3, 7, 30, 156, 157, 159, 163 | ringsubdi 20031 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ ยท ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) = ((๐ ยท (๐ทโ๐))(-gโ๐
)(๐ ยท ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))) |
165 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
166 | 165 | crngmgp 19980 |
. . . . . . . . . . . . . . . 16
โข (๐
โ CRing โ
(mulGrpโ๐
) โ
CMnd) |
167 | 23, 166 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (mulGrpโ๐
) โ CMnd) |
168 | 167 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (mulGrpโ๐
) โ CMnd) |
169 | 165, 3 | mgpbas 19910 |
. . . . . . . . . . . . . . 15
โข ๐พ =
(Baseโ(mulGrpโ๐
)) |
170 | 165, 7 | mgpplusg 19908 |
. . . . . . . . . . . . . . 15
โข ยท =
(+gโ(mulGrpโ๐
)) |
171 | 169, 170 | cmn12 19592 |
. . . . . . . . . . . . . 14
โข
(((mulGrpโ๐
)
โ CMnd โง (๐ โ
๐พ โง (๐ทโ(1rโ๐ด)) โ ๐พ โง (๐ธโ๐) โ ๐พ)) โ (๐ ยท ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ(1rโ๐ด)) ยท (๐ ยท (๐ธโ๐)))) |
172 | 168, 157,
160, 162, 171 | syl13anc 1373 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ ยท ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ(1rโ๐ด)) ยท (๐ ยท (๐ธโ๐)))) |
173 | 172 | oveq2d 7377 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ ((๐ ยท (๐ทโ๐))(-gโ๐
)(๐ ยท ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) = ((๐ ยท (๐ทโ๐))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ ยท (๐ธโ๐))))) |
174 | 155, 164,
173 | 3eqtrd 2777 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (๐ ยท ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)) = ((๐ ยท (๐ทโ๐))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ ยท (๐ธโ๐))))) |
175 | 174 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ (๐ ยท ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)) = ((๐ ยท (๐ทโ๐))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ ยท (๐ธโ๐))))) |
176 | 149, 152,
175 | 3eqtr4d 2783 |
. . . . . . . . 9
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐)) โง ((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐)))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (๐ ยท ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐))) |
177 | 176 | 3expia 1122 |
. . . . . . . 8
โข ((๐ โง ((๐ โ ๐ต โง ๐ โ ๐พ) โง (๐ โ ๐ต โง ๐ โ ๐))) โ (((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (๐ ยท ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)))) |
178 | 177 | anassrs 469 |
. . . . . . 7
โข (((๐ โง (๐ โ ๐ต โง ๐ โ ๐พ)) โง (๐ โ ๐ต โง ๐ โ ๐)) โ (((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (๐ ยท ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)))) |
179 | 178 | ralrimivva 3194 |
. . . . . 6
โข ((๐ โง (๐ โ ๐ต โง ๐ โ ๐พ)) โ โ๐ โ ๐ต โ๐ โ ๐ (((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (๐ ยท ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)))) |
180 | 179 | ralrimivva 3194 |
. . . . 5
โข (๐ โ โ๐ โ ๐ต โ๐ โ ๐พ โ๐ โ ๐ต โ๐ โ ๐ (((๐ โพ ({๐} ร ๐)) = ((({๐} ร ๐) ร {๐}) โf ยท (๐ โพ ({๐} ร ๐))) โง (๐ โพ ((๐ โ {๐}) ร ๐)) = (๐ โพ ((๐ โ {๐}) ร ๐))) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = (๐ ยท ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐)))) |
181 | | eqidd 2734 |
. . . . . 6
โข (๐ โ (๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) = (๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))) |
182 | | fveq2 6846 |
. . . . . . . 8
โข (๐ = (1rโ๐ด) โ (๐ทโ๐) = (๐ทโ(1rโ๐ด))) |
183 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = (1rโ๐ด) โ (๐ธโ๐) = (๐ธโ(1rโ๐ด))) |
184 | 183 | oveq2d 7377 |
. . . . . . . 8
โข (๐ = (1rโ๐ด) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) = ((๐ทโ(1rโ๐ด)) ยท (๐ธโ(1rโ๐ด)))) |
185 | 182, 184 | oveq12d 7379 |
. . . . . . 7
โข (๐ = (1rโ๐ด) โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ(1rโ๐ด))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ(1rโ๐ด))))) |
186 | 24, 1, 18, 5 | mdet1 21973 |
. . . . . . . . . . . 12
โข ((๐
โ CRing โง ๐ โ Fin) โ (๐ธโ(1rโ๐ด)) = 1 ) |
187 | 23, 8, 186 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐ธโ(1rโ๐ด)) = 1 ) |
188 | 187 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ(1rโ๐ด))) = ((๐ทโ(1rโ๐ด)) ยท 1 )) |
189 | 3, 7, 5 | ringridm 20001 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง (๐ทโ(1rโ๐ด)) โ ๐พ) โ ((๐ทโ(1rโ๐ด)) ยท 1 ) = (๐ทโ(1rโ๐ด))) |
190 | 9, 21, 189 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((๐ทโ(1rโ๐ด)) ยท 1 ) = (๐ทโ(1rโ๐ด))) |
191 | 188, 190 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ(1rโ๐ด))) = (๐ทโ(1rโ๐ด))) |
192 | 191 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ ((๐ทโ(1rโ๐ด))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ(1rโ๐ด)))) = ((๐ทโ(1rโ๐ด))(-gโ๐
)(๐ทโ(1rโ๐ด)))) |
193 | 3, 4, 30 | grpsubid 18839 |
. . . . . . . . 9
โข ((๐
โ Grp โง (๐ทโ(1rโ๐ด)) โ ๐พ) โ ((๐ทโ(1rโ๐ด))(-gโ๐
)(๐ทโ(1rโ๐ด))) = 0 ) |
194 | 11, 21, 193 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((๐ทโ(1rโ๐ด))(-gโ๐
)(๐ทโ(1rโ๐ด))) = 0 ) |
195 | 192, 194 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ ((๐ทโ(1rโ๐ด))(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ(1rโ๐ด)))) = 0 ) |
196 | 185, 195 | sylan9eqr 2795 |
. . . . . 6
โข ((๐ โง ๐ = (1rโ๐ด)) โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = 0 ) |
197 | 4 | fvexi 6860 |
. . . . . . 7
โข 0 โ
V |
198 | 197 | a1i 11 |
. . . . . 6
โข (๐ โ 0 โ V) |
199 | 181, 196,
20, 198 | fvmptd 6959 |
. . . . 5
โข (๐ โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ(1rโ๐ด)) = 0 ) |
200 | | eqid 2733 |
. . . . 5
โข {๐ โฃ โ๐ โ ๐ต โ๐ โ (๐ โm ๐)(โ๐ โ ๐ (๐โ๐) = if(๐ โ ๐, 1 , 0 ) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = 0 )} = {๐ โฃ โ๐ โ ๐ต โ๐ โ (๐ โm ๐)(โ๐ โ ๐ (๐โ๐) = if(๐ โ ๐, 1 , 0 ) โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐) = 0 )} |
201 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 33,
74, 136, 180, 199, 200 | mdetunilem9 21992 |
. . . 4
โข (๐ โ (๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)))) = (๐ต ร { 0 })) |
202 | 201 | fveq1d 6848 |
. . 3
โข (๐ โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐น) = ((๐ต ร { 0 })โ๐น)) |
203 | | fveq2 6846 |
. . . . . 6
โข (๐ = ๐น โ (๐ทโ๐) = (๐ทโ๐น)) |
204 | | fveq2 6846 |
. . . . . . 7
โข (๐ = ๐น โ (๐ธโ๐) = (๐ธโ๐น)) |
205 | 204 | oveq2d 7377 |
. . . . . 6
โข (๐ = ๐น โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐)) = ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น))) |
206 | 203, 205 | oveq12d 7379 |
. . . . 5
โข (๐ = ๐น โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ๐น)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น)))) |
207 | 206 | adantl 483 |
. . . 4
โข ((๐ โง ๐ = ๐น) โ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))) = ((๐ทโ๐น)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น)))) |
208 | | mdetuni.f |
. . . 4
โข (๐ โ ๐น โ ๐ต) |
209 | | ovexd 7396 |
. . . 4
โข (๐ โ ((๐ทโ๐น)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น))) โ V) |
210 | 181, 207,
208, 209 | fvmptd 6959 |
. . 3
โข (๐ โ ((๐ โ ๐ต โฆ ((๐ทโ๐)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐))))โ๐น) = ((๐ทโ๐น)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น)))) |
211 | 197 | fvconst2 7157 |
. . . 4
โข (๐น โ ๐ต โ ((๐ต ร { 0 })โ๐น) = 0 ) |
212 | 208, 211 | syl 17 |
. . 3
โข (๐ โ ((๐ต ร { 0 })โ๐น) = 0 ) |
213 | 202, 210,
212 | 3eqtr3d 2781 |
. 2
โข (๐ โ ((๐ทโ๐น)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น))) = 0 ) |
214 | 13, 208 | ffvelcdmd 7040 |
. . 3
โข (๐ โ (๐ทโ๐น) โ ๐พ) |
215 | 26, 208 | ffvelcdmd 7040 |
. . . 4
โข (๐ โ (๐ธโ๐น) โ ๐พ) |
216 | 3, 7 | ringcl 19989 |
. . . 4
โข ((๐
โ Ring โง (๐ทโ(1rโ๐ด)) โ ๐พ โง (๐ธโ๐น) โ ๐พ) โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น)) โ ๐พ) |
217 | 9, 21, 215, 216 | syl3anc 1372 |
. . 3
โข (๐ โ ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น)) โ ๐พ) |
218 | 3, 4, 30 | grpsubeq0 18841 |
. . 3
โข ((๐
โ Grp โง (๐ทโ๐น) โ ๐พ โง ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น)) โ ๐พ) โ (((๐ทโ๐น)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น))) = 0 โ (๐ทโ๐น) = ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น)))) |
219 | 11, 214, 217, 218 | syl3anc 1372 |
. 2
โข (๐ โ (((๐ทโ๐น)(-gโ๐
)((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น))) = 0 โ (๐ทโ๐น) = ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น)))) |
220 | 213, 219 | mpbid 231 |
1
โข (๐ โ (๐ทโ๐น) = ((๐ทโ(1rโ๐ด)) ยท (๐ธโ๐น))) |