| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . 6
⊢ (𝑎 = 0 → (𝐴↑𝑎) = (𝐴↑0)) | 
| 2 | 1 | mpteq2dv 5243 | . . . . 5
⊢ (𝑎 = 0 → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑0))) | 
| 3 | 2 | eleq1d 2825 | . . . 4
⊢ (𝑎 = 0 → ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉) ↔ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑0)) ∈ (mzPoly‘𝑉))) | 
| 4 | 3 | imbi2d 340 | . . 3
⊢ (𝑎 = 0 → (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉)) ↔ ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑0)) ∈ (mzPoly‘𝑉)))) | 
| 5 |  | oveq2 7440 | . . . . . 6
⊢ (𝑎 = 𝑏 → (𝐴↑𝑎) = (𝐴↑𝑏)) | 
| 6 | 5 | mpteq2dv 5243 | . . . . 5
⊢ (𝑎 = 𝑏 → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑏))) | 
| 7 | 6 | eleq1d 2825 | . . . 4
⊢ (𝑎 = 𝑏 → ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉) ↔ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉))) | 
| 8 | 7 | imbi2d 340 | . . 3
⊢ (𝑎 = 𝑏 → (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉)) ↔ ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)))) | 
| 9 |  | oveq2 7440 | . . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐴↑𝑎) = (𝐴↑(𝑏 + 1))) | 
| 10 | 9 | mpteq2dv 5243 | . . . . 5
⊢ (𝑎 = (𝑏 + 1) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑(𝑏 + 1)))) | 
| 11 | 10 | eleq1d 2825 | . . . 4
⊢ (𝑎 = (𝑏 + 1) → ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉) ↔ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉))) | 
| 12 | 11 | imbi2d 340 | . . 3
⊢ (𝑎 = (𝑏 + 1) → (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉)) ↔ ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉)))) | 
| 13 |  | oveq2 7440 | . . . . . 6
⊢ (𝑎 = 𝐷 → (𝐴↑𝑎) = (𝐴↑𝐷)) | 
| 14 | 13 | mpteq2dv 5243 | . . . . 5
⊢ (𝑎 = 𝐷 → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝐷))) | 
| 15 | 14 | eleq1d 2825 | . . . 4
⊢ (𝑎 = 𝐷 → ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉) ↔ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉))) | 
| 16 | 15 | imbi2d 340 | . . 3
⊢ (𝑎 = 𝐷 → (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉)) ↔ ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉)))) | 
| 17 |  | mzpf 42752 | . . . . . . 7
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴):(ℤ
↑m 𝑉)⟶ℤ) | 
| 18 |  | zsscn 12623 | . . . . . . 7
⊢ ℤ
⊆ ℂ | 
| 19 |  | fss 6751 | . . . . . . 7
⊢ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴):(ℤ
↑m 𝑉)⟶ℤ ∧ ℤ ⊆
ℂ) → (𝑥 ∈
(ℤ ↑m 𝑉) ↦ 𝐴):(ℤ ↑m 𝑉)⟶ℂ) | 
| 20 | 17, 18, 19 | sylancl 586 | . . . . . 6
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴):(ℤ
↑m 𝑉)⟶ℂ) | 
| 21 |  | eqid 2736 | . . . . . . 7
⊢ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) = (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) | 
| 22 | 21 | fmpt 7129 | . . . . . 6
⊢
(∀𝑥 ∈
(ℤ ↑m 𝑉)𝐴 ∈ ℂ ↔ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴):(ℤ ↑m 𝑉)⟶ℂ) | 
| 23 | 20, 22 | sylibr 234 | . . . . 5
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
∀𝑥 ∈ (ℤ
↑m 𝑉)𝐴 ∈
ℂ) | 
| 24 |  | nfra1 3283 | . . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ (ℤ ↑m 𝑉)𝐴 ∈ ℂ | 
| 25 |  | rspa 3247 | . . . . . . 7
⊢
((∀𝑥 ∈
(ℤ ↑m 𝑉)𝐴 ∈ ℂ ∧ 𝑥 ∈ (ℤ ↑m 𝑉)) → 𝐴 ∈ ℂ) | 
| 26 | 25 | exp0d 14181 | . . . . . 6
⊢
((∀𝑥 ∈
(ℤ ↑m 𝑉)𝐴 ∈ ℂ ∧ 𝑥 ∈ (ℤ ↑m 𝑉)) → (𝐴↑0) = 1) | 
| 27 | 24, 26 | mpteq2da 5239 | . . . . 5
⊢
(∀𝑥 ∈
(ℤ ↑m 𝑉)𝐴 ∈ ℂ → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑0)) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 1)) | 
| 28 | 23, 27 | syl 17 | . . . 4
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑0)) =
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 1)) | 
| 29 |  | elfvex 6943 | . . . . 5
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
𝑉 ∈
V) | 
| 30 |  | 1z 12649 | . . . . 5
⊢ 1 ∈
ℤ | 
| 31 |  | mzpconstmpt 42756 | . . . . 5
⊢ ((𝑉 ∈ V ∧ 1 ∈
ℤ) → (𝑥 ∈
(ℤ ↑m 𝑉) ↦ 1) ∈ (mzPoly‘𝑉)) | 
| 32 | 29, 30, 31 | sylancl 586 | . . . 4
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ 1) ∈ (mzPoly‘𝑉)) | 
| 33 | 28, 32 | eqeltrd 2840 | . . 3
⊢ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑0)) ∈
(mzPoly‘𝑉)) | 
| 34 | 23 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → ∀𝑥 ∈ (ℤ
↑m 𝑉)𝐴 ∈
ℂ) | 
| 35 |  | simp1 1136 | . . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → 𝑏 ∈ ℕ0) | 
| 36 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑥 𝑏 ∈
ℕ0 | 
| 37 | 24, 36 | nfan 1898 | . . . . . . . 8
⊢
Ⅎ𝑥(∀𝑥 ∈ (ℤ ↑m 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) | 
| 38 | 25 | adantlr 715 | . . . . . . . . 9
⊢
(((∀𝑥 ∈
(ℤ ↑m 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) ∧ 𝑥 ∈ (ℤ
↑m 𝑉))
→ 𝐴 ∈
ℂ) | 
| 39 |  | simplr 768 | . . . . . . . . 9
⊢
(((∀𝑥 ∈
(ℤ ↑m 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) ∧ 𝑥 ∈ (ℤ
↑m 𝑉))
→ 𝑏 ∈
ℕ0) | 
| 40 | 38, 39 | expp1d 14188 | . . . . . . . 8
⊢
(((∀𝑥 ∈
(ℤ ↑m 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) ∧ 𝑥 ∈ (ℤ
↑m 𝑉))
→ (𝐴↑(𝑏 + 1)) = ((𝐴↑𝑏) · 𝐴)) | 
| 41 | 37, 40 | mpteq2da 5239 | . . . . . . 7
⊢
((∀𝑥 ∈
(ℤ ↑m 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) → (𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑(𝑏 + 1))) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ ((𝐴↑𝑏) · 𝐴))) | 
| 42 | 34, 35, 41 | syl2anc 584 | . . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑(𝑏 + 1))) = (𝑥 ∈ (ℤ ↑m 𝑉) ↦ ((𝐴↑𝑏) · 𝐴))) | 
| 43 |  | simp3 1138 | . . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) | 
| 44 |  | simp2 1137 | . . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉)) | 
| 45 |  | mzpmulmpt 42758 | . . . . . . 7
⊢ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ ((𝐴↑𝑏) · 𝐴)) ∈ (mzPoly‘𝑉)) | 
| 46 | 43, 44, 45 | syl2anc 584 | . . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ ((𝐴↑𝑏) · 𝐴)) ∈ (mzPoly‘𝑉)) | 
| 47 | 42, 46 | eqeltrd 2840 | . . . . 5
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉)) | 
| 48 | 47 | 3exp 1119 | . . . 4
⊢ (𝑏 ∈ ℕ0
→ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
((𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉)))) | 
| 49 | 48 | a2d 29 | . . 3
⊢ (𝑏 ∈ ℕ0
→ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉)))) | 
| 50 | 4, 8, 12, 16, 33, 49 | nn0ind 12715 | . 2
⊢ (𝐷 ∈ ℕ0
→ ((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) →
(𝑥 ∈ (ℤ
↑m 𝑉)
↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉))) | 
| 51 | 50 | impcom 407 | 1
⊢ (((𝑥 ∈ (ℤ
↑m 𝑉)
↦ 𝐴) ∈
(mzPoly‘𝑉) ∧
𝐷 ∈
ℕ0) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉)) |