Proof of Theorem mzpsubmpt
Step | Hyp | Ref
| Expression |
1 | | nfmpt1 4982 |
. . . . 5
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) |
2 | 1 | nfel1 2948 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) |
3 | | nfmpt1 4982 |
. . . . 5
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) |
4 | 3 | nfel1 2948 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) |
5 | 2, 4 | nfan 1946 |
. . 3
⊢
Ⅎ𝑥((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) |
6 | | mzpf 38259 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵):(ℤ
↑𝑚 𝑉)⟶ℤ) |
7 | 6 | ad2antlr 717 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵):(ℤ ↑𝑚 𝑉)⟶ℤ) |
8 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝑥 ∈ (ℤ
↑𝑚 𝑉)) |
9 | | mptfcl 38243 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵):(ℤ ↑𝑚 𝑉)⟶ℤ → (𝑥 ∈ (ℤ
↑𝑚 𝑉) → 𝐵 ∈ ℤ)) |
10 | 7, 8, 9 | sylc 65 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐵 ∈
ℤ) |
11 | 10 | zcnd 11835 |
. . . . . 6
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐵 ∈
ℂ) |
12 | 11 | mulm1d 10827 |
. . . . 5
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (-1 ·
𝐵) = -𝐵) |
13 | 12 | oveq2d 6938 |
. . . 4
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝐴 + (-1 · 𝐵)) = (𝐴 + -𝐵)) |
14 | | mzpf 38259 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴):(ℤ
↑𝑚 𝑉)⟶ℤ) |
15 | 14 | ad2antrr 716 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴):(ℤ ↑𝑚 𝑉)⟶ℤ) |
16 | | mptfcl 38243 |
. . . . . . 7
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴):(ℤ ↑𝑚 𝑉)⟶ℤ → (𝑥 ∈ (ℤ
↑𝑚 𝑉) → 𝐴 ∈ ℤ)) |
17 | 15, 8, 16 | sylc 65 |
. . . . . 6
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐴 ∈
ℤ) |
18 | 17 | zcnd 11835 |
. . . . 5
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐴 ∈
ℂ) |
19 | 18, 11 | negsubd 10740 |
. . . 4
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝐴 + -𝐵) = (𝐴 − 𝐵)) |
20 | 13, 19 | eqtr2d 2815 |
. . 3
⊢ ((((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵))) |
21 | 5, 20 | mpteq2da 4978 |
. 2
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴 − 𝐵)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴 + (-1 · 𝐵)))) |
22 | | elfvex 6480 |
. . . . 5
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) → 𝑉 ∈ V) |
23 | | neg1z 11765 |
. . . . 5
⊢ -1 ∈
ℤ |
24 | | mzpconstmpt 38263 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ -1 ∈
ℤ) → (𝑥 ∈
(ℤ ↑𝑚 𝑉) ↦ -1) ∈ (mzPoly‘𝑉)) |
25 | 22, 23, 24 | sylancl 580 |
. . . 4
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ -1) ∈
(mzPoly‘𝑉)) |
26 | | mzpmulmpt 38265 |
. . . 4
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ -1) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (-1 ·
𝐵)) ∈
(mzPoly‘𝑉)) |
27 | 25, 26 | mpancom 678 |
. . 3
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (-1 ·
𝐵)) ∈
(mzPoly‘𝑉)) |
28 | | mzpaddmpt 38264 |
. . 3
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (-1 ·
𝐵)) ∈
(mzPoly‘𝑉)) →
(𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝐴 + (-1 · 𝐵))) ∈ (mzPoly‘𝑉)) |
29 | 27, 28 | sylan2 586 |
. 2
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴 + (-1 · 𝐵))) ∈ (mzPoly‘𝑉)) |
30 | 21, 29 | eqeltrd 2859 |
1
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘𝑉)) |