| Step | Hyp | Ref
| Expression |
| 1 | | zringbas 21464 |
. . . . . 6
⊢ ℤ =
(Base‘ℤring) |
| 2 | | eqid 2737 |
. . . . . . . 8
⊢ (𝐼 eval ℤring) =
(𝐼 eval
ℤring) |
| 3 | 2, 1 | evlval 22119 |
. . . . . . 7
⊢ (𝐼 eval ℤring) =
((𝐼 evalSub
ℤring)‘ℤ) |
| 4 | 3 | rneqi 5948 |
. . . . . 6
⊢ ran
(𝐼 eval
ℤring) = ran ((𝐼 evalSub
ℤring)‘ℤ) |
| 5 | | simpl 482 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ ℤ) → 𝐼 ∈ V) |
| 6 | | zringcrng 21459 |
. . . . . . 7
⊢
ℤring ∈ CRing |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ ℤ) →
ℤring ∈ CRing) |
| 8 | | zringring 21460 |
. . . . . . . 8
⊢
ℤring ∈ Ring |
| 9 | 1 | subrgid 20573 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → ℤ ∈
(SubRing‘ℤring)) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . . 7
⊢ ℤ
∈ (SubRing‘ℤring) |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ ℤ) → ℤ
∈ (SubRing‘ℤring)) |
| 12 | | simpr 484 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ ℤ) → 𝑓 ∈
ℤ) |
| 13 | 1, 4, 5, 7, 11, 12 | mpfconst 22125 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ ℤ) →
((ℤ ↑m 𝐼) × {𝑓}) ∈ ran (𝐼 eval
ℤring)) |
| 14 | | simpl 482 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ 𝐼) → 𝐼 ∈ V) |
| 15 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ 𝐼) → ℤring ∈
CRing) |
| 16 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ 𝐼) → ℤ ∈
(SubRing‘ℤring)) |
| 17 | | simpr 484 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑓 ∈ 𝐼) → 𝑓 ∈ 𝐼) |
| 18 | 1, 4, 14, 15, 16, 17 | mpfproj 22126 |
. . . . 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 21465 |
. . . . . . 7
⊢ + =
(+g‘ℤring) |
| 22 | 4, 21 | mpfaddcl 22129 |
. . . . . 6
⊢ ((𝑓 ∈ ran (𝐼 eval ℤring) ∧ 𝑔 ∈ ran (𝐼 eval ℤring)) → (𝑓 ∘f + 𝑔) ∈ ran (𝐼 eval
ℤring)) |
| 23 | 19, 20, 22 | syl2anc 584 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ (𝑓:(ℤ ↑m
𝐼)⟶ℤ ∧
𝑓 ∈ ran (𝐼 eval ℤring))
∧ (𝑔:(ℤ
↑m 𝐼)⟶ℤ ∧ 𝑔 ∈ ran (𝐼 eval ℤring))) →
(𝑓 ∘f +
𝑔) ∈ ran (𝐼 eval
ℤring)) |
| 24 | | zringmulr 21468 |
. . . . . . 7
⊢ ·
= (.r‘ℤring) |
| 25 | 4, 24 | mpfmulcl 22130 |
. . . . . 6
⊢ ((𝑓 ∈ ran (𝐼 eval ℤring) ∧ 𝑔 ∈ ran (𝐼 eval ℤring)) → (𝑓 ∘f ·
𝑔) ∈ ran (𝐼 eval
ℤring)) |
| 26 | 19, 20, 25 | syl2anc 584 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ (𝑓:(ℤ ↑m
𝐼)⟶ℤ ∧
𝑓 ∈ ran (𝐼 eval ℤring))
∧ (𝑔:(ℤ
↑m 𝐼)⟶ℤ ∧ 𝑔 ∈ ran (𝐼 eval ℤring))) →
(𝑓 ∘f
· 𝑔) ∈ ran
(𝐼 eval
ℤring)) |
| 27 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = ((ℤ ↑m
𝐼) × {𝑓}) → (𝑏 ∈ ran (𝐼 eval ℤring) ↔
((ℤ ↑m 𝐼) × {𝑓}) ∈ ran (𝐼 eval
ℤring))) |
| 28 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = (𝑔 ∈ (ℤ ↑m 𝐼) ↦ (𝑔‘𝑓)) → (𝑏 ∈ ran (𝐼 eval ℤring) ↔ (𝑔 ∈ (ℤ
↑m 𝐼)
↦ (𝑔‘𝑓)) ∈ ran (𝐼 eval
ℤring))) |
| 29 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = 𝑓 → (𝑏 ∈ ran (𝐼 eval ℤring) ↔ 𝑓 ∈ ran (𝐼 eval
ℤring))) |
| 30 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = 𝑔 → (𝑏 ∈ ran (𝐼 eval ℤring) ↔ 𝑔 ∈ ran (𝐼 eval
ℤring))) |
| 31 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = (𝑓 ∘f + 𝑔) → (𝑏 ∈ ran (𝐼 eval ℤring) ↔ (𝑓 ∘f + 𝑔) ∈ ran (𝐼 eval
ℤring))) |
| 32 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = (𝑓 ∘f · 𝑔) → (𝑏 ∈ ran (𝐼 eval ℤring) ↔ (𝑓 ∘f ·
𝑔) ∈ ran (𝐼 eval
ℤring))) |
| 33 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = 𝑎 → (𝑏 ∈ ran (𝐼 eval ℤring) ↔ 𝑎 ∈ ran (𝐼 eval
ℤring))) |
| 34 | 13, 18, 23, 26, 27, 28, 29, 30, 31, 32, 33 | mzpindd 42757 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑎 ∈ (mzPoly‘𝐼)) → 𝑎 ∈ ran (𝐼 eval
ℤring)) |
| 35 | | simprlr 780 |
. . . . . 6
⊢ (((𝐼 ∈ V ∧ 𝑎 ∈ ran (𝐼 eval ℤring)) ∧ ((𝑥 ∈ ran (𝐼 eval ℤring) ∧ 𝑥 ∈ (mzPoly‘𝐼)) ∧ (𝑦 ∈ ran (𝐼 eval ℤring) ∧ 𝑦 ∈ (mzPoly‘𝐼)))) → 𝑥 ∈ (mzPoly‘𝐼)) |
| 36 | | simprrr 782 |
. . . . . 6
⊢ (((𝐼 ∈ V ∧ 𝑎 ∈ ran (𝐼 eval ℤring)) ∧ ((𝑥 ∈ ran (𝐼 eval ℤring) ∧ 𝑥 ∈ (mzPoly‘𝐼)) ∧ (𝑦 ∈ ran (𝐼 eval ℤring) ∧ 𝑦 ∈ (mzPoly‘𝐼)))) → 𝑦 ∈ (mzPoly‘𝐼)) |
| 37 | | mzpadd 42749 |
. . . . . 6
⊢ ((𝑥 ∈ (mzPoly‘𝐼) ∧ 𝑦 ∈ (mzPoly‘𝐼)) → (𝑥 ∘f + 𝑦) ∈ (mzPoly‘𝐼)) |
| 38 | 35, 36, 37 | syl2anc 584 |
. . . . 5
⊢ (((𝐼 ∈ V ∧ 𝑎 ∈ ran (𝐼 eval ℤring)) ∧ ((𝑥 ∈ ran (𝐼 eval ℤring) ∧ 𝑥 ∈ (mzPoly‘𝐼)) ∧ (𝑦 ∈ ran (𝐼 eval ℤring) ∧ 𝑦 ∈ (mzPoly‘𝐼)))) → (𝑥 ∘f + 𝑦) ∈ (mzPoly‘𝐼)) |
| 39 | | mzpmul 42750 |
. . . . . 6
⊢ ((𝑥 ∈ (mzPoly‘𝐼) ∧ 𝑦 ∈ (mzPoly‘𝐼)) → (𝑥 ∘f · 𝑦) ∈ (mzPoly‘𝐼)) |
| 40 | 35, 36, 39 | syl2anc 584 |
. . . . 5
⊢ (((𝐼 ∈ V ∧ 𝑎 ∈ ran (𝐼 eval ℤring)) ∧ ((𝑥 ∈ ran (𝐼 eval ℤring) ∧ 𝑥 ∈ (mzPoly‘𝐼)) ∧ (𝑦 ∈ ran (𝐼 eval ℤring) ∧ 𝑦 ∈ (mzPoly‘𝐼)))) → (𝑥 ∘f · 𝑦) ∈ (mzPoly‘𝐼)) |
| 41 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = ((ℤ ↑m
𝐼) × {𝑥}) → (𝑏 ∈ (mzPoly‘𝐼) ↔ ((ℤ ↑m 𝐼) × {𝑥}) ∈ (mzPoly‘𝐼))) |
| 42 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = (𝑦 ∈ (ℤ ↑m 𝐼) ↦ (𝑦‘𝑥)) → (𝑏 ∈ (mzPoly‘𝐼) ↔ (𝑦 ∈ (ℤ ↑m 𝐼) ↦ (𝑦‘𝑥)) ∈ (mzPoly‘𝐼))) |
| 43 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = 𝑥 → (𝑏 ∈ (mzPoly‘𝐼) ↔ 𝑥 ∈ (mzPoly‘𝐼))) |
| 44 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = 𝑦 → (𝑏 ∈ (mzPoly‘𝐼) ↔ 𝑦 ∈ (mzPoly‘𝐼))) |
| 45 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = (𝑥 ∘f + 𝑦) → (𝑏 ∈ (mzPoly‘𝐼) ↔ (𝑥 ∘f + 𝑦) ∈ (mzPoly‘𝐼))) |
| 46 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = (𝑥 ∘f · 𝑦) → (𝑏 ∈ (mzPoly‘𝐼) ↔ (𝑥 ∘f · 𝑦) ∈ (mzPoly‘𝐼))) |
| 47 | | eleq1 2829 |
. . . . 5
⊢ (𝑏 = 𝑎 → (𝑏 ∈ (mzPoly‘𝐼) ↔ 𝑎 ∈ (mzPoly‘𝐼))) |
| 48 | | mzpconst 42746 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑥 ∈ ℤ) →
((ℤ ↑m 𝐼) × {𝑥}) ∈ (mzPoly‘𝐼)) |
| 49 | 48 | adantlr 715 |
. . . . 5
⊢ (((𝐼 ∈ V ∧ 𝑎 ∈ ran (𝐼 eval ℤring)) ∧ 𝑥 ∈ ℤ) →
((ℤ ↑m 𝐼) × {𝑥}) ∈ (mzPoly‘𝐼)) |
| 50 | | mzpproj 42748 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ (ℤ ↑m 𝐼) ↦ (𝑦‘𝑥)) ∈ (mzPoly‘𝐼)) |
| 51 | 50 | adantlr 715 |
. . . . 5
⊢ (((𝐼 ∈ V ∧ 𝑎 ∈ ran (𝐼 eval ℤring)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ (ℤ ↑m 𝐼) ↦ (𝑦‘𝑥)) ∈ (mzPoly‘𝐼)) |
| 52 | | simpr 484 |
. . . . 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 22131 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑎 ∈ ran (𝐼 eval ℤring)) → 𝑎 ∈ (mzPoly‘𝐼)) |
| 54 | 34, 53 | impbida 801 |
. . 3
⊢ (𝐼 ∈ V → (𝑎 ∈ (mzPoly‘𝐼) ↔ 𝑎 ∈ ran (𝐼 eval
ℤring))) |
| 55 | 54 | eqrdv 2735 |
. 2
⊢ (𝐼 ∈ V →
(mzPoly‘𝐼) = ran
(𝐼 eval
ℤring)) |
| 56 | | fvprc 6898 |
. . 3
⊢ (¬
𝐼 ∈ V →
(mzPoly‘𝐼) =
∅) |
| 57 | | df-evl 22099 |
. . . . . . 7
⊢ eval =
(𝑎 ∈ V, 𝑏 ∈ V ↦ ((𝑎 evalSub 𝑏)‘(Base‘𝑏))) |
| 58 | 57 | reldmmpo 7567 |
. . . . . 6
⊢ Rel dom
eval |
| 59 | 58 | ovprc1 7470 |
. . . . 5
⊢ (¬
𝐼 ∈ V → (𝐼 eval ℤring) =
∅) |
| 60 | 59 | rneqd 5949 |
. . . 4
⊢ (¬
𝐼 ∈ V → ran
(𝐼 eval
ℤring) = ran ∅) |
| 61 | | rn0 5936 |
. . . 4
⊢ ran
∅ = ∅ |
| 62 | 60, 61 | eqtrdi 2793 |
. . 3
⊢ (¬
𝐼 ∈ V → ran
(𝐼 eval
ℤring) = ∅) |
| 63 | 56, 62 | eqtr4d 2780 |
. 2
⊢ (¬
𝐼 ∈ V →
(mzPoly‘𝐼) = ran
(𝐼 eval
ℤring)) |
| 64 | 55, 63 | pm2.61i 182 |
1
⊢
(mzPoly‘𝐼) =
ran (𝐼 eval
ℤring) |