Step | Hyp | Ref
| Expression |
1 | | mplmon2.p |
. . 3
โข ๐ = (๐ผ mPoly ๐
) |
2 | | mplmon2.v |
. . 3
โข ยท = (
ยท๐ โ๐) |
3 | | mplmon2.b |
. . 3
โข ๐ต = (Baseโ๐
) |
4 | | eqid 2733 |
. . 3
โข
(Baseโ๐) =
(Baseโ๐) |
5 | | eqid 2733 |
. . 3
โข
(.rโ๐
) = (.rโ๐
) |
6 | | mplmon2.d |
. . 3
โข ๐ท = {๐ โ (โ0
โm ๐ผ)
โฃ (โก๐ โ โ) โ
Fin} |
7 | | mplmon2.x |
. . 3
โข (๐ โ ๐ โ ๐ต) |
8 | | mplmon2.z |
. . . 4
โข 0 =
(0gโ๐
) |
9 | | mplmon2.o |
. . . 4
โข 1 =
(1rโ๐
) |
10 | | mplmon2.i |
. . . 4
โข (๐ โ ๐ผ โ ๐) |
11 | | mplmon2.r |
. . . 4
โข (๐ โ ๐
โ Ring) |
12 | | mplmon2.k |
. . . 4
โข (๐ โ ๐พ โ ๐ท) |
13 | 1, 4, 8, 9, 6, 10,
11, 12 | mplmon 21459 |
. . 3
โข (๐ โ (๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, 1 , 0 )) โ
(Baseโ๐)) |
14 | 1, 2, 3, 4, 5, 6, 7, 13 | mplvsca 21442 |
. 2
โข (๐ โ (๐ ยท (๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, 1 , 0 ))) = ((๐ท ร {๐}) โf
(.rโ๐
)(๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, 1 , 0 )))) |
15 | | ovex 7394 |
. . . . 5
โข
(โ0 โm ๐ผ) โ V |
16 | 6, 15 | rabex2 5295 |
. . . 4
โข ๐ท โ V |
17 | 16 | a1i 11 |
. . 3
โข (๐ โ ๐ท โ V) |
18 | 7 | adantr 482 |
. . 3
โข ((๐ โง ๐ฆ โ ๐ท) โ ๐ โ ๐ต) |
19 | 9 | fvexi 6860 |
. . . . 5
โข 1 โ
V |
20 | 8 | fvexi 6860 |
. . . . 5
โข 0 โ
V |
21 | 19, 20 | ifex 4540 |
. . . 4
โข if(๐ฆ = ๐พ, 1 , 0 ) โ
V |
22 | 21 | a1i 11 |
. . 3
โข ((๐ โง ๐ฆ โ ๐ท) โ if(๐ฆ = ๐พ, 1 , 0 ) โ
V) |
23 | | fconstmpt 5698 |
. . . 4
โข (๐ท ร {๐}) = (๐ฆ โ ๐ท โฆ ๐) |
24 | 23 | a1i 11 |
. . 3
โข (๐ โ (๐ท ร {๐}) = (๐ฆ โ ๐ท โฆ ๐)) |
25 | | eqidd 2734 |
. . 3
โข (๐ โ (๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, 1 , 0 )) = (๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, 1 , 0 ))) |
26 | 17, 18, 22, 24, 25 | offval2 7641 |
. 2
โข (๐ โ ((๐ท ร {๐}) โf
(.rโ๐
)(๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, 1 , 0 ))) = (๐ฆ โ ๐ท โฆ (๐(.rโ๐
)if(๐ฆ = ๐พ, 1 , 0 )))) |
27 | | oveq2 7369 |
. . . . 5
โข ( 1 = if(๐ฆ = ๐พ, 1 , 0 ) โ (๐(.rโ๐
) 1 ) = (๐(.rโ๐
)if(๐ฆ = ๐พ, 1 , 0 ))) |
28 | 27 | eqeq1d 2735 |
. . . 4
โข ( 1 = if(๐ฆ = ๐พ, 1 , 0 ) โ ((๐(.rโ๐
) 1 ) = if(๐ฆ = ๐พ, ๐, 0 ) โ (๐(.rโ๐
)if(๐ฆ = ๐พ, 1 , 0 )) = if(๐ฆ = ๐พ, ๐, 0 ))) |
29 | | oveq2 7369 |
. . . . 5
โข ( 0 = if(๐ฆ = ๐พ, 1 , 0 ) โ (๐(.rโ๐
) 0 ) = (๐(.rโ๐
)if(๐ฆ = ๐พ, 1 , 0 ))) |
30 | 29 | eqeq1d 2735 |
. . . 4
โข ( 0 = if(๐ฆ = ๐พ, 1 , 0 ) โ ((๐(.rโ๐
) 0 ) = if(๐ฆ = ๐พ, ๐, 0 ) โ (๐(.rโ๐
)if(๐ฆ = ๐พ, 1 , 0 )) = if(๐ฆ = ๐พ, ๐, 0 ))) |
31 | 3, 5, 9 | ringridm 20001 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐(.rโ๐
) 1 ) = ๐) |
32 | 11, 7, 31 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐(.rโ๐
) 1 ) = ๐) |
33 | | iftrue 4496 |
. . . . . 6
โข (๐ฆ = ๐พ โ if(๐ฆ = ๐พ, ๐, 0 ) = ๐) |
34 | 33 | eqcomd 2739 |
. . . . 5
โข (๐ฆ = ๐พ โ ๐ = if(๐ฆ = ๐พ, ๐, 0 )) |
35 | 32, 34 | sylan9eq 2793 |
. . . 4
โข ((๐ โง ๐ฆ = ๐พ) โ (๐(.rโ๐
) 1 ) = if(๐ฆ = ๐พ, ๐, 0 )) |
36 | 3, 5, 8 | ringrz 20020 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐(.rโ๐
) 0 ) = 0 ) |
37 | 11, 7, 36 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐(.rโ๐
) 0 ) = 0 ) |
38 | | iffalse 4499 |
. . . . . 6
โข (ยฌ
๐ฆ = ๐พ โ if(๐ฆ = ๐พ, ๐, 0 ) = 0 ) |
39 | 38 | eqcomd 2739 |
. . . . 5
โข (ยฌ
๐ฆ = ๐พ โ 0 = if(๐ฆ = ๐พ, ๐, 0 )) |
40 | 37, 39 | sylan9eq 2793 |
. . . 4
โข ((๐ โง ยฌ ๐ฆ = ๐พ) โ (๐(.rโ๐
) 0 ) = if(๐ฆ = ๐พ, ๐, 0 )) |
41 | 28, 30, 35, 40 | ifbothda 4528 |
. . 3
โข (๐ โ (๐(.rโ๐
)if(๐ฆ = ๐พ, 1 , 0 )) = if(๐ฆ = ๐พ, ๐, 0 )) |
42 | 41 | mpteq2dv 5211 |
. 2
โข (๐ โ (๐ฆ โ ๐ท โฆ (๐(.rโ๐
)if(๐ฆ = ๐พ, 1 , 0 ))) = (๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, ๐, 0 ))) |
43 | 14, 26, 42 | 3eqtrd 2777 |
1
โข (๐ โ (๐ ยท (๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, 1 , 0 ))) = (๐ฆ โ ๐ท โฆ if(๐ฆ = ๐พ, ๐, 0 ))) |