Step | Hyp | Ref
| Expression |
1 | | zringbas 20891 |
. . . . . 6
β’ β€ =
(Baseββ€ring) |
2 | | eqid 2733 |
. . . . . . . 8
β’ (πΌ eval β€ring) =
(πΌ eval
β€ring) |
3 | 2, 1 | evlval 21521 |
. . . . . . 7
β’ (πΌ eval β€ring) =
((πΌ evalSub
β€ring)ββ€) |
4 | 3 | rneqi 5893 |
. . . . . 6
β’ ran
(πΌ eval
β€ring) = ran ((πΌ evalSub
β€ring)ββ€) |
5 | | simpl 484 |
. . . . . 6
β’ ((πΌ β V β§ π β β€) β πΌ β V) |
6 | | zringcrng 20887 |
. . . . . . 7
β’
β€ring β CRing |
7 | 6 | a1i 11 |
. . . . . 6
β’ ((πΌ β V β§ π β β€) β
β€ring β CRing) |
8 | | zringring 20888 |
. . . . . . . 8
β’
β€ring β Ring |
9 | 1 | subrgid 20238 |
. . . . . . . 8
β’
(β€ring β Ring β β€ β
(SubRingββ€ring)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
β’ β€
β (SubRingββ€ring) |
11 | 10 | a1i 11 |
. . . . . 6
β’ ((πΌ β V β§ π β β€) β β€
β (SubRingββ€ring)) |
12 | | simpr 486 |
. . . . . 6
β’ ((πΌ β V β§ π β β€) β π β
β€) |
13 | 1, 4, 5, 7, 11, 12 | mpfconst 21527 |
. . . . 5
β’ ((πΌ β V β§ π β β€) β
((β€ βm πΌ) Γ {π}) β ran (πΌ eval
β€ring)) |
14 | | simpl 484 |
. . . . . 6
β’ ((πΌ β V β§ π β πΌ) β πΌ β V) |
15 | 6 | a1i 11 |
. . . . . 6
β’ ((πΌ β V β§ π β πΌ) β β€ring β
CRing) |
16 | 10 | a1i 11 |
. . . . . 6
β’ ((πΌ β V β§ π β πΌ) β β€ β
(SubRingββ€ring)) |
17 | | simpr 486 |
. . . . . 6
β’ ((πΌ β V β§ π β πΌ) β π β πΌ) |
18 | 1, 4, 14, 15, 16, 17 | mpfproj 21528 |
. . . . 5
β’ ((πΌ β V β§ π β πΌ) β (π β (β€ βm πΌ) β¦ (πβπ)) β ran (πΌ eval
β€ring)) |
19 | | simp2r 1201 |
. . . . . 6
β’ ((πΌ β V β§ (π:(β€ βm
πΌ)βΆβ€ β§
π β ran (πΌ eval β€ring))
β§ (π:(β€
βm πΌ)βΆβ€ β§ π β ran (πΌ eval β€ring))) β π β ran (πΌ eval
β€ring)) |
20 | | simp3r 1203 |
. . . . . 6
β’ ((πΌ β V β§ (π:(β€ βm
πΌ)βΆβ€ β§
π β ran (πΌ eval β€ring))
β§ (π:(β€
βm πΌ)βΆβ€ β§ π β ran (πΌ eval β€ring))) β π β ran (πΌ eval
β€ring)) |
21 | | zringplusg 20892 |
. . . . . . 7
β’ + =
(+gββ€ring) |
22 | 4, 21 | mpfaddcl 21531 |
. . . . . 6
β’ ((π β ran (πΌ eval β€ring) β§ π β ran (πΌ eval β€ring)) β (π βf + π) β ran (πΌ eval
β€ring)) |
23 | 19, 20, 22 | syl2anc 585 |
. . . . 5
β’ ((πΌ β V β§ (π:(β€ βm
πΌ)βΆβ€ β§
π β ran (πΌ eval β€ring))
β§ (π:(β€
βm πΌ)βΆβ€ β§ π β ran (πΌ eval β€ring))) β
(π βf +
π) β ran (πΌ eval
β€ring)) |
24 | | zringmulr 20894 |
. . . . . . 7
β’ Β·
= (.rββ€ring) |
25 | 4, 24 | mpfmulcl 21532 |
. . . . . 6
β’ ((π β ran (πΌ eval β€ring) β§ π β ran (πΌ eval β€ring)) β (π βf Β·
π) β ran (πΌ eval
β€ring)) |
26 | 19, 20, 25 | syl2anc 585 |
. . . . 5
β’ ((πΌ β V β§ (π:(β€ βm
πΌ)βΆβ€ β§
π β ran (πΌ eval β€ring))
β§ (π:(β€
βm πΌ)βΆβ€ β§ π β ran (πΌ eval β€ring))) β
(π βf
Β· π) β ran
(πΌ eval
β€ring)) |
27 | | eleq1 2822 |
. . . . 5
β’ (π = ((β€ βm
πΌ) Γ {π}) β (π β ran (πΌ eval β€ring) β
((β€ βm πΌ) Γ {π}) β ran (πΌ eval
β€ring))) |
28 | | eleq1 2822 |
. . . . 5
β’ (π = (π β (β€ βm πΌ) β¦ (πβπ)) β (π β ran (πΌ eval β€ring) β (π β (β€
βm πΌ)
β¦ (πβπ)) β ran (πΌ eval
β€ring))) |
29 | | eleq1 2822 |
. . . . 5
β’ (π = π β (π β ran (πΌ eval β€ring) β π β ran (πΌ eval
β€ring))) |
30 | | eleq1 2822 |
. . . . 5
β’ (π = π β (π β ran (πΌ eval β€ring) β π β ran (πΌ eval
β€ring))) |
31 | | eleq1 2822 |
. . . . 5
β’ (π = (π βf + π) β (π β ran (πΌ eval β€ring) β (π βf + π) β ran (πΌ eval
β€ring))) |
32 | | eleq1 2822 |
. . . . 5
β’ (π = (π βf Β· π) β (π β ran (πΌ eval β€ring) β (π βf Β·
π) β ran (πΌ eval
β€ring))) |
33 | | eleq1 2822 |
. . . . 5
β’ (π = π β (π β ran (πΌ eval β€ring) β π β ran (πΌ eval
β€ring))) |
34 | 13, 18, 23, 26, 27, 28, 29, 30, 31, 32, 33 | mzpindd 41112 |
. . . 4
β’ ((πΌ β V β§ π β (mzPolyβπΌ)) β π β ran (πΌ eval
β€ring)) |
35 | | simprlr 779 |
. . . . . 6
β’ (((πΌ β V β§ π β ran (πΌ eval β€ring)) β§ ((π₯ β ran (πΌ eval β€ring) β§ π₯ β (mzPolyβπΌ)) β§ (π¦ β ran (πΌ eval β€ring) β§ π¦ β (mzPolyβπΌ)))) β π₯ β (mzPolyβπΌ)) |
36 | | simprrr 781 |
. . . . . 6
β’ (((πΌ β V β§ π β ran (πΌ eval β€ring)) β§ ((π₯ β ran (πΌ eval β€ring) β§ π₯ β (mzPolyβπΌ)) β§ (π¦ β ran (πΌ eval β€ring) β§ π¦ β (mzPolyβπΌ)))) β π¦ β (mzPolyβπΌ)) |
37 | | mzpadd 41104 |
. . . . . 6
β’ ((π₯ β (mzPolyβπΌ) β§ π¦ β (mzPolyβπΌ)) β (π₯ βf + π¦) β (mzPolyβπΌ)) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . 5
β’ (((πΌ β V β§ π β ran (πΌ eval β€ring)) β§ ((π₯ β ran (πΌ eval β€ring) β§ π₯ β (mzPolyβπΌ)) β§ (π¦ β ran (πΌ eval β€ring) β§ π¦ β (mzPolyβπΌ)))) β (π₯ βf + π¦) β (mzPolyβπΌ)) |
39 | | mzpmul 41105 |
. . . . . 6
β’ ((π₯ β (mzPolyβπΌ) β§ π¦ β (mzPolyβπΌ)) β (π₯ βf Β· π¦) β (mzPolyβπΌ)) |
40 | 35, 36, 39 | syl2anc 585 |
. . . . 5
β’ (((πΌ β V β§ π β ran (πΌ eval β€ring)) β§ ((π₯ β ran (πΌ eval β€ring) β§ π₯ β (mzPolyβπΌ)) β§ (π¦ β ran (πΌ eval β€ring) β§ π¦ β (mzPolyβπΌ)))) β (π₯ βf Β· π¦) β (mzPolyβπΌ)) |
41 | | eleq1 2822 |
. . . . 5
β’ (π = ((β€ βm
πΌ) Γ {π₯}) β (π β (mzPolyβπΌ) β ((β€ βm πΌ) Γ {π₯}) β (mzPolyβπΌ))) |
42 | | eleq1 2822 |
. . . . 5
β’ (π = (π¦ β (β€ βm πΌ) β¦ (π¦βπ₯)) β (π β (mzPolyβπΌ) β (π¦ β (β€ βm πΌ) β¦ (π¦βπ₯)) β (mzPolyβπΌ))) |
43 | | eleq1 2822 |
. . . . 5
β’ (π = π₯ β (π β (mzPolyβπΌ) β π₯ β (mzPolyβπΌ))) |
44 | | eleq1 2822 |
. . . . 5
β’ (π = π¦ β (π β (mzPolyβπΌ) β π¦ β (mzPolyβπΌ))) |
45 | | eleq1 2822 |
. . . . 5
β’ (π = (π₯ βf + π¦) β (π β (mzPolyβπΌ) β (π₯ βf + π¦) β (mzPolyβπΌ))) |
46 | | eleq1 2822 |
. . . . 5
β’ (π = (π₯ βf Β· π¦) β (π β (mzPolyβπΌ) β (π₯ βf Β· π¦) β (mzPolyβπΌ))) |
47 | | eleq1 2822 |
. . . . 5
β’ (π = π β (π β (mzPolyβπΌ) β π β (mzPolyβπΌ))) |
48 | | mzpconst 41101 |
. . . . . 6
β’ ((πΌ β V β§ π₯ β β€) β
((β€ βm πΌ) Γ {π₯}) β (mzPolyβπΌ)) |
49 | 48 | adantlr 714 |
. . . . 5
β’ (((πΌ β V β§ π β ran (πΌ eval β€ring)) β§ π₯ β β€) β
((β€ βm πΌ) Γ {π₯}) β (mzPolyβπΌ)) |
50 | | mzpproj 41103 |
. . . . . 6
β’ ((πΌ β V β§ π₯ β πΌ) β (π¦ β (β€ βm πΌ) β¦ (π¦βπ₯)) β (mzPolyβπΌ)) |
51 | 50 | adantlr 714 |
. . . . 5
β’ (((πΌ β V β§ π β ran (πΌ eval β€ring)) β§ π₯ β πΌ) β (π¦ β (β€ βm πΌ) β¦ (π¦βπ₯)) β (mzPolyβπΌ)) |
52 | | simpr 486 |
. . . . 5
β’ ((πΌ β V β§ π β ran (πΌ eval β€ring)) β π β ran (πΌ eval
β€ring)) |
53 | 1, 21, 24, 4, 38, 40, 41, 42, 43, 44, 45, 46, 47, 49, 51, 52 | mpfind 21533 |
. . . 4
β’ ((πΌ β V β§ π β ran (πΌ eval β€ring)) β π β (mzPolyβπΌ)) |
54 | 34, 53 | impbida 800 |
. . 3
β’ (πΌ β V β (π β (mzPolyβπΌ) β π β ran (πΌ eval
β€ring))) |
55 | 54 | eqrdv 2731 |
. 2
β’ (πΌ β V β
(mzPolyβπΌ) = ran
(πΌ eval
β€ring)) |
56 | | fvprc 6835 |
. . 3
β’ (Β¬
πΌ β V β
(mzPolyβπΌ) =
β
) |
57 | | df-evl 21499 |
. . . . . . 7
β’ eval =
(π β V, π β V β¦ ((π evalSub π)β(Baseβπ))) |
58 | 57 | reldmmpo 7491 |
. . . . . 6
β’ Rel dom
eval |
59 | 58 | ovprc1 7397 |
. . . . 5
β’ (Β¬
πΌ β V β (πΌ eval β€ring) =
β
) |
60 | 59 | rneqd 5894 |
. . . 4
β’ (Β¬
πΌ β V β ran
(πΌ eval
β€ring) = ran β
) |
61 | | rn0 5882 |
. . . 4
β’ ran
β
= β
|
62 | 60, 61 | eqtrdi 2789 |
. . 3
β’ (Β¬
πΌ β V β ran
(πΌ eval
β€ring) = β
) |
63 | 56, 62 | eqtr4d 2776 |
. 2
β’ (Β¬
πΌ β V β
(mzPolyβπΌ) = ran
(πΌ eval
β€ring)) |
64 | 55, 63 | pm2.61i 182 |
1
β’
(mzPolyβπΌ) =
ran (πΌ eval
β€ring) |