Proof of Theorem mzpsubmpt
| Step | Hyp | Ref
| Expression |
| 1 | | nfmpt1 5250 |
. . . . 5
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) |
| 2 | 1 | nfel1 2922 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) |
| 3 | | nfmpt1 5250 |
. . . . 5
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) |
| 4 | 3 | nfel1 2922 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉) |
| 5 | 2, 4 | nfan 1899 |
. . 3
⊢
Ⅎ𝑥((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) |
| 6 | | mzpf 42747 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵):(ℤ
↑m 𝑉)⟶ℤ) |
| 7 | 6 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵):(ℤ
↑m 𝑉)⟶ℤ) |
| 8 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ 𝑥 ∈ (ℤ
↑m 𝑉)) |
| 9 | | mptfcl 42731 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵):(ℤ
↑m 𝑉)⟶ℤ → (𝑥 ∈ (ℤ ↑m 𝑉) → 𝐵 ∈ ℤ)) |
| 10 | 7, 8, 9 | sylc 65 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ 𝐵 ∈
ℤ) |
| 11 | 10 | zcnd 12723 |
. . . . . 6
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ 𝐵 ∈
ℂ) |
| 12 | 11 | mulm1d 11715 |
. . . . 5
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ (-1 · 𝐵) =
-𝐵) |
| 13 | 12 | oveq2d 7447 |
. . . 4
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ (𝐴 + (-1 ·
𝐵)) = (𝐴 + -𝐵)) |
| 14 | | mzpf 42747 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴):(ℤ
↑m 𝑉)⟶ℤ) |
| 15 | 14 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴):(ℤ
↑m 𝑉)⟶ℤ) |
| 16 | | mptfcl 42731 |
. . . . . . 7
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴):(ℤ
↑m 𝑉)⟶ℤ → (𝑥 ∈ (ℤ ↑m 𝑉) → 𝐴 ∈ ℤ)) |
| 17 | 15, 8, 16 | sylc 65 |
. . . . . 6
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ 𝐴 ∈
ℤ) |
| 18 | 17 | zcnd 12723 |
. . . . 5
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ 𝐴 ∈
ℂ) |
| 19 | 18, 11 | negsubd 11626 |
. . . 4
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ (𝐴 + -𝐵) = (𝐴 − 𝐵)) |
| 20 | 13, 19 | eqtr2d 2778 |
. . 3
⊢ ((((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) ∧
𝑥 ∈ (ℤ
↑m 𝑉))
→ (𝐴 − 𝐵) = (𝐴 + (-1 · 𝐵))) |
| 21 | 5, 20 | mpteq2da 5240 |
. 2
⊢ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴 − 𝐵)) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 + (-1 · 𝐵)))) |
| 22 | | elfvex 6944 |
. . . . 5
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉) →
𝑉 ∈
V) |
| 23 | | neg1z 12653 |
. . . . 5
⊢ -1 ∈
ℤ |
| 24 | | mzpconstmpt 42751 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ -1 ∈
ℤ) → (𝑥 ∈
(ℤ ↑m 𝑉) ↦ -1) ∈ (mzPoly‘𝑉)) |
| 25 | 22, 23, 24 | sylancl 586 |
. . . 4
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ -1) ∈ (mzPoly‘𝑉)) |
| 26 | | mzpmulmpt 42753 |
. . . 4
⊢ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ -1) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (-1 · 𝐵)) ∈ (mzPoly‘𝑉)) |
| 27 | 25, 26 | mpancom 688 |
. . 3
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (-1 · 𝐵))
∈ (mzPoly‘𝑉)) |
| 28 | | mzpaddmpt 42752 |
. . 3
⊢ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (-1 · 𝐵))
∈ (mzPoly‘𝑉))
→ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴 + (-1 ·
𝐵))) ∈
(mzPoly‘𝑉)) |
| 29 | 27, 28 | sylan2 593 |
. 2
⊢ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴 + (-1 ·
𝐵))) ∈
(mzPoly‘𝑉)) |
| 30 | 21, 29 | eqeltrd 2841 |
1
⊢ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐵) ∈
(mzPoly‘𝑉)) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴 − 𝐵)) ∈ (mzPoly‘𝑉)) |