Proof of Theorem mzpsubmpt
Step | Hyp | Ref
| Expression |
1 | | nfmpt1 4747 |
. . . . 5
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) |
2 | 1 | nfel1 2779 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) |
3 | | nfmpt1 4747 |
. . . . 5
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) |
4 | 3 | nfel1 2779 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) |
5 | 2, 4 | nfan 1828 |
. . 3
⊢
Ⅎ𝑥((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) |
6 | | mzpf 37299 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵):(ℤ
↑𝑚 𝑉)⟶ℤ) |
7 | 6 | ad2antlr 763 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵):(ℤ ↑𝑚 𝑉)⟶ℤ) |
8 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝑥 ∈ (ℤ
↑𝑚 𝑉)) |
9 | | mptfcl 37283 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵):(ℤ ↑𝑚 𝑉)⟶ℤ → (𝑥 ∈ (ℤ
↑𝑚 𝑉) → 𝐵 ∈ ℤ)) |
10 | 7, 8, 9 | sylc 65 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐵 ∈
ℤ) |
11 | 10 | zcnd 11483 |
. . . . . 6
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐵 ∈
ℂ) |
12 | 11 | mulm1d 10482 |
. . . . 5
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (-1 ·
𝐵) = -𝐵) |
13 | 12 | oveq2d 6666 |
. . . 4
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝐴 + (-1 · 𝐵)) = (𝐴 + -𝐵)) |
14 | | mzpf 37299 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴):(ℤ
↑𝑚 𝑉)⟶ℤ) |
15 | 14 | ad2antrr 762 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴):(ℤ ↑𝑚 𝑉)⟶ℤ) |
16 | | mptfcl 37283 |
. . . . . . 7
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴):(ℤ ↑𝑚 𝑉)⟶ℤ → (𝑥 ∈ (ℤ
↑𝑚 𝑉) → 𝐴 ∈ ℤ)) |
17 | 15, 8, 16 | sylc 65 |
. . . . . 6
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐴 ∈
ℤ) |
18 | 17 | zcnd 11483 |
. . . . 5
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐴 ∈
ℂ) |
19 | 18, 11 | negsubd 10398 |
. . . 4
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝐴 + -𝐵) = (𝐴 − 𝐵)) |
20 | 13, 19 | eqtr2d 2657 |
. . 3
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵))) |
21 | 5, 20 | mpteq2da 4743 |
. 2
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴 − 𝐵)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴 + (-1 · 𝐵)))) |
22 | | elfvex 6221 |
. . . . 5
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) → 𝑉 ∈ V) |
23 | | neg1z 11413 |
. . . . 5
⊢ -1 ∈
ℤ |
24 | | mzpconstmpt 37303 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ -1 ∈
ℤ) → (𝑥 ∈
(ℤ ↑𝑚 𝑉) ↦ -1) ∈ (mzPoly‘𝑉)) |
25 | 22, 23, 24 | sylancl 694 |
. . . 4
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ -1) ∈
(mzPoly‘𝑉)) |
26 | | mzpmulmpt 37305 |
. . . 4
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ -1) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (-1 ·
𝐵)) ∈
(mzPoly‘𝑉)) |
27 | 25, 26 | mpancom 703 |
. . 3
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (-1 ·
𝐵)) ∈
(mzPoly‘𝑉)) |
28 | | mzpaddmpt 37304 |
. . 3
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (-1 ·
𝐵)) ∈
(mzPoly‘𝑉)) →
(𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝐴 + (-1 · 𝐵))) ∈ (mzPoly‘𝑉)) |
29 | 27, 28 | sylan2 491 |
. 2
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴 + (-1 · 𝐵))) ∈ (mzPoly‘𝑉)) |
30 | 21, 29 | eqeltrd 2701 |
1
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘𝑉)) |