Step | Hyp | Ref
| Expression |
1 | | tru 1543 |
. . 3
โข
โค |
2 | | 0fin 8992 |
. . . . . 6
โข โ
โ Fin |
3 | | 0ex 5240 |
. . . . . . . 8
โข โ
โ V |
4 | | mzpconst 40752 |
. . . . . . . 8
โข ((โ
โ V โง ๐ โ
โค) โ ((โค โm โ
) ร {๐}) โ
(mzPolyโโ
)) |
5 | 3, 4 | mpan 688 |
. . . . . . 7
โข (๐ โ โค โ ((โค
โm โ
) ร {๐}) โ
(mzPolyโโ
)) |
6 | | 0ss 4336 |
. . . . . . . 8
โข โ
โ ๐ต |
7 | 6 | a1i 11 |
. . . . . . 7
โข (๐ โ โค โ โ
โ ๐ต) |
8 | | fconstmpt 5660 |
. . . . . . . 8
โข ((โค
โm ๐ต)
ร {๐}) = (๐ โ (โค
โm ๐ต)
โฆ ๐) |
9 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ (โค
โm ๐ต))
โ ๐ โ (โค
โm ๐ต)) |
10 | | elmapssres 8686 |
. . . . . . . . . . 11
โข ((๐ โ (โค
โm ๐ต) โง
โ
โ ๐ต) โ
(๐ โพ โ
) โ
(โค โm โ
)) |
11 | 9, 6, 10 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ (โค
โm ๐ต))
โ (๐ โพ โ
)
โ (โค โm โ
)) |
12 | | vex 3441 |
. . . . . . . . . . 11
โข ๐ โ V |
13 | 12 | fvconst2 7111 |
. . . . . . . . . 10
โข ((๐ โพ โ
) โ
(โค โm โ
) โ (((โค โm
โ
) ร {๐})โ(๐ โพ โ
)) = ๐) |
14 | 11, 13 | syl 17 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ (โค
โm ๐ต))
โ (((โค โm โ
) ร {๐})โ(๐ โพ โ
)) = ๐) |
15 | 14 | mpteq2dva 5181 |
. . . . . . . 8
โข (๐ โ โค โ (๐ โ (โค
โm ๐ต)
โฆ (((โค โm โ
) ร {๐})โ(๐ โพ โ
))) = (๐ โ (โค โm ๐ต) โฆ ๐)) |
16 | 8, 15 | eqtr4id 2795 |
. . . . . . 7
โข (๐ โ โค โ ((โค
โm ๐ต)
ร {๐}) = (๐ โ (โค
โm ๐ต)
โฆ (((โค โm โ
) ร {๐})โ(๐ โพ โ
)))) |
17 | | fveq1 6803 |
. . . . . . . . . . 11
โข (๐ = ((โค โm
โ
) ร {๐})
โ (๐โ(๐ โพ โ
)) = (((โค
โm โ
) ร {๐})โ(๐ โพ โ
))) |
18 | 17 | mpteq2dv 5183 |
. . . . . . . . . 10
โข (๐ = ((โค โm
โ
) ร {๐})
โ (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ โ
))) = (๐ โ (โค
โm ๐ต)
โฆ (((โค โm โ
) ร {๐})โ(๐ โพ โ
)))) |
19 | 18 | eqeq2d 2747 |
. . . . . . . . 9
โข (๐ = ((โค โm
โ
) ร {๐})
โ (((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ
))) โ ((โค
โm ๐ต)
ร {๐}) = (๐ โ (โค
โm ๐ต)
โฆ (((โค โm โ
) ร {๐})โ(๐ โพ โ
))))) |
20 | 19 | anbi2d 630 |
. . . . . . . 8
โข (๐ = ((โค โm
โ
) ร {๐})
โ ((โ
โ ๐ต
โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ
)))) โ (โ
โ
๐ต โง ((โค
โm ๐ต)
ร {๐}) = (๐ โ (โค
โm ๐ต)
โฆ (((โค โm โ
) ร {๐})โ(๐ โพ โ
)))))) |
21 | 20 | rspcev 3566 |
. . . . . . 7
โข
((((โค โm โ
) ร {๐}) โ (mzPolyโโ
) โง
(โ
โ ๐ต โง
((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (((โค
โm โ
) ร {๐})โ(๐ โพ โ
))))) โ โ๐ โ
(mzPolyโโ
)(โ
โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ
))))) |
22 | 5, 7, 16, 21 | syl12anc 835 |
. . . . . 6
โข (๐ โ โค โ
โ๐ โ
(mzPolyโโ
)(โ
โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ
))))) |
23 | | fveq2 6804 |
. . . . . . . 8
โข (๐ = โ
โ
(mzPolyโ๐) =
(mzPolyโโ
)) |
24 | | sseq1 3951 |
. . . . . . . . 9
โข (๐ = โ
โ (๐ โ ๐ต โ โ
โ ๐ต)) |
25 | | reseq2 5898 |
. . . . . . . . . . . 12
โข (๐ = โ
โ (๐ โพ ๐) = (๐ โพ โ
)) |
26 | 25 | fveq2d 6808 |
. . . . . . . . . . 11
โข (๐ = โ
โ (๐โ(๐ โพ ๐)) = (๐โ(๐ โพ โ
))) |
27 | 26 | mpteq2dv 5183 |
. . . . . . . . . 10
โข (๐ = โ
โ (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ
)))) |
28 | 27 | eqeq2d 2747 |
. . . . . . . . 9
โข (๐ = โ
โ (((โค
โm ๐ต)
ร {๐}) = (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐))) โ ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ
))))) |
29 | 24, 28 | anbi12d 632 |
. . . . . . . 8
โข (๐ = โ
โ ((๐ โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (โ
โ ๐ต โง ((โค
โm ๐ต)
ร {๐}) = (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ
โ
)))))) |
30 | 23, 29 | rexeqbidv 3356 |
. . . . . . 7
โข (๐ = โ
โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโโ
)(โ
โ ๐ต โง ((โค
โm ๐ต)
ร {๐}) = (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ
โ
)))))) |
31 | 30 | rspcev 3566 |
. . . . . 6
โข ((โ
โ Fin โง โ๐
โ (mzPolyโโ
)(โ
โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ
))))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
32 | 2, 22, 31 | sylancr 588 |
. . . . 5
โข (๐ โ โค โ
โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
33 | 32 | adantl 483 |
. . . 4
โข
((โค โง ๐
โ โค) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
34 | | snfi 8869 |
. . . . . 6
โข {๐} โ Fin |
35 | | snex 5363 |
. . . . . . . . 9
โข {๐} โ V |
36 | | vsnid 4602 |
. . . . . . . . 9
โข ๐ โ {๐} |
37 | | mzpproj 40754 |
. . . . . . . . 9
โข (({๐} โ V โง ๐ โ {๐}) โ (๐ โ (โค โm {๐}) โฆ (๐โ๐)) โ (mzPolyโ{๐})) |
38 | 35, 36, 37 | mp2an 690 |
. . . . . . . 8
โข (๐ โ (โค
โm {๐})
โฆ (๐โ๐)) โ (mzPolyโ{๐}) |
39 | 38 | a1i 11 |
. . . . . . 7
โข (๐ โ ๐ต โ (๐ โ (โค โm {๐}) โฆ (๐โ๐)) โ (mzPolyโ{๐})) |
40 | | snssi 4747 |
. . . . . . 7
โข (๐ โ ๐ต โ {๐} โ ๐ต) |
41 | | fveq1 6803 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
42 | 41 | cbvmptv 5194 |
. . . . . . . 8
โข (๐ โ (โค
โm ๐ต)
โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) |
43 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โ ๐ต โง ๐ โ (โค โm ๐ต)) โ ๐ โ (โค โm ๐ต)) |
44 | | simpl 484 |
. . . . . . . . . . . . 13
โข ((๐ โ ๐ต โง ๐ โ (โค โm ๐ต)) โ ๐ โ ๐ต) |
45 | 44 | snssd 4748 |
. . . . . . . . . . . 12
โข ((๐ โ ๐ต โง ๐ โ (โค โm ๐ต)) โ {๐} โ ๐ต) |
46 | | elmapssres 8686 |
. . . . . . . . . . . 12
โข ((๐ โ (โค
โm ๐ต) โง
{๐} โ ๐ต) โ (๐ โพ {๐}) โ (โค โm {๐})) |
47 | 43, 45, 46 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โ ๐ต โง ๐ โ (โค โm ๐ต)) โ (๐ โพ {๐}) โ (โค โm {๐})) |
48 | | fveq1 6803 |
. . . . . . . . . . . 12
โข (๐ = (๐ โพ {๐}) โ (๐โ๐) = ((๐ โพ {๐})โ๐)) |
49 | | eqid 2736 |
. . . . . . . . . . . 12
โข (๐ โ (โค
โm {๐})
โฆ (๐โ๐)) = (๐ โ (โค โm {๐}) โฆ (๐โ๐)) |
50 | | fvex 6817 |
. . . . . . . . . . . 12
โข ((๐ โพ {๐})โ๐) โ V |
51 | 48, 49, 50 | fvmpt 6907 |
. . . . . . . . . . 11
โข ((๐ โพ {๐}) โ (โค โm {๐}) โ ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐})) = ((๐ โพ {๐})โ๐)) |
52 | 47, 51 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ ๐ต โง ๐ โ (โค โm ๐ต)) โ ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐})) = ((๐ โพ {๐})โ๐)) |
53 | | fvres 6823 |
. . . . . . . . . . 11
โข (๐ โ {๐} โ ((๐ โพ {๐})โ๐) = (๐โ๐)) |
54 | 36, 53 | ax-mp 5 |
. . . . . . . . . 10
โข ((๐ โพ {๐})โ๐) = (๐โ๐) |
55 | 52, 54 | eqtr2di 2793 |
. . . . . . . . 9
โข ((๐ โ ๐ต โง ๐ โ (โค โm ๐ต)) โ (๐โ๐) = ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐}))) |
56 | 55 | mpteq2dva 5181 |
. . . . . . . 8
โข (๐ โ ๐ต โ (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐})))) |
57 | 42, 56 | eqtrid 2788 |
. . . . . . 7
โข (๐ โ ๐ต โ (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐})))) |
58 | | fveq1 6803 |
. . . . . . . . . . 11
โข (๐ = (๐ โ (โค โm {๐}) โฆ (๐โ๐)) โ (๐โ(๐ โพ {๐})) = ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐}))) |
59 | 58 | mpteq2dv 5183 |
. . . . . . . . . 10
โข (๐ = (๐ โ (โค โm {๐}) โฆ (๐โ๐)) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐}))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐})))) |
60 | 59 | eqeq2d 2747 |
. . . . . . . . 9
โข (๐ = (๐ โ (โค โm {๐}) โฆ (๐โ๐)) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐}))) โ (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐}))))) |
61 | 60 | anbi2d 630 |
. . . . . . . 8
โข (๐ = (๐ โ (โค โm {๐}) โฆ (๐โ๐)) โ (({๐} โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐})))) โ ({๐} โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐})))))) |
62 | 61 | rspcev 3566 |
. . . . . . 7
โข (((๐ โ (โค
โm {๐})
โฆ (๐โ๐)) โ (mzPolyโ{๐}) โง ({๐} โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm {๐}) โฆ (๐โ๐))โ(๐ โพ {๐}))))) โ โ๐ โ (mzPolyโ{๐})({๐} โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐}))))) |
63 | 39, 40, 57, 62 | syl12anc 835 |
. . . . . 6
โข (๐ โ ๐ต โ โ๐ โ (mzPolyโ{๐})({๐} โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐}))))) |
64 | | fveq2 6804 |
. . . . . . . 8
โข (๐ = {๐} โ (mzPolyโ๐) = (mzPolyโ{๐})) |
65 | | sseq1 3951 |
. . . . . . . . 9
โข (๐ = {๐} โ (๐ โ ๐ต โ {๐} โ ๐ต)) |
66 | | reseq2 5898 |
. . . . . . . . . . . 12
โข (๐ = {๐} โ (๐ โพ ๐) = (๐ โพ {๐})) |
67 | 66 | fveq2d 6808 |
. . . . . . . . . . 11
โข (๐ = {๐} โ (๐โ(๐ โพ ๐)) = (๐โ(๐ โพ {๐}))) |
68 | 67 | mpteq2dv 5183 |
. . . . . . . . . 10
โข (๐ = {๐} โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐})))) |
69 | 68 | eqeq2d 2747 |
. . . . . . . . 9
โข (๐ = {๐} โ ((๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐}))))) |
70 | 65, 69 | anbi12d 632 |
. . . . . . . 8
โข (๐ = {๐} โ ((๐ โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ ({๐} โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐})))))) |
71 | 64, 70 | rexeqbidv 3356 |
. . . . . . 7
โข (๐ = {๐} โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโ{๐})({๐} โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐})))))) |
72 | 71 | rspcev 3566 |
. . . . . 6
โข (({๐} โ Fin โง โ๐ โ (mzPolyโ{๐})({๐} โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ {๐}))))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
73 | 34, 63, 72 | sylancr 588 |
. . . . 5
โข (๐ โ ๐ต โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
74 | 73 | adantl 483 |
. . . 4
โข
((โค โง ๐
โ ๐ต) โ
โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
75 | | simplll 773 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ โ โ Fin) |
76 | | simprll 777 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ๐ โ Fin) |
77 | | unfi 8993 |
. . . . . . . . . . . . . . . . . 18
โข ((โ โ Fin โง ๐ โ Fin) โ (โ โช ๐) โ Fin) |
78 | 75, 76, 77 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (โ โช ๐) โ Fin) |
79 | | vex 3441 |
. . . . . . . . . . . . . . . . . . . . . 22
โข โ โ V |
80 | | vex 3441 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ๐ โ V |
81 | 79, 80 | unex 7628 |
. . . . . . . . . . . . . . . . . . . . 21
โข (โ โช ๐) โ V |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (โ โช ๐) โ V) |
83 | | ssun1 4112 |
. . . . . . . . . . . . . . . . . . . . 21
โข โ โ (โ โช ๐) |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ โ โ (โ โช ๐)) |
85 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ๐ โ (mzPolyโโ)) |
86 | | mzpresrename 40767 |
. . . . . . . . . . . . . . . . . . . 20
โข (((โ โช ๐) โ V โง โ โ (โ โช ๐) โง ๐ โ (mzPolyโโ)) โ (๐ โ (โค โm (โ โช ๐)) โฆ (๐โ(๐ โพ โ))) โ (mzPolyโ(โ โช ๐))) |
87 | 82, 84, 85, 86 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm (โ โช ๐)) โฆ (๐โ(๐ โพ โ))) โ (mzPolyโ(โ โช ๐))) |
88 | | ssun2 4113 |
. . . . . . . . . . . . . . . . . . . . 21
โข ๐ โ (โ โช ๐) |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ๐ โ (โ โช ๐)) |
90 | | simprlr 778 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ๐ โ (mzPolyโ๐)) |
91 | | mzpresrename 40767 |
. . . . . . . . . . . . . . . . . . . 20
โข (((โ โช ๐) โ V โง ๐ โ (โ โช ๐) โง ๐ โ (mzPolyโ๐)) โ (๐ โ (โค โm (โ โช ๐)) โฆ (๐โ(๐ โพ ๐))) โ (mzPolyโ(โ โช ๐))) |
92 | 82, 89, 90, 91 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm (โ โช ๐)) โฆ (๐โ(๐ โพ ๐))) โ (mzPolyโ(โ โช ๐))) |
93 | | mzpaddmpt 40758 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โค
โm (โ โช
๐)) โฆ (๐โ(๐ โพ โ))) โ (mzPolyโ(โ โช ๐)) โง (๐ โ (โค โm (โ โช ๐)) โฆ (๐โ(๐ โพ ๐))) โ (mzPolyโ(โ โช ๐))) โ (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) โ (mzPolyโ(โ โช ๐))) |
94 | 87, 92, 93 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) โ (mzPolyโ(โ โช ๐))) |
95 | | simplr 767 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ โ โ ๐ต) |
96 | | simprr 771 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
97 | 95, 96 | unssd 4126 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (โ โช ๐) โ ๐ต) |
98 | | ovex 7340 |
. . . . . . . . . . . . . . . . . . . . 21
โข (โค
โm ๐ต)
โ V |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (โค โm ๐ต) โ V) |
100 | | mzpcompact2lem.i |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ๐ต โ V |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ๐ต โ V) |
102 | | mzpresrename 40767 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ต โ V โง โ โ ๐ต โง ๐ โ (mzPolyโโ)) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โ (mzPolyโ๐ต)) |
103 | 101, 95, 85, 102 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โ (mzPolyโ๐ต)) |
104 | | mzpf 40753 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ โ))) โ (mzPolyโ๐ต) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))):(โค โm ๐ต)โถโค) |
105 | | ffn 6630 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ โ))):(โค โm ๐ต)โถโค โ (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ โ))) Fn (โค โm ๐ต)) |
106 | 103, 104,
105 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) Fn (โค โm ๐ต)) |
107 | | mzpresrename 40767 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ต โ V โง ๐ โ ๐ต โง ๐ โ (mzPolyโ๐)) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ (mzPolyโ๐ต)) |
108 | 101, 96, 90, 107 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ (mzPolyโ๐ต)) |
109 | | mzpf 40753 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐))) โ (mzPolyโ๐ต) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))):(โค โm ๐ต)โถโค) |
110 | | ffn 6630 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐))):(โค โm ๐ต)โถโค โ (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐))) Fn (โค โm ๐ต)) |
111 | 108, 109,
110 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) Fn (โค โm ๐ต)) |
112 | | ofmpteq 7587 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((โค โm ๐ต) โ V โง (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) Fn (โค โm ๐ต) โง (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) Fn (โค โm ๐ต)) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))) |
113 | 99, 106, 111, 112 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))) |
114 | | elmapi 8668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (โค
โm ๐ต)
โ ๐:๐ตโถโค) |
115 | | fssres 6670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐:๐ตโถโค โง (โ โช ๐) โ ๐ต) โ (๐ โพ (โ โช ๐)):(โ โช ๐)โถโค) |
116 | 114, 97, 115 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((โ โ Fin
โง ๐ โ
(mzPolyโโ)) โง
โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โง ๐ โ (โค โm ๐ต)) โ (๐ โพ (โ โช ๐)):(โ โช ๐)โถโค) |
117 | | zex 12378 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข โค
โ V |
118 | 117, 81 | elmap 8690 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โพ (โ โช ๐)) โ (โค โm (โ โช ๐)) โ (๐ โพ (โ โช ๐)):(โ โช ๐)โถโค) |
119 | 116, 118 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((โ โ Fin
โง ๐ โ
(mzPolyโโ)) โง
โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โง ๐ โ (โค โm ๐ต)) โ (๐ โพ (โ โช ๐)) โ (โค โm (โ โช ๐))) |
120 | | reseq1 5897 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = (๐ โพ (โ โช ๐)) โ (๐ โพ โ) = ((๐ โพ (โ โช ๐)) โพ โ)) |
121 | 120 | fveq2d 6808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = (๐ โพ (โ โช ๐)) โ (๐โ(๐ โพ โ)) = (๐โ((๐ โพ (โ โช ๐)) โพ โ))) |
122 | | reseq1 5897 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = (๐ โพ (โ โช ๐)) โ (๐ โพ ๐) = ((๐ โพ (โ โช ๐)) โพ ๐)) |
123 | 122 | fveq2d 6808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = (๐ โพ (โ โช ๐)) โ (๐โ(๐ โพ ๐)) = (๐โ((๐ โพ (โ โช ๐)) โพ ๐))) |
124 | 121, 123 | oveq12d 7325 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = (๐ โพ (โ โช ๐)) โ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))) = ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) + (๐โ((๐ โพ (โ โช ๐)) โพ ๐)))) |
125 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (โค
โm (โ โช
๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) |
126 | | ovex 7340 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) + (๐โ((๐ โพ (โ โช ๐)) โพ ๐))) โ V |
127 | 124, 125,
126 | fvmpt 6907 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โพ (โ โช ๐)) โ (โค โm (โ โช ๐)) โ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))) = ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) + (๐โ((๐ โพ (โ โช ๐)) โพ ๐)))) |
128 | 119, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((โ โ Fin
โง ๐ โ
(mzPolyโโ)) โง
โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โง ๐ โ (โค โm ๐ต)) โ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))) = ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) + (๐โ((๐ โพ (โ โช ๐)) โพ ๐)))) |
129 | | resabs1 5933 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (โ โ (โ โช ๐) โ ((๐ โพ (โ โช ๐)) โพ โ) = (๐ โพ โ)) |
130 | 83, 129 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โพ (โ โช ๐)) โพ โ) = (๐ โพ โ) |
131 | 130 | fveq2i 6807 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐โ((๐ โพ (โ โช ๐)) โพ โ)) = (๐โ(๐ โพ โ)) |
132 | | resabs1 5933 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (โ โช ๐) โ ((๐ โพ (โ โช ๐)) โพ ๐) = (๐ โพ ๐)) |
133 | 88, 132 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โพ (โ โช ๐)) โพ ๐) = (๐ โพ ๐) |
134 | 133 | fveq2i 6807 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐โ((๐ โพ (โ โช ๐)) โพ ๐)) = (๐โ(๐ โพ ๐)) |
135 | 131, 134 | oveq12i 7319 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) + (๐โ((๐ โพ (โ โช ๐)) โพ ๐))) = ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))) |
136 | 128, 135 | eqtr2di 2793 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((โ โ Fin
โง ๐ โ
(mzPolyโโ)) โง
โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โง ๐ โ (โค โm ๐ต)) โ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))) = ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐)))) |
137 | 136 | mpteq2dva 5181 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm ๐ต) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))))) |
138 | 113, 137 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))))) |
139 | | fveq1 6803 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) โ (๐โ(๐ โพ (โ โช ๐))) = ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐)))) |
140 | 139 | mpteq2dv 5183 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))))) |
141 | 140 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) โ (((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐)))))) |
142 | 141 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) โ (((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))) โ ((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))))))) |
143 | 142 | rspcev 3566 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (โค
โm (โ โช
๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐)))) โ (mzPolyโ(โ โช ๐)) โง ((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) + (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐)))))) โ โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))))) |
144 | 94, 97, 138, 143 | syl12anc 835 |
. . . . . . . . . . . . . . . . 17
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))))) |
145 | | mzpmulmpt 40759 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โค
โm (โ โช
๐)) โฆ (๐โ(๐ โพ โ))) โ (mzPolyโ(โ โช ๐)) โง (๐ โ (โค โm (โ โช ๐)) โฆ (๐โ(๐ โพ ๐))) โ (mzPolyโ(โ โช ๐))) โ (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) โ (mzPolyโ(โ โช ๐))) |
146 | 87, 92, 145 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) โ (mzPolyโ(โ โช ๐))) |
147 | | ofmpteq 7587 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((โค โm ๐ต) โ V โง (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) Fn (โค โm ๐ต) โง (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) Fn (โค โm ๐ต)) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))) |
148 | 99, 106, 111, 147 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))) |
149 | 121, 123 | oveq12d 7325 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = (๐ โพ (โ โช ๐)) โ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))) = ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) ยท (๐โ((๐ โพ (โ โช ๐)) โพ ๐)))) |
150 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (โค
โm (โ โช
๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) |
151 | | ovex 7340 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) ยท (๐โ((๐ โพ (โ โช ๐)) โพ ๐))) โ V |
152 | 149, 150,
151 | fvmpt 6907 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โพ (โ โช ๐)) โ (โค โm (โ โช ๐)) โ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))) = ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) ยท (๐โ((๐ โพ (โ โช ๐)) โพ ๐)))) |
153 | 119, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((โ โ Fin
โง ๐ โ
(mzPolyโโ)) โง
โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โง ๐ โ (โค โm ๐ต)) โ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))) = ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) ยท (๐โ((๐ โพ (โ โช ๐)) โพ ๐)))) |
154 | 131, 134 | oveq12i 7319 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐โ((๐ โพ (โ โช ๐)) โพ โ)) ยท (๐โ((๐ โพ (โ โช ๐)) โพ ๐))) = ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))) |
155 | 153, 154 | eqtr2di 2793 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((โ โ Fin
โง ๐ โ
(mzPolyโโ)) โง
โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โง ๐ โ (โค โm ๐ต)) โ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))) = ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐)))) |
156 | 155 | mpteq2dva 5181 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ (๐ โ (โค โm ๐ต) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))))) |
157 | 148, 156 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))))) |
158 | | fveq1 6803 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) โ (๐โ(๐ โพ (โ โช ๐))) = ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐)))) |
159 | 158 | mpteq2dv 5183 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))))) |
160 | 159 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) โ (((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐)))))) |
161 | 160 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) โ (((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))) โ ((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐))))))) |
162 | 161 | rspcev 3566 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (โค
โm (โ โช
๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐)))) โ (mzPolyโ(โ โช ๐)) โง ((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ ((๐ โ (โค โm (โ โช ๐)) โฆ ((๐โ(๐ โพ โ)) ยท (๐โ(๐ โพ ๐))))โ(๐ โพ (โ โช ๐)))))) โ โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))))) |
163 | 146, 97, 157, 162 | syl12anc 835 |
. . . . . . . . . . . . . . . . 17
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))))) |
164 | | fveq2 6804 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (โ โช ๐) โ (mzPolyโ๐) = (mzPolyโ(โ โช ๐))) |
165 | | sseq1 3951 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (โ โช ๐) โ (๐ โ ๐ต โ (โ โช ๐) โ ๐ต)) |
166 | | reseq2 5898 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = (โ โช ๐) โ (๐ โพ ๐) = (๐ โพ (โ โช ๐))) |
167 | 166 | fveq2d 6808 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = (โ โช ๐) โ (๐โ(๐ โพ ๐)) = (๐โ(๐ โพ (โ โช ๐)))) |
168 | 167 | mpteq2dv 5183 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = (โ โช ๐) โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))) |
169 | 168 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (โ โช ๐) โ (((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))))) |
170 | 165, 169 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (โ โช ๐) โ ((๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ ((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))))) |
171 | 164, 170 | rexeqbidv 3356 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (โ โช ๐) โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))))) |
172 | 168 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (โ โช ๐) โ (((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))))) |
173 | 165, 172 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (โ โช ๐) โ ((๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ ((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))))) |
174 | 164, 173 | rexeqbidv 3356 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (โ โช ๐) โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))))) |
175 | 171, 174 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (โ โช ๐) โ ((โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) โ (โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))) โง โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐)))))))) |
176 | 175 | rspcev 3566 |
. . . . . . . . . . . . . . . . 17
โข (((โ โช ๐) โ Fin โง (โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))) โง โ๐ โ (mzPolyโ(โ โช ๐))((โ โช ๐) โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ (โ โช ๐))))))) โ โ๐ โ Fin (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
177 | 78, 144, 163, 176 | syl12anc 835 |
. . . . . . . . . . . . . . . 16
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง โ โ ๐ต) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ โ๐ โ Fin (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
178 | 177 | adantlrr 719 |
. . . . . . . . . . . . . . 15
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง ๐ โ ๐ต)) โ โ๐ โ Fin (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
179 | 178 | adantrrr 723 |
. . . . . . . . . . . . . 14
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ โ๐ โ Fin (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
180 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))) |
181 | | simprrr 780 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) |
182 | 180, 181 | oveq12d 7325 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ (๐ โf + ๐) = ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
183 | 182 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ ((๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
184 | 183 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ ((๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
185 | 184 | rexbidv 3172 |
. . . . . . . . . . . . . . . 16
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
186 | 180, 181 | oveq12d 7325 |
. . . . . . . . . . . . . . . . . . 19
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ (๐ โf ยท ๐) = ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐))))) |
187 | 186 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . . 18
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ ((๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
188 | 187 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ ((๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
189 | 188 | rexbidv 3172 |
. . . . . . . . . . . . . . . 16
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
190 | 185, 189 | anbi12d 632 |
. . . . . . . . . . . . . . 15
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ ((โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))))) |
191 | 190 | rexbidv 3172 |
. . . . . . . . . . . . . 14
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ (โ๐ โ Fin (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) โ โ๐ โ Fin (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf + (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โf ยท (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐)))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))))) |
192 | 179, 191 | mpbird 257 |
. . . . . . . . . . . . 13
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ โ๐ โ Fin (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
193 | | r19.40 3119 |
. . . . . . . . . . . . 13
โข
(โ๐ โ Fin
(โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
194 | 192, 193 | syl 17 |
. . . . . . . . . . . 12
โข ((((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โง (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
195 | 194 | exp32 422 |
. . . . . . . . . . 11
โข (((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โ ((๐ โ Fin โง ๐ โ (mzPolyโ๐)) โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))))) |
196 | 195 | rexlimdvv 3201 |
. . . . . . . . . 10
โข (((โ โ Fin โง ๐ โ (mzPolyโโ)) โง (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))))) |
197 | 196 | ex 414 |
. . . . . . . . 9
โข ((โ โ Fin โง ๐ โ (mzPolyโโ)) โ ((โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))))) |
198 | 197 | rexlimivv 3193 |
. . . . . . . 8
โข
(โโ โ Fin
โ๐ โ
(mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))))) |
199 | 198 | imp 408 |
. . . . . . 7
โข
((โโ โ Fin
โ๐ โ
(mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
200 | 199 | ad2ant2l 744 |
. . . . . 6
โข (((๐:(โค โm
๐ต)โถโค โง
โโ โ Fin
โ๐ โ
(mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง (๐:(โค โm ๐ต)โถโค โง
โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
201 | 200 | 3adant1 1130 |
. . . . 5
โข
((โค โง (๐:(โค โm ๐ต)โถโค โง
โโ โ Fin
โ๐ โ
(mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง (๐:(โค โm ๐ต)โถโค โง
โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โง โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
202 | 201 | simpld 496 |
. . . 4
โข
((โค โง (๐:(โค โm ๐ต)โถโค โง
โโ โ Fin
โ๐ โ
(mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง (๐:(โค โm ๐ต)โถโค โง
โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
203 | 201 | simprd 497 |
. . . 4
โข
((โค โง (๐:(โค โm ๐ต)โถโค โง
โโ โ Fin
โ๐ โ
(mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) โง (๐:(โค โm ๐ต)โถโค โง
โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
204 | | eqeq1 2740 |
. . . . . 6
โข (๐ = ((โค โm
๐ต) ร {๐}) โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
205 | 204 | anbi2d 630 |
. . . . 5
โข (๐ = ((โค โm
๐ต) ร {๐}) โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
206 | 205 | 2rexbidv 3210 |
. . . 4
โข (๐ = ((โค โm
๐ต) ร {๐}) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ((โค โm ๐ต) ร {๐}) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
207 | | eqeq1 2740 |
. . . . . 6
โข (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
208 | 207 | anbi2d 630 |
. . . . 5
โข (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
209 | 208 | 2rexbidv 3210 |
. . . 4
โข (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โ (โค โm ๐ต) โฆ (๐โ๐)) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
210 | | eqeq1 2740 |
. . . . . . 7
โข (๐ = ๐ โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
211 | 210 | anbi2d 630 |
. . . . . 6
โข (๐ = ๐ โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
212 | 211 | 2rexbidv 3210 |
. . . . 5
โข (๐ = ๐ โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
213 | | fveq2 6804 |
. . . . . . . 8
โข (๐ = โ โ (mzPolyโ๐) = (mzPolyโโ)) |
214 | | sseq1 3951 |
. . . . . . . . 9
โข (๐ = โ โ (๐ โ ๐ต โ โ โ ๐ต)) |
215 | | reseq2 5898 |
. . . . . . . . . . . 12
โข (๐ = โ โ (๐ โพ ๐) = (๐ โพ โ)) |
216 | 215 | fveq2d 6808 |
. . . . . . . . . . 11
โข (๐ = โ โ (๐โ(๐ โพ ๐)) = (๐โ(๐ โพ โ))) |
217 | 216 | mpteq2dv 5183 |
. . . . . . . . . 10
โข (๐ = โ โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))) |
218 | 217 | eqeq2d 2747 |
. . . . . . . . 9
โข (๐ = โ โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) |
219 | 214, 218 | anbi12d 632 |
. . . . . . . 8
โข (๐ = โ โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))))) |
220 | 213, 219 | rexeqbidv 3356 |
. . . . . . 7
โข (๐ = โ โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))))) |
221 | | fveq1 6803 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ(๐ โพ โ)) = (๐โ(๐ โพ โ))) |
222 | 221 | mpteq2dv 5183 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))) |
223 | 222 | eqeq2d 2747 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))) โ ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) |
224 | 223 | anbi2d 630 |
. . . . . . . 8
โข (๐ = ๐ โ ((โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))) โ (โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))))) |
225 | 224 | cbvrexvw 3223 |
. . . . . . 7
โข
(โ๐ โ
(mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))) โ โ๐ โ (mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) |
226 | 220, 225 | bitrdi 287 |
. . . . . 6
โข (๐ = โ โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))))) |
227 | 226 | cbvrexvw 3223 |
. . . . 5
โข
(โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โโ โ Fin โ๐ โ (mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ))))) |
228 | 212, 227 | bitrdi 287 |
. . . 4
โข (๐ = ๐ โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โโ โ Fin โ๐ โ (mzPolyโโ)(โ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ โ)))))) |
229 | | eqeq1 2740 |
. . . . . . 7
โข (๐ = ๐ โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
230 | 229 | anbi2d 630 |
. . . . . 6
โข (๐ = ๐ โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
231 | 230 | 2rexbidv 3210 |
. . . . 5
โข (๐ = ๐ โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
232 | | fveq2 6804 |
. . . . . . . 8
โข (๐ = ๐ โ (mzPolyโ๐) = (mzPolyโ๐)) |
233 | | sseq1 3951 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ ๐ต โ ๐ โ ๐ต)) |
234 | | reseq2 5898 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โพ ๐) = (๐ โพ ๐)) |
235 | 234 | fveq2d 6808 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ(๐ โพ ๐)) = (๐โ(๐ โพ ๐))) |
236 | 235 | mpteq2dv 5183 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) |
237 | 236 | eqeq2d 2747 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
238 | 233, 237 | anbi12d 632 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
239 | 232, 238 | rexeqbidv 3356 |
. . . . . . 7
โข (๐ = ๐ โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
240 | | fveq1 6803 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ(๐ โพ ๐)) = (๐โ(๐ โพ ๐))) |
241 | 240 | mpteq2dv 5183 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) |
242 | 241 | eqeq2d 2747 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
243 | 242 | anbi2d 630 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
244 | 243 | cbvrexvw 3223 |
. . . . . . 7
โข
(โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
245 | 239, 244 | bitrdi 287 |
. . . . . 6
โข (๐ = ๐ โ (โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
246 | 245 | cbvrexvw 3223 |
. . . . 5
โข
(โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
247 | 231, 246 | bitrdi 287 |
. . . 4
โข (๐ = ๐ โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
248 | | eqeq1 2740 |
. . . . . 6
โข (๐ = (๐ โf + ๐) โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
249 | 248 | anbi2d 630 |
. . . . 5
โข (๐ = (๐ โf + ๐) โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
250 | 249 | 2rexbidv 3210 |
. . . 4
โข (๐ = (๐ โf + ๐) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf + ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
251 | | eqeq1 2740 |
. . . . . 6
โข (๐ = (๐ โf ยท ๐) โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
252 | 251 | anbi2d 630 |
. . . . 5
โข (๐ = (๐ โf ยท ๐) โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
253 | 252 | 2rexbidv 3210 |
. . . 4
โข (๐ = (๐ โf ยท ๐) โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง (๐ โf ยท ๐) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
254 | | eqeq1 2740 |
. . . . . 6
โข (๐ = ๐ด โ (๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
255 | 254 | anbi2d 630 |
. . . . 5
โข (๐ = ๐ด โ ((๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
256 | 255 | 2rexbidv 3210 |
. . . 4
โข (๐ = ๐ด โ (โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))))) |
257 | 33, 74, 202, 203, 206, 209, 228, 247, 250, 253, 256 | mzpindd 40763 |
. . 3
โข
((โค โง ๐ด
โ (mzPolyโ๐ต))
โ โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
258 | 1, 257 | mpan 688 |
. 2
โข (๐ด โ (mzPolyโ๐ต) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
259 | | reseq1 5897 |
. . . . . . 7
โข (๐ = ๐ โ (๐ โพ ๐) = (๐ โพ ๐)) |
260 | 259 | fveq2d 6808 |
. . . . . 6
โข (๐ = ๐ โ (๐โ(๐ โพ ๐)) = (๐โ(๐ โพ ๐))) |
261 | 260 | cbvmptv 5194 |
. . . . 5
โข (๐ โ (โค
โm ๐ต)
โฆ (๐โ(๐ โพ ๐))) = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) |
262 | 261 | eqeq2i 2749 |
. . . 4
โข (๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))) โ ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) |
263 | 262 | anbi2i 624 |
. . 3
โข ((๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ (๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
264 | 263 | 2rexbii 3125 |
. 2
โข
(โ๐ โ Fin
โ๐ โ
(mzPolyโ๐)(๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐)))) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |
265 | 258, 264 | sylib 217 |
1
โข (๐ด โ (mzPolyโ๐ต) โ โ๐ โ Fin โ๐ โ (mzPolyโ๐)(๐ โ ๐ต โง ๐ด = (๐ โ (โค โm ๐ต) โฆ (๐โ(๐ โพ ๐))))) |