Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . 6
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ๐) |
2 | | mdetuni.n |
. . . . . . . . 9
โข (๐ โ ๐ โ Fin) |
3 | | enrefg 8980 |
. . . . . . . . 9
โข (๐ โ Fin โ ๐ โ ๐) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ ๐) |
5 | | f1finf1o 9271 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ โ Fin) โ (๐ธ:๐โ1-1โ๐ โ ๐ธ:๐โ1-1-ontoโ๐)) |
6 | 4, 2, 5 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ธ:๐โ1-1โ๐ โ ๐ธ:๐โ1-1-ontoโ๐)) |
7 | 6 | biimpa 478 |
. . . . . 6
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ๐ธ:๐โ1-1-ontoโ๐) |
8 | | mdetuni.r |
. . . . . . . . 9
โข (๐ โ ๐
โ Ring) |
9 | | mdetuni.a |
. . . . . . . . . 10
โข ๐ด = (๐ Mat ๐
) |
10 | 9 | matring 21945 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
11 | 2, 8, 10 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ๐ด โ Ring) |
12 | | mdetuni.b |
. . . . . . . . 9
โข ๐ต = (Baseโ๐ด) |
13 | | eqid 2733 |
. . . . . . . . 9
โข
(1rโ๐ด) = (1rโ๐ด) |
14 | 12, 13 | ringidcl 20083 |
. . . . . . . 8
โข (๐ด โ Ring โ
(1rโ๐ด)
โ ๐ต) |
15 | 11, 14 | syl 17 |
. . . . . . 7
โข (๐ โ (1rโ๐ด) โ ๐ต) |
16 | 15 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ (1rโ๐ด) โ ๐ต) |
17 | | mdetuni.k |
. . . . . . 7
โข ๐พ = (Baseโ๐
) |
18 | | mdetuni.0g |
. . . . . . 7
โข 0 =
(0gโ๐
) |
19 | | mdetuni.1r |
. . . . . . 7
โข 1 =
(1rโ๐
) |
20 | | mdetuni.pg |
. . . . . . 7
โข + =
(+gโ๐
) |
21 | | mdetuni.tg |
. . . . . . 7
โข ยท =
(.rโ๐
) |
22 | | mdetuni.ff |
. . . . . . 7
โข (๐ โ ๐ท:๐ตโถ๐พ) |
23 | | mdetuni.al |
. . . . . . 7
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) |
24 | | mdetuni.li |
. . . . . . 7
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) |
25 | | mdetuni.sc |
. . . . . . 7
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) |
26 | 9, 12, 17, 18, 19, 20, 21, 2, 8, 22, 23, 24, 25 | mdetunilem7 22120 |
. . . . . 6
โข ((๐ โง ๐ธ:๐โ1-1-ontoโ๐ โง
(1rโ๐ด)
โ ๐ต) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ ((๐ธโ๐)(1rโ๐ด)๐))) = ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐ธ) ยท (๐ทโ(1rโ๐ด)))) |
27 | 1, 7, 16, 26 | syl3anc 1372 |
. . . . 5
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ ((๐ธโ๐)(1rโ๐ด)๐))) = ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐ธ) ยท (๐ทโ(1rโ๐ด)))) |
28 | 2 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ๐ โ Fin) |
29 | 28 | 3ad2ant1 1134 |
. . . . . . . 8
โข (((๐ โง ๐ธ:๐โ1-1โ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ Fin) |
30 | 8 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ๐
โ Ring) |
31 | 30 | 3ad2ant1 1134 |
. . . . . . . 8
โข (((๐ โง ๐ธ:๐โ1-1โ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐
โ Ring) |
32 | | simp1r 1199 |
. . . . . . . . . 10
โข (((๐ โง ๐ธ:๐โ1-1โ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ธ:๐โ1-1โ๐) |
33 | | f1f 6788 |
. . . . . . . . . 10
โข (๐ธ:๐โ1-1โ๐ โ ๐ธ:๐โถ๐) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
โข (((๐ โง ๐ธ:๐โ1-1โ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ธ:๐โถ๐) |
35 | | simp2 1138 |
. . . . . . . . 9
โข (((๐ โง ๐ธ:๐โ1-1โ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐) |
36 | 34, 35 | ffvelcdmd 7088 |
. . . . . . . 8
โข (((๐ โง ๐ธ:๐โ1-1โ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ธโ๐) โ ๐) |
37 | | simp3 1139 |
. . . . . . . 8
โข (((๐ โง ๐ธ:๐โ1-1โ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐) |
38 | 9, 19, 18, 29, 31, 36, 37, 13 | mat1ov 21950 |
. . . . . . 7
โข (((๐ โง ๐ธ:๐โ1-1โ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐ธโ๐)(1rโ๐ด)๐) = if((๐ธโ๐) = ๐, 1 , 0 )) |
39 | 38 | mpoeq3dva 7486 |
. . . . . 6
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ (๐ โ ๐, ๐ โ ๐ โฆ ((๐ธโ๐)(1rโ๐ด)๐)) = (๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) |
40 | 39 | fveq2d 6896 |
. . . . 5
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ ((๐ธโ๐)(1rโ๐ด)๐))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 )))) |
41 | | mdetunilem8.id |
. . . . . . . 8
โข (๐ โ (๐ทโ(1rโ๐ด)) = 0 ) |
42 | 41 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ (๐ทโ(1rโ๐ด)) = 0 ) |
43 | 42 | oveq2d 7425 |
. . . . . 6
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐ธ) ยท (๐ทโ(1rโ๐ด))) =
((((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐ธ) ยท 0 )) |
44 | | zrhpsgnmhm 21137 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ๐ โ Fin) โ
((โคRHomโ๐
)
โ (pmSgnโ๐))
โ ((SymGrpโ๐)
MndHom (mulGrpโ๐
))) |
45 | 8, 2, 44 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((โคRHomโ๐
) โ (pmSgnโ๐)) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
))) |
46 | | eqid 2733 |
. . . . . . . . . . 11
โข
(Baseโ(SymGrpโ๐)) = (Baseโ(SymGrpโ๐)) |
47 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
48 | 47, 17 | mgpbas 19993 |
. . . . . . . . . . 11
โข ๐พ =
(Baseโ(mulGrpโ๐
)) |
49 | 46, 48 | mhmf 18677 |
. . . . . . . . . 10
โข
(((โคRHomโ๐
) โ (pmSgnโ๐)) โ ((SymGrpโ๐) MndHom (mulGrpโ๐
)) โ ((โคRHomโ๐
) โ (pmSgnโ๐)):(Baseโ(SymGrpโ๐))โถ๐พ) |
50 | 45, 49 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((โคRHomโ๐
) โ (pmSgnโ๐)):(Baseโ(SymGrpโ๐))โถ๐พ) |
51 | 50 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ((โคRHomโ๐
) โ (pmSgnโ๐)):(Baseโ(SymGrpโ๐))โถ๐พ) |
52 | | eqid 2733 |
. . . . . . . . . . 11
โข
(SymGrpโ๐) =
(SymGrpโ๐) |
53 | 52, 46 | elsymgbas 19241 |
. . . . . . . . . 10
โข (๐ โ Fin โ (๐ธ โ
(Baseโ(SymGrpโ๐)) โ ๐ธ:๐โ1-1-ontoโ๐)) |
54 | 28, 53 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ (๐ธ โ (Baseโ(SymGrpโ๐)) โ ๐ธ:๐โ1-1-ontoโ๐)) |
55 | 7, 54 | mpbird 257 |
. . . . . . . 8
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ๐ธ โ (Baseโ(SymGrpโ๐))) |
56 | 51, 55 | ffvelcdmd 7088 |
. . . . . . 7
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ (((โคRHomโ๐
) โ (pmSgnโ๐))โ๐ธ) โ ๐พ) |
57 | 17, 21, 18 | ringrz 20108 |
. . . . . . 7
โข ((๐
โ Ring โง
(((โคRHomโ๐
)
โ (pmSgnโ๐))โ๐ธ) โ ๐พ) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐ธ) ยท 0 ) = 0 ) |
58 | 30, 56, 57 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐ธ) ยท 0 ) = 0 ) |
59 | 43, 58 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ ((((โคRHomโ๐
) โ (pmSgnโ๐))โ๐ธ) ยท (๐ทโ(1rโ๐ด))) = 0 ) |
60 | 27, 40, 59 | 3eqtr3d 2781 |
. . . 4
โข ((๐ โง ๐ธ:๐โ1-1โ๐) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = 0 ) |
61 | 60 | ex 414 |
. . 3
โข (๐ โ (๐ธ:๐โ1-1โ๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = 0 )) |
62 | 61 | adantr 482 |
. 2
โข ((๐ โง ๐ธ:๐โถ๐) โ (๐ธ:๐โ1-1โ๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = 0 )) |
63 | | dff13 7254 |
. . . . . 6
โข (๐ธ:๐โ1-1โ๐ โ (๐ธ:๐โถ๐ โง โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐))) |
64 | | ibar 530 |
. . . . . . 7
โข (๐ธ:๐โถ๐ โ (โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ (๐ธ:๐โถ๐ โง โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐)))) |
65 | 64 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ธ:๐โถ๐) โ (โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ (๐ธ:๐โถ๐ โง โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐)))) |
66 | 63, 65 | bitr4id 290 |
. . . . 5
โข ((๐ โง ๐ธ:๐โถ๐) โ (๐ธ:๐โ1-1โ๐ โ โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐))) |
67 | 66 | notbid 318 |
. . . 4
โข ((๐ โง ๐ธ:๐โถ๐) โ (ยฌ ๐ธ:๐โ1-1โ๐ โ ยฌ โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐))) |
68 | | rexnal 3101 |
. . . . 5
โข
(โ๐ โ
๐ ยฌ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ ยฌ โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐)) |
69 | | rexnal 3101 |
. . . . . . 7
โข
(โ๐ โ
๐ ยฌ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ ยฌ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐)) |
70 | | df-ne 2942 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ยฌ ๐ = ๐) |
71 | 70 | anbi2i 624 |
. . . . . . . . 9
โข (((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐) โ ((๐ธโ๐) = (๐ธโ๐) โง ยฌ ๐ = ๐)) |
72 | | annim 405 |
. . . . . . . . 9
โข (((๐ธโ๐) = (๐ธโ๐) โง ยฌ ๐ = ๐) โ ยฌ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐)) |
73 | 71, 72 | bitr2i 276 |
. . . . . . . 8
โข (ยฌ
((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐)) |
74 | 73 | rexbii 3095 |
. . . . . . 7
โข
(โ๐ โ
๐ ยฌ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐)) |
75 | 69, 74 | bitr3i 277 |
. . . . . 6
โข (ยฌ
โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐)) |
76 | 75 | rexbii 3095 |
. . . . 5
โข
(โ๐ โ
๐ ยฌ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐)) |
77 | 68, 76 | bitr3i 277 |
. . . 4
โข (ยฌ
โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โ ๐ = ๐) โ โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐)) |
78 | 67, 77 | bitrdi 287 |
. . 3
โข ((๐ โง ๐ธ:๐โถ๐) โ (ยฌ ๐ธ:๐โ1-1โ๐ โ โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) |
79 | | simprrl 780 |
. . . . . . 7
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ (๐ธโ๐) = (๐ธโ๐)) |
80 | | fveqeq2 6901 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐ธโ๐) = ๐ โ (๐ธโ๐) = ๐)) |
81 | 80 | ifbid 4552 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ if((๐ธโ๐) = ๐, 1 , 0 ) = if((๐ธโ๐) = ๐, 1 , 0 )) |
82 | | iftrue 4535 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))) = if((๐ธโ๐) = ๐, 1 , 0 )) |
83 | 81, 82 | eqtr4d 2776 |
. . . . . . . . . . 11
โข (๐ = ๐ โ if((๐ธโ๐) = ๐, 1 , 0 ) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )))) |
84 | | fveqeq2 6901 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((๐ธโ๐) = ๐ โ (๐ธโ๐) = ๐)) |
85 | 84 | ifbid 4552 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ if((๐ธโ๐) = ๐, 1 , 0 ) = if((๐ธโ๐) = ๐, 1 , 0 )) |
86 | | iftrue 4535 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )) = if((๐ธโ๐) = ๐, 1 , 0 )) |
87 | 85, 86 | eqtr4d 2776 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ if((๐ธโ๐) = ๐, 1 , 0 ) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))) |
88 | | iffalse 4538 |
. . . . . . . . . . . . . 14
โข (ยฌ
๐ = ๐ โ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )) = if((๐ธโ๐) = ๐, 1 , 0 )) |
89 | 88 | eqcomd 2739 |
. . . . . . . . . . . . 13
โข (ยฌ
๐ = ๐ โ if((๐ธโ๐) = ๐, 1 , 0 ) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))) |
90 | 87, 89 | pm2.61i 182 |
. . . . . . . . . . . 12
โข if((๐ธโ๐) = ๐, 1 , 0 ) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )) |
91 | | iffalse 4538 |
. . . . . . . . . . . 12
โข (ยฌ
๐ = ๐ โ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))) |
92 | 90, 91 | eqtr4id 2792 |
. . . . . . . . . . 11
โข (ยฌ
๐ = ๐ โ if((๐ธโ๐) = ๐, 1 , 0 ) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )))) |
93 | 83, 92 | pm2.61i 182 |
. . . . . . . . . 10
โข if((๐ธโ๐) = ๐, 1 , 0 ) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))) |
94 | | eqeq1 2737 |
. . . . . . . . . . . . . 14
โข ((๐ธโ๐) = (๐ธโ๐) โ ((๐ธโ๐) = ๐ โ (๐ธโ๐) = ๐)) |
95 | 94 | eqcoms 2741 |
. . . . . . . . . . . . 13
โข ((๐ธโ๐) = (๐ธโ๐) โ ((๐ธโ๐) = ๐ โ (๐ธโ๐) = ๐)) |
96 | 95 | ifbid 4552 |
. . . . . . . . . . . 12
โข ((๐ธโ๐) = (๐ธโ๐) โ if((๐ธโ๐) = ๐, 1 , 0 ) = if((๐ธโ๐) = ๐, 1 , 0 )) |
97 | 96 | ifeq1d 4548 |
. . . . . . . . . . 11
โข ((๐ธโ๐) = (๐ธโ๐) โ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))) |
98 | 97 | ifeq2d 4549 |
. . . . . . . . . 10
โข ((๐ธโ๐) = (๐ธโ๐) โ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )))) |
99 | 93, 98 | eqtrid 2785 |
. . . . . . . . 9
โข ((๐ธโ๐) = (๐ธโ๐) โ if((๐ธโ๐) = ๐, 1 , 0 ) = if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )))) |
100 | 99 | mpoeq3dv 7488 |
. . . . . . . 8
โข ((๐ธโ๐) = (๐ธโ๐) โ (๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 )) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))))) |
101 | 100 | fveq2d 6896 |
. . . . . . 7
โข ((๐ธโ๐) = (๐ธโ๐) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )))))) |
102 | 79, 101 | syl 17 |
. . . . . 6
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 )))))) |
103 | | simpll 766 |
. . . . . . 7
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ ๐) |
104 | | simprll 778 |
. . . . . . . 8
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ ๐ โ ๐) |
105 | | simprlr 779 |
. . . . . . . 8
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ ๐ โ ๐) |
106 | | simprrr 781 |
. . . . . . . 8
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ ๐ โ ๐) |
107 | 104, 105,
106 | 3jca 1129 |
. . . . . . 7
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) |
108 | 17, 19 | ringidcl 20083 |
. . . . . . . . . 10
โข (๐
โ Ring โ 1 โ ๐พ) |
109 | 8, 108 | syl 17 |
. . . . . . . . 9
โข (๐ โ 1 โ ๐พ) |
110 | 17, 18 | ring0cl 20084 |
. . . . . . . . . 10
โข (๐
โ Ring โ 0 โ ๐พ) |
111 | 8, 110 | syl 17 |
. . . . . . . . 9
โข (๐ โ 0 โ ๐พ) |
112 | 109, 111 | ifcld 4575 |
. . . . . . . 8
โข (๐ โ if((๐ธโ๐) = ๐, 1 , 0 ) โ ๐พ) |
113 | 112 | ad3antrrr 729 |
. . . . . . 7
โข ((((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โง ๐ โ ๐) โ if((๐ธโ๐) = ๐, 1 , 0 ) โ ๐พ) |
114 | | simp1ll 1237 |
. . . . . . . 8
โข ((((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐) |
115 | 109, 111 | ifcld 4575 |
. . . . . . . 8
โข (๐ โ if((๐ธโ๐) = ๐, 1 , 0 ) โ ๐พ) |
116 | 114, 115 | syl 17 |
. . . . . . 7
โข ((((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โง ๐ โ ๐ โง ๐ โ ๐) โ if((๐ธโ๐) = ๐, 1 , 0 ) โ ๐พ) |
117 | 9, 12, 17, 18, 19, 20, 21, 2, 8, 22, 23, 24, 25, 103, 107, 113, 116 | mdetunilem2 22115 |
. . . . . 6
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if(๐ = ๐, if((๐ธโ๐) = ๐, 1 , 0 ), if((๐ธโ๐) = ๐, 1 , 0 ))))) = 0 ) |
118 | 102, 117 | eqtrd 2773 |
. . . . 5
โข (((๐ โง ๐ธ:๐โถ๐) โง ((๐ โ ๐ โง ๐ โ ๐) โง ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐))) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = 0 ) |
119 | 118 | expr 458 |
. . . 4
โข (((๐ โง ๐ธ:๐โถ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = 0 )) |
120 | 119 | rexlimdvva 3212 |
. . 3
โข ((๐ โง ๐ธ:๐โถ๐) โ (โ๐ โ ๐ โ๐ โ ๐ ((๐ธโ๐) = (๐ธโ๐) โง ๐ โ ๐) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = 0 )) |
121 | 78, 120 | sylbid 239 |
. 2
โข ((๐ โง ๐ธ:๐โถ๐) โ (ยฌ ๐ธ:๐โ1-1โ๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = 0 )) |
122 | 62, 121 | pm2.61d 179 |
1
โข ((๐ โง ๐ธ:๐โถ๐) โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if((๐ธโ๐) = ๐, 1 , 0 ))) = 0 ) |