| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | coe1tmmul.r | . . 3
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 2 |  | coe1tmmul.a | . . 3
⊢ (𝜑 → 𝐴 ∈ 𝐵) | 
| 3 |  | coe1tmmul.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ 𝐾) | 
| 4 |  | coe1tmmul.d | . . . 4
⊢ (𝜑 → 𝐷 ∈
ℕ0) | 
| 5 |  | coe1tm.k | . . . . 5
⊢ 𝐾 = (Base‘𝑅) | 
| 6 |  | coe1tm.p | . . . . 5
⊢ 𝑃 = (Poly1‘𝑅) | 
| 7 |  | coe1tm.x | . . . . 5
⊢ 𝑋 = (var1‘𝑅) | 
| 8 |  | coe1tm.m | . . . . 5
⊢  · = (
·𝑠 ‘𝑃) | 
| 9 |  | coe1tm.n | . . . . 5
⊢ 𝑁 = (mulGrp‘𝑃) | 
| 10 |  | coe1tm.e | . . . . 5
⊢  ↑ =
(.g‘𝑁) | 
| 11 |  | coe1tmmul.b | . . . . 5
⊢ 𝐵 = (Base‘𝑃) | 
| 12 | 5, 6, 7, 8, 9, 10,
11 | ply1tmcl 22275 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) | 
| 13 | 1, 3, 4, 12 | syl3anc 1373 | . . 3
⊢ (𝜑 → (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) | 
| 14 |  | coe1tmmul.t | . . . 4
⊢  ∙ =
(.r‘𝑃) | 
| 15 |  | coe1tmmul.u | . . . 4
⊢  × =
(.r‘𝑅) | 
| 16 | 6, 14, 15, 11 | coe1mul 22273 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ∧ (𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵) → (coe1‘(𝐴 ∙ (𝐶 · (𝐷 ↑ 𝑋)))) = (𝑥 ∈ ℕ0 ↦ (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))))) | 
| 17 | 1, 2, 13, 16 | syl3anc 1373 | . 2
⊢ (𝜑 →
(coe1‘(𝐴
∙
(𝐶 · (𝐷 ↑ 𝑋)))) = (𝑥 ∈ ℕ0 ↦ (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))))) | 
| 18 |  | eqeq2 2749 | . . . 4
⊢
((((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶) = if(𝐷 ≤ 𝑥, (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶), 0 ) → ((𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶) ↔ (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = if(𝐷 ≤ 𝑥, (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶), 0 ))) | 
| 19 |  | eqeq2 2749 | . . . 4
⊢ ( 0 = if(𝐷 ≤ 𝑥, (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶), 0 ) → ((𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = 0 ↔ (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = if(𝐷 ≤ 𝑥, (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶), 0 ))) | 
| 20 |  | coe1tm.z | . . . . . . 7
⊢  0 =
(0g‘𝑅) | 
| 21 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝑅 ∈ Ring) | 
| 22 |  | ringmnd 20240 | . . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 23 | 21, 22 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝑅 ∈ Mnd) | 
| 24 |  | ovex 7464 | . . . . . . . 8
⊢
(0...𝑥) ∈
V | 
| 25 | 24 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (0...𝑥) ∈ V) | 
| 26 |  | simprr 773 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝐷 ≤ 𝑥) | 
| 27 | 4 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝐷 ∈
ℕ0) | 
| 28 |  | simprl 771 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝑥 ∈ ℕ0) | 
| 29 |  | nn0sub 12576 | . . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ0
∧ 𝑥 ∈
ℕ0) → (𝐷 ≤ 𝑥 ↔ (𝑥 − 𝐷) ∈
ℕ0)) | 
| 30 | 27, 28, 29 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (𝐷 ≤ 𝑥 ↔ (𝑥 − 𝐷) ∈
ℕ0)) | 
| 31 | 26, 30 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (𝑥 − 𝐷) ∈
ℕ0) | 
| 32 | 27 | nn0ge0d 12590 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐷) | 
| 33 |  | nn0re 12535 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) | 
| 34 | 33 | ad2antrl 728 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝑥 ∈ ℝ) | 
| 35 | 4 | nn0red 12588 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 36 | 35 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝐷 ∈ ℝ) | 
| 37 | 34, 36 | subge02d 11855 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (0 ≤ 𝐷 ↔ (𝑥 − 𝐷) ≤ 𝑥)) | 
| 38 | 32, 37 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (𝑥 − 𝐷) ≤ 𝑥) | 
| 39 |  | fznn0 13659 | . . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ ((𝑥 − 𝐷) ∈ (0...𝑥) ↔ ((𝑥 − 𝐷) ∈ ℕ0 ∧ (𝑥 − 𝐷) ≤ 𝑥))) | 
| 40 | 39 | ad2antrl 728 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → ((𝑥 − 𝐷) ∈ (0...𝑥) ↔ ((𝑥 − 𝐷) ∈ ℕ0 ∧ (𝑥 − 𝐷) ≤ 𝑥))) | 
| 41 | 31, 38, 40 | mpbir2and 713 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (𝑥 − 𝐷) ∈ (0...𝑥)) | 
| 42 | 1 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → 𝑅 ∈ Ring) | 
| 43 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(coe1‘𝐴) = (coe1‘𝐴) | 
| 44 | 43, 11, 6, 5 | coe1f 22213 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝐵 → (coe1‘𝐴):ℕ0⟶𝐾) | 
| 45 | 2, 44 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 →
(coe1‘𝐴):ℕ0⟶𝐾) | 
| 46 | 45 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → (coe1‘𝐴):ℕ0⟶𝐾) | 
| 47 |  | elfznn0 13660 | . . . . . . . . . . 11
⊢ (𝑦 ∈ (0...𝑥) → 𝑦 ∈ ℕ0) | 
| 48 | 47 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → 𝑦 ∈ ℕ0) | 
| 49 | 46, 48 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → ((coe1‘𝐴)‘𝑦) ∈ 𝐾) | 
| 50 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(coe1‘(𝐶 · (𝐷 ↑ 𝑋))) = (coe1‘(𝐶 · (𝐷 ↑ 𝑋))) | 
| 51 | 50, 11, 6, 5 | coe1f 22213 | . . . . . . . . . . . 12
⊢ ((𝐶 · (𝐷 ↑ 𝑋)) ∈ 𝐵 → (coe1‘(𝐶 · (𝐷 ↑ 𝑋))):ℕ0⟶𝐾) | 
| 52 | 13, 51 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 →
(coe1‘(𝐶
·
(𝐷 ↑ 𝑋))):ℕ0⟶𝐾) | 
| 53 | 52 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → (coe1‘(𝐶 · (𝐷 ↑ 𝑋))):ℕ0⟶𝐾) | 
| 54 |  | fznn0sub 13596 | . . . . . . . . . . 11
⊢ (𝑦 ∈ (0...𝑥) → (𝑥 − 𝑦) ∈
ℕ0) | 
| 55 | 54 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → (𝑥 − 𝑦) ∈
ℕ0) | 
| 56 | 53, 55 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)) ∈ 𝐾) | 
| 57 | 5, 15 | ringcl 20247 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧
((coe1‘𝐴)‘𝑦) ∈ 𝐾 ∧ ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)) ∈ 𝐾) → (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))) ∈ 𝐾) | 
| 58 | 42, 49, 56, 57 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))) ∈ 𝐾) | 
| 59 | 58 | fmpttd 7135 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)))):(0...𝑥)⟶𝐾) | 
| 60 | 1 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → 𝑅 ∈ Ring) | 
| 61 | 3 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → 𝐶 ∈ 𝐾) | 
| 62 | 4 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → 𝐷 ∈
ℕ0) | 
| 63 |  | eldifi 4131 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)}) → 𝑦 ∈ (0...𝑥)) | 
| 64 | 63, 54 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)}) → (𝑥 − 𝑦) ∈
ℕ0) | 
| 65 | 64 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → (𝑥 − 𝑦) ∈
ℕ0) | 
| 66 |  | eldifsn 4786 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)}) ↔ (𝑦 ∈ (0...𝑥) ∧ 𝑦 ≠ (𝑥 − 𝐷))) | 
| 67 |  | simplrl 777 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → 𝑥 ∈ ℕ0) | 
| 68 | 67 | nn0cnd 12589 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → 𝑥 ∈ ℂ) | 
| 69 | 47 | nn0cnd 12589 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (0...𝑥) → 𝑦 ∈ ℂ) | 
| 70 | 69 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → 𝑦 ∈ ℂ) | 
| 71 | 68, 70 | nncand 11625 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → (𝑥 − (𝑥 − 𝑦)) = 𝑦) | 
| 72 | 71 | eqcomd 2743 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → 𝑦 = (𝑥 − (𝑥 − 𝑦))) | 
| 73 |  | oveq2 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝐷 = (𝑥 − 𝑦) → (𝑥 − 𝐷) = (𝑥 − (𝑥 − 𝑦))) | 
| 74 | 73 | eqeq2d 2748 | . . . . . . . . . . . . . . 15
⊢ (𝐷 = (𝑥 − 𝑦) → (𝑦 = (𝑥 − 𝐷) ↔ 𝑦 = (𝑥 − (𝑥 − 𝑦)))) | 
| 75 | 72, 74 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → (𝐷 = (𝑥 − 𝑦) → 𝑦 = (𝑥 − 𝐷))) | 
| 76 | 75 | necon3d 2961 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → (𝑦 ≠ (𝑥 − 𝐷) → 𝐷 ≠ (𝑥 − 𝑦))) | 
| 77 | 76 | impr 454 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ (𝑦 ∈ (0...𝑥) ∧ 𝑦 ≠ (𝑥 − 𝐷))) → 𝐷 ≠ (𝑥 − 𝑦)) | 
| 78 | 66, 77 | sylan2b 594 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → 𝐷 ≠ (𝑥 − 𝑦)) | 
| 79 | 20, 5, 6, 7, 8, 9, 10, 60, 61, 62, 65, 78 | coe1tmfv2 22278 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)) = 0 ) | 
| 80 | 79 | oveq2d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))) = (((coe1‘𝐴)‘𝑦) × 0 )) | 
| 81 | 5, 15, 20 | ringrz 20291 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
((coe1‘𝐴)‘𝑦) ∈ 𝐾) → (((coe1‘𝐴)‘𝑦) × 0 ) = 0 ) | 
| 82 | 42, 49, 81 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ (0...𝑥)) → (((coe1‘𝐴)‘𝑦) × 0 ) = 0 ) | 
| 83 | 63, 82 | sylan2 593 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → (((coe1‘𝐴)‘𝑦) × 0 ) = 0 ) | 
| 84 | 80, 83 | eqtrd 2777 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) ∧ 𝑦 ∈ ((0...𝑥) ∖ {(𝑥 − 𝐷)})) → (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))) = 0 ) | 
| 85 | 84, 25 | suppss2 8225 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)))) supp 0 ) ⊆ {(𝑥 − 𝐷)}) | 
| 86 | 5, 20, 23, 25, 41, 59, 85 | gsumpt 19980 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))‘(𝑥 − 𝐷))) | 
| 87 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑦 = (𝑥 − 𝐷) → ((coe1‘𝐴)‘𝑦) = ((coe1‘𝐴)‘(𝑥 − 𝐷))) | 
| 88 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑦 = (𝑥 − 𝐷) → (𝑥 − 𝑦) = (𝑥 − (𝑥 − 𝐷))) | 
| 89 | 88 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑦 = (𝑥 − 𝐷) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)) = ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘(𝑥 − (𝑥 − 𝐷)))) | 
| 90 | 87, 89 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑦 = (𝑥 − 𝐷) → (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))) = (((coe1‘𝐴)‘(𝑥 − 𝐷)) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − (𝑥 − 𝐷))))) | 
| 91 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)))) = (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)))) | 
| 92 |  | ovex 7464 | . . . . . . . 8
⊢
(((coe1‘𝐴)‘(𝑥 − 𝐷)) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − (𝑥 − 𝐷)))) ∈ V | 
| 93 | 90, 91, 92 | fvmpt 7016 | . . . . . . 7
⊢ ((𝑥 − 𝐷) ∈ (0...𝑥) → ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))‘(𝑥 − 𝐷)) = (((coe1‘𝐴)‘(𝑥 − 𝐷)) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − (𝑥 − 𝐷))))) | 
| 94 | 41, 93 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → ((𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))‘(𝑥 − 𝐷)) = (((coe1‘𝐴)‘(𝑥 − 𝐷)) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − (𝑥 − 𝐷))))) | 
| 95 | 28 | nn0cnd 12589 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝑥 ∈ ℂ) | 
| 96 | 27 | nn0cnd 12589 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝐷 ∈ ℂ) | 
| 97 | 95, 96 | nncand 11625 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (𝑥 − (𝑥 − 𝐷)) = 𝐷) | 
| 98 | 97 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘(𝑥 − (𝑥 − 𝐷))) = ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷)) | 
| 99 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → 𝐶 ∈ 𝐾) | 
| 100 | 20, 5, 6, 7, 8, 9, 10 | coe1tmfv1 22277 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘𝐷) = 𝐶) | 
| 101 | 21, 99, 27, 100 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘𝐷) = 𝐶) | 
| 102 | 98, 101 | eqtrd 2777 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘(𝑥 − (𝑥 − 𝐷))) = 𝐶) | 
| 103 | 102 | oveq2d 7447 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (((coe1‘𝐴)‘(𝑥 − 𝐷)) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − (𝑥 − 𝐷)))) = (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶)) | 
| 104 | 86, 94, 103 | 3eqtrd 2781 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℕ0 ∧ 𝐷 ≤ 𝑥)) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶)) | 
| 105 | 104 | anassrs 467 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶)) | 
| 106 | 1 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝑅 ∈ Ring) | 
| 107 | 3 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝐶 ∈ 𝐾) | 
| 108 | 4 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝐷 ∈
ℕ0) | 
| 109 | 54 | ad2antll 729 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (𝑥 − 𝑦) ∈
ℕ0) | 
| 110 | 54 | nn0red 12588 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0...𝑥) → (𝑥 − 𝑦) ∈ ℝ) | 
| 111 | 110 | ad2antll 729 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (𝑥 − 𝑦) ∈ ℝ) | 
| 112 | 33 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝑥 ∈ ℝ) | 
| 113 | 35 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝐷 ∈ ℝ) | 
| 114 | 47 | ad2antll 729 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝑦 ∈ ℕ0) | 
| 115 | 114 | nn0ge0d 12590 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 0 ≤ 𝑦) | 
| 116 | 47 | nn0red 12588 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...𝑥) → 𝑦 ∈ ℝ) | 
| 117 | 116 | ad2antll 729 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝑦 ∈ ℝ) | 
| 118 | 112, 117 | subge02d 11855 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (0 ≤ 𝑦 ↔ (𝑥 − 𝑦) ≤ 𝑥)) | 
| 119 | 115, 118 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (𝑥 − 𝑦) ≤ 𝑥) | 
| 120 |  | simprl 771 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → ¬ 𝐷 ≤ 𝑥) | 
| 121 | 112, 113 | ltnled 11408 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (𝑥 < 𝐷 ↔ ¬ 𝐷 ≤ 𝑥)) | 
| 122 | 120, 121 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝑥 < 𝐷) | 
| 123 | 111, 112,
113, 119, 122 | lelttrd 11419 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (𝑥 − 𝑦) < 𝐷) | 
| 124 | 111, 123 | gtned 11396 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → 𝐷 ≠ (𝑥 − 𝑦)) | 
| 125 | 20, 5, 6, 7, 8, 9, 10, 106, 107, 108, 109, 124 | coe1tmfv2 22278 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → ((coe1‘(𝐶 · (𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)) = 0 ) | 
| 126 | 125 | oveq2d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))) = (((coe1‘𝐴)‘𝑦) × 0 )) | 
| 127 | 45 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (coe1‘𝐴):ℕ0⟶𝐾) | 
| 128 | 127, 114 | ffvelcdmd 7105 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → ((coe1‘𝐴)‘𝑦) ∈ 𝐾) | 
| 129 | 106, 128,
81 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (((coe1‘𝐴)‘𝑦) × 0 ) = 0 ) | 
| 130 | 126, 129 | eqtrd 2777 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ (¬
𝐷 ≤ 𝑥 ∧ 𝑦 ∈ (0...𝑥))) → (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))) = 0 ) | 
| 131 | 130 | anassrs 467 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) ∧ 𝑦 ∈ (0...𝑥)) → (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))) = 0 ) | 
| 132 | 131 | mpteq2dva 5242 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)))) = (𝑦 ∈ (0...𝑥) ↦ 0 )) | 
| 133 | 132 | oveq2d 7447 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ 0 ))) | 
| 134 | 1, 22 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Mnd) | 
| 135 | 20 | gsumz 18849 | . . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ (0...𝑥) ∈ V) → (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦ 0 )) = 0 ) | 
| 136 | 134, 24, 135 | sylancl 586 | . . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ 0 )) = 0 ) | 
| 137 | 136 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ 0 )) = 0 ) | 
| 138 | 133, 137 | eqtrd 2777 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ ¬
𝐷 ≤ 𝑥) → (𝑅 Σg (𝑦 ∈ (0...𝑥) ↦ (((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = 0 ) | 
| 139 | 18, 19, 105, 138 | ifbothda 4564 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦))))) = if(𝐷 ≤ 𝑥, (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶), 0 )) | 
| 140 | 139 | mpteq2dva 5242 | . 2
⊢ (𝜑 → (𝑥 ∈ ℕ0 ↦ (𝑅 Σg
(𝑦 ∈ (0...𝑥) ↦
(((coe1‘𝐴)‘𝑦) ×
((coe1‘(𝐶
·
(𝐷 ↑ 𝑋)))‘(𝑥 − 𝑦)))))) = (𝑥 ∈ ℕ0 ↦ if(𝐷 ≤ 𝑥, (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶), 0 ))) | 
| 141 | 17, 140 | eqtrd 2777 | 1
⊢ (𝜑 →
(coe1‘(𝐴
∙
(𝐶 · (𝐷 ↑ 𝑋)))) = (𝑥 ∈ ℕ0 ↦ if(𝐷 ≤ 𝑥, (((coe1‘𝐴)‘(𝑥 − 𝐷)) × 𝐶), 0 ))) |