Proof of Theorem dvmptfprodlem
| Step | Hyp | Ref
| Expression |
| 1 | | dvmptfprodlem.xph |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 2 | | dvmptfprodlem.iph |
. . . . . . 7
⊢
Ⅎ𝑖𝜑 |
| 3 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑖𝑥 |
| 4 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑖𝑋 |
| 5 | 3, 4 | nfel 2920 |
. . . . . . 7
⊢
Ⅎ𝑖 𝑥 ∈ 𝑋 |
| 6 | 2, 5 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑖(𝜑 ∧ 𝑥 ∈ 𝑋) |
| 7 | | dvmptfprodlem.if |
. . . . . . 7
⊢
Ⅎ𝑖𝐹 |
| 8 | 7 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Ⅎ𝑖𝐹) |
| 9 | | dvmptfprodlem.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ Fin) |
| 10 | | snfi 9083 |
. . . . . . . . 9
⊢ {𝐸} ∈ Fin |
| 11 | 10 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → {𝐸} ∈ Fin) |
| 12 | | unfi 9211 |
. . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧ {𝐸} ∈ Fin) → (𝐷 ∪ {𝐸}) ∈ Fin) |
| 13 | 9, 11, 12 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐷 ∪ {𝐸}) ∈ Fin) |
| 14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐷 ∪ {𝐸}) ∈ Fin) |
| 15 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ (𝐷 ∪ {𝐸})) → 𝜑) |
| 16 | | dvmptfprodlem.ss |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 ∪ {𝐸}) ⊆ 𝐼) |
| 17 | 16 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐷 ∪ {𝐸})) → 𝑖 ∈ 𝐼) |
| 18 | 17 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ (𝐷 ∪ {𝐸})) → 𝑖 ∈ 𝐼) |
| 19 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ (𝐷 ∪ {𝐸})) → 𝑥 ∈ 𝑋) |
| 20 | | dvmptfprodlem.a |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) |
| 21 | 15, 18, 19, 20 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ (𝐷 ∪ {𝐸})) → 𝐴 ∈ ℂ) |
| 22 | | dvmptfprodlem.e |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ V) |
| 23 | | snidg 4660 |
. . . . . . . . 9
⊢ (𝐸 ∈ V → 𝐸 ∈ {𝐸}) |
| 24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ {𝐸}) |
| 25 | | elun2 4183 |
. . . . . . . 8
⊢ (𝐸 ∈ {𝐸} → 𝐸 ∈ (𝐷 ∪ {𝐸})) |
| 26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ (𝐷 ∪ {𝐸})) |
| 27 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐸 ∈ (𝐷 ∪ {𝐸})) |
| 28 | | dvmptfprodlem.f |
. . . . . . 7
⊢ (𝑖 = 𝐸 → 𝐴 = 𝐹) |
| 29 | 28 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 = 𝐸) → 𝐴 = 𝐹) |
| 30 | 6, 8, 14, 21, 27, 29 | fprodsplit1f 16026 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∏𝑖 ∈ (𝐷 ∪ {𝐸})𝐴 = (𝐹 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴)) |
| 31 | | difundir 4291 |
. . . . . . . . . 10
⊢ ((𝐷 ∪ {𝐸}) ∖ {𝐸}) = ((𝐷 ∖ {𝐸}) ∪ ({𝐸} ∖ {𝐸})) |
| 32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐷 ∪ {𝐸}) ∖ {𝐸}) = ((𝐷 ∖ {𝐸}) ∪ ({𝐸} ∖ {𝐸}))) |
| 33 | | dvmptfprodlem.db |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝐸 ∈ 𝐷) |
| 34 | | difsn 4798 |
. . . . . . . . . . 11
⊢ (¬
𝐸 ∈ 𝐷 → (𝐷 ∖ {𝐸}) = 𝐷) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ∖ {𝐸}) = 𝐷) |
| 36 | | difid 4376 |
. . . . . . . . . . 11
⊢ ({𝐸} ∖ {𝐸}) = ∅ |
| 37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ({𝐸} ∖ {𝐸}) = ∅) |
| 38 | 35, 37 | uneq12d 4169 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐷 ∖ {𝐸}) ∪ ({𝐸} ∖ {𝐸})) = (𝐷 ∪ ∅)) |
| 39 | | un0 4394 |
. . . . . . . . . 10
⊢ (𝐷 ∪ ∅) = 𝐷 |
| 40 | 39 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 ∪ ∅) = 𝐷) |
| 41 | 32, 38, 40 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → ((𝐷 ∪ {𝐸}) ∖ {𝐸}) = 𝐷) |
| 42 | 41 | prodeq1d 15956 |
. . . . . . 7
⊢ (𝜑 → ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴 = ∏𝑖 ∈ 𝐷 𝐴) |
| 43 | 42 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝐹 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) = (𝐹 · ∏𝑖 ∈ 𝐷 𝐴)) |
| 44 | 43 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) = (𝐹 · ∏𝑖 ∈ 𝐷 𝐴)) |
| 45 | 30, 44 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∏𝑖 ∈ (𝐷 ∪ {𝐸})𝐴 = (𝐹 · ∏𝑖 ∈ 𝐷 𝐴)) |
| 46 | 1, 45 | mpteq2da 5240 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑖 ∈ (𝐷 ∪ {𝐸})𝐴) = (𝑥 ∈ 𝑋 ↦ (𝐹 · ∏𝑖 ∈ 𝐷 𝐴))) |
| 47 | 46 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ ∏𝑖 ∈ (𝐷 ∪ {𝐸})𝐴)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐹 · ∏𝑖 ∈ 𝐷 𝐴)))) |
| 48 | | dvmptfprodlem.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
| 49 | 16, 26 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ 𝐼) |
| 50 | 49 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐸 ∈ 𝐼) |
| 51 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝜑) |
| 52 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 53 | 51, 50, 52 | 3jca 1129 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) |
| 54 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑖𝐸 |
| 55 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑖 𝐸 ∈ 𝐼 |
| 56 | 2, 55, 5 | nf3an 1901 |
. . . . . 6
⊢
Ⅎ𝑖(𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) |
| 57 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑖ℂ |
| 58 | 7, 57 | nfel 2920 |
. . . . . 6
⊢
Ⅎ𝑖 𝐹 ∈ ℂ |
| 59 | 56, 58 | nfim 1896 |
. . . . 5
⊢
Ⅎ𝑖((𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ) |
| 60 | | ancom 460 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 = 𝐸) ↔ (𝑖 = 𝐸 ∧ (𝜑 ∧ 𝑥 ∈ 𝑋))) |
| 61 | 60 | imbi1i 349 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 = 𝐸) → 𝐴 = 𝐹) ↔ ((𝑖 = 𝐸 ∧ (𝜑 ∧ 𝑥 ∈ 𝑋)) → 𝐴 = 𝐹)) |
| 62 | | eqcom 2744 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 𝐹 ↔ 𝐹 = 𝐴) |
| 63 | 62 | imbi2i 336 |
. . . . . . . . . . . 12
⊢ (((𝑖 = 𝐸 ∧ (𝜑 ∧ 𝑥 ∈ 𝑋)) → 𝐴 = 𝐹) ↔ ((𝑖 = 𝐸 ∧ (𝜑 ∧ 𝑥 ∈ 𝑋)) → 𝐹 = 𝐴)) |
| 64 | 61, 63 | bitri 275 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 = 𝐸) → 𝐴 = 𝐹) ↔ ((𝑖 = 𝐸 ∧ (𝜑 ∧ 𝑥 ∈ 𝑋)) → 𝐹 = 𝐴)) |
| 65 | 29, 64 | mpbi 230 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝐸 ∧ (𝜑 ∧ 𝑥 ∈ 𝑋)) → 𝐹 = 𝐴) |
| 66 | 65 | 3adantr2 1171 |
. . . . . . . . 9
⊢ ((𝑖 = 𝐸 ∧ (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) → 𝐹 = 𝐴) |
| 67 | 66 | 3adant2 1132 |
. . . . . . . 8
⊢ ((𝑖 = 𝐸 ∧ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) ∧ (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) → 𝐹 = 𝐴) |
| 68 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝑖 = 𝐸 ∧ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) ∧ (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) → (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) |
| 69 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝐸 → (𝑖 ∈ 𝐼 ↔ 𝐸 ∈ 𝐼)) |
| 70 | 69 | 3anbi2d 1443 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐸 → ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) ↔ (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋))) |
| 71 | 70 | imbi1d 341 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐸 → (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) ↔ ((𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ))) |
| 72 | 71 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝐸 ∧ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)) → ((𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)) |
| 73 | 72 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑖 = 𝐸 ∧ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) ∧ (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) → ((𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ)) |
| 74 | 68, 73 | mpd 15 |
. . . . . . . 8
⊢ ((𝑖 = 𝐸 ∧ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) ∧ (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) → 𝐴 ∈ ℂ) |
| 75 | 67, 74 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑖 = 𝐸 ∧ ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) ∧ (𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋)) → 𝐹 ∈ ℂ) |
| 76 | 75 | 3exp 1120 |
. . . . . 6
⊢ (𝑖 = 𝐸 → (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) → ((𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ))) |
| 77 | 20 | 2a1i 12 |
. . . . . 6
⊢ (𝑖 = 𝐸 → (((𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ) → ((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ))) |
| 78 | 76, 77 | impbid 212 |
. . . . 5
⊢ (𝑖 = 𝐸 → (((𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) ↔ ((𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ))) |
| 79 | 54, 59, 78, 20 | vtoclgf 3569 |
. . . 4
⊢ (𝐸 ∈ 𝐼 → ((𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ)) |
| 80 | 50, 53, 79 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ℂ) |
| 81 | | dvmptfprodlem.14 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐺 ∈ ℂ) |
| 82 | | dvmptfprodlem.dvf |
. . 3
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐹)) = (𝑥 ∈ 𝑋 ↦ 𝐺)) |
| 83 | 51, 9 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ Fin) |
| 84 | 51 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ 𝐷) → 𝜑) |
| 85 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐷) → (𝐷 ∪ {𝐸}) ⊆ 𝐼) |
| 86 | | elun1 4182 |
. . . . . . . 8
⊢ (𝑖 ∈ 𝐷 → 𝑖 ∈ (𝐷 ∪ {𝐸})) |
| 87 | 86 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐷) → 𝑖 ∈ (𝐷 ∪ {𝐸})) |
| 88 | 85, 87 | sseldd 3984 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐷) → 𝑖 ∈ 𝐼) |
| 89 | 88 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ 𝐷) → 𝑖 ∈ 𝐼) |
| 90 | 52 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ 𝐷) → 𝑥 ∈ 𝑋) |
| 91 | 84, 89, 90, 20 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ 𝐷) → 𝐴 ∈ ℂ) |
| 92 | 6, 83, 91 | fprodclf 16028 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∏𝑖 ∈ 𝐷 𝐴 ∈ ℂ) |
| 93 | | dvmptfprodlem.jph |
. . . . 5
⊢
Ⅎ𝑗𝜑 |
| 94 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑗 𝑥 ∈ 𝑋 |
| 95 | 93, 94 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑗(𝜑 ∧ 𝑥 ∈ 𝑋) |
| 96 | | dvmptfprodlem.c |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → 𝐶 ∈ ℂ) |
| 97 | | diffi 9215 |
. . . . . . . . 9
⊢ (𝐷 ∈ Fin → (𝐷 ∖ {𝑗}) ∈ Fin) |
| 98 | 9, 97 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 ∖ {𝑗}) ∈ Fin) |
| 99 | 98 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐷 ∖ {𝑗}) ∈ Fin) |
| 100 | | eldifi 4131 |
. . . . . . . . 9
⊢ (𝑖 ∈ (𝐷 ∖ {𝑗}) → 𝑖 ∈ 𝐷) |
| 101 | 100 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ (𝐷 ∖ {𝑗})) → 𝑖 ∈ 𝐷) |
| 102 | 101, 91 | syldan 591 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ (𝐷 ∖ {𝑗})) → 𝐴 ∈ ℂ) |
| 103 | 6, 99, 102 | fprodclf 16028 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 ∈ ℂ) |
| 104 | 103 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 ∈ ℂ) |
| 105 | 96, 104 | mulcld 11281 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) ∈ ℂ) |
| 106 | 95, 83, 105 | fsumclf 15774 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) ∈ ℂ) |
| 107 | | dvmptfprodlem.dvp |
. . 3
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ ∏𝑖 ∈ 𝐷 𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴))) |
| 108 | 1, 48, 80, 81, 82, 92, 106, 107 | dvmptmulf 45952 |
. 2
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (𝐹 · ∏𝑖 ∈ 𝐷 𝐴))) = (𝑥 ∈ 𝑋 ↦ ((𝐺 · ∏𝑖 ∈ 𝐷 𝐴) + (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)))) |
| 109 | | dvmptfprodlem.jg |
. . . . . 6
⊢
Ⅎ𝑗𝐺 |
| 110 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑗
· |
| 111 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑗∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴 |
| 112 | 109, 110,
111 | nfov 7461 |
. . . . 5
⊢
Ⅎ𝑗(𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) |
| 113 | 51, 22 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐸 ∈ V) |
| 114 | 51, 33 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ¬ 𝐸 ∈ 𝐷) |
| 115 | | diffi 9215 |
. . . . . . . . . 10
⊢ ((𝐷 ∪ {𝐸}) ∈ Fin → ((𝐷 ∪ {𝐸}) ∖ {𝑗}) ∈ Fin) |
| 116 | 13, 115 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐷 ∪ {𝐸}) ∖ {𝑗}) ∈ Fin) |
| 117 | 116 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐷 ∪ {𝐸}) ∖ {𝑗}) ∈ Fin) |
| 118 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗}) → 𝑖 ∈ (𝐷 ∪ {𝐸})) |
| 119 | 118 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})) → 𝑖 ∈ (𝐷 ∪ {𝐸})) |
| 120 | 119, 21 | syldan 591 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})) → 𝐴 ∈ ℂ) |
| 121 | 6, 117, 120 | fprodclf 16028 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴 ∈ ℂ) |
| 122 | 121 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴 ∈ ℂ) |
| 123 | 96, 122 | mulcld 11281 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) ∈ ℂ) |
| 124 | | dvmptfprodlem.cg |
. . . . . 6
⊢ (𝑗 = 𝐸 → 𝐶 = 𝐺) |
| 125 | | sneq 4636 |
. . . . . . . 8
⊢ (𝑗 = 𝐸 → {𝑗} = {𝐸}) |
| 126 | 125 | difeq2d 4126 |
. . . . . . 7
⊢ (𝑗 = 𝐸 → ((𝐷 ∪ {𝐸}) ∖ {𝑗}) = ((𝐷 ∪ {𝐸}) ∖ {𝐸})) |
| 127 | 126 | prodeq1d 15956 |
. . . . . 6
⊢ (𝑗 = 𝐸 → ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴 = ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) |
| 128 | 124, 127 | oveq12d 7449 |
. . . . 5
⊢ (𝑗 = 𝐸 → (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) = (𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴)) |
| 129 | 41, 9 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝜑 → ((𝐷 ∪ {𝐸}) ∖ {𝐸}) ∈ Fin) |
| 130 | 129 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐷 ∪ {𝐸}) ∖ {𝐸}) ∈ Fin) |
| 131 | 51 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})) → 𝜑) |
| 132 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})) → (𝐷 ∪ {𝐸}) ⊆ 𝐼) |
| 133 | | eldifi 4131 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸}) → 𝑖 ∈ (𝐷 ∪ {𝐸})) |
| 134 | 133 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})) → 𝑖 ∈ (𝐷 ∪ {𝐸})) |
| 135 | 132, 134 | sseldd 3984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})) → 𝑖 ∈ 𝐼) |
| 136 | 135 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})) → 𝑖 ∈ 𝐼) |
| 137 | 52 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})) → 𝑥 ∈ 𝑋) |
| 138 | 131, 136,
137, 20 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})) → 𝐴 ∈ ℂ) |
| 139 | 6, 130, 138 | fprodclf 16028 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴 ∈ ℂ) |
| 140 | 81, 139 | mulcld 11281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) ∈ ℂ) |
| 141 | 95, 112, 83, 113, 114, 123, 128, 140 | fsumsplitsn 15780 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑗 ∈ (𝐷 ∪ {𝐸})(𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) = (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) + (𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴))) |
| 142 | | difundir 4291 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∪ {𝐸}) ∖ {𝑗}) = ((𝐷 ∖ {𝑗}) ∪ ({𝐸} ∖ {𝑗})) |
| 143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → ((𝐷 ∪ {𝐸}) ∖ {𝑗}) = ((𝐷 ∖ {𝑗}) ∪ ({𝐸} ∖ {𝑗}))) |
| 144 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥 𝑗 ∈ 𝐷 |
| 145 | 1, 144 | nfan 1899 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝜑 ∧ 𝑗 ∈ 𝐷) |
| 146 | | elsni 4643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ {𝐸} → 𝑥 = 𝐸) |
| 147 | 146 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ {𝐸} → 𝐸 = 𝑥) |
| 148 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ {𝐸} ∧ 𝑥 = 𝑗) → 𝐸 = 𝑥) |
| 149 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ {𝐸} ∧ 𝑥 = 𝑗) → 𝑥 = 𝑗) |
| 150 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ {𝐸} ∧ 𝑥 = 𝑗) → 𝑗 = 𝑗) |
| 151 | 148, 149,
150 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ {𝐸} ∧ 𝑥 = 𝑗) → 𝐸 = 𝑗) |
| 152 | 151 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐷) ∧ 𝑥 ∈ {𝐸}) ∧ 𝑥 = 𝑗) → 𝐸 = 𝑗) |
| 153 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐷) ∧ 𝑥 ∈ {𝐸}) ∧ 𝑥 = 𝑗) → 𝑗 ∈ 𝐷) |
| 154 | 152, 153 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐷) ∧ 𝑥 ∈ {𝐸}) ∧ 𝑥 = 𝑗) → 𝐸 ∈ 𝐷) |
| 155 | 33 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐷) ∧ 𝑥 ∈ {𝐸}) ∧ 𝑥 = 𝑗) → ¬ 𝐸 ∈ 𝐷) |
| 156 | 154, 155 | pm2.65da 817 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐷) ∧ 𝑥 ∈ {𝐸}) → ¬ 𝑥 = 𝑗) |
| 157 | | velsn 4642 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ {𝑗} ↔ 𝑥 = 𝑗) |
| 158 | 156, 157 | sylnibr 329 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐷) ∧ 𝑥 ∈ {𝐸}) → ¬ 𝑥 ∈ {𝑗}) |
| 159 | 158 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝑥 ∈ {𝐸} → ¬ 𝑥 ∈ {𝑗})) |
| 160 | 145, 159 | ralrimi 3257 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → ∀𝑥 ∈ {𝐸} ¬ 𝑥 ∈ {𝑗}) |
| 161 | | disj 4450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (({𝐸} ∩ {𝑗}) = ∅ ↔ ∀𝑥 ∈ {𝐸} ¬ 𝑥 ∈ {𝑗}) |
| 162 | 160, 161 | sylibr 234 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → ({𝐸} ∩ {𝑗}) = ∅) |
| 163 | | disjdif2 4480 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝐸} ∩ {𝑗}) = ∅ → ({𝐸} ∖ {𝑗}) = {𝐸}) |
| 164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → ({𝐸} ∖ {𝑗}) = {𝐸}) |
| 165 | 164 | uneq2d 4168 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → ((𝐷 ∖ {𝑗}) ∪ ({𝐸} ∖ {𝑗})) = ((𝐷 ∖ {𝑗}) ∪ {𝐸})) |
| 166 | 143, 165 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → ((𝐷 ∪ {𝐸}) ∖ {𝑗}) = ((𝐷 ∖ {𝑗}) ∪ {𝐸})) |
| 167 | 166 | prodeq1d 15956 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴 = ∏𝑖 ∈ ((𝐷 ∖ {𝑗}) ∪ {𝐸})𝐴) |
| 168 | 167 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴 = ∏𝑖 ∈ ((𝐷 ∖ {𝑗}) ∪ {𝐸})𝐴) |
| 169 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖 𝑗 ∈ 𝐷 |
| 170 | 6, 169 | nfan 1899 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) |
| 171 | 99 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → (𝐷 ∖ {𝑗}) ∈ Fin) |
| 172 | 51 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → 𝜑) |
| 173 | 172, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → 𝐸 ∈ V) |
| 174 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝐸 ∈ 𝐷 → ¬ 𝐸 ∈ 𝐷) |
| 175 | 174 | intnanrd 489 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝐸 ∈ 𝐷 → ¬ (𝐸 ∈ 𝐷 ∧ ¬ 𝐸 ∈ {𝑗})) |
| 176 | 174, 175 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝐸 ∈ 𝐷 → ¬ (𝐸 ∈ 𝐷 ∧ ¬ 𝐸 ∈ {𝑗})) |
| 177 | | eldif 3961 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸 ∈ (𝐷 ∖ {𝑗}) ↔ (𝐸 ∈ 𝐷 ∧ ¬ 𝐸 ∈ {𝑗})) |
| 178 | 176, 177 | sylnibr 329 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝐸 ∈ 𝐷 → ¬ 𝐸 ∈ (𝐷 ∖ {𝑗})) |
| 179 | 33, 178 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ 𝐸 ∈ (𝐷 ∖ {𝑗})) |
| 180 | 172, 179 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → ¬ 𝐸 ∈ (𝐷 ∖ {𝑗})) |
| 181 | 102 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) ∧ 𝑖 ∈ (𝐷 ∖ {𝑗})) → 𝐴 ∈ ℂ) |
| 182 | 80 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → 𝐹 ∈ ℂ) |
| 183 | 170, 7, 171, 173, 180, 181, 28, 182 | fprodsplitsn 16025 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → ∏𝑖 ∈ ((𝐷 ∖ {𝑗}) ∪ {𝐸})𝐴 = (∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 · 𝐹)) |
| 184 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → (∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 · 𝐹) = (∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 · 𝐹)) |
| 185 | 168, 183,
184 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴 = (∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 · 𝐹)) |
| 186 | 185 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) = (𝐶 · (∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 · 𝐹))) |
| 187 | 96, 104, 182 | mulassd 11284 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → ((𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹) = (𝐶 · (∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 · 𝐹))) |
| 188 | 187 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → (𝐶 · (∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴 · 𝐹)) = ((𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) |
| 189 | 186, 188 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑗 ∈ 𝐷) → (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) = ((𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) |
| 190 | 189 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑗 ∈ 𝐷 → (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) = ((𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹))) |
| 191 | 95, 190 | ralrimi 3257 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) = ((𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) |
| 192 | 191 | sumeq2d 15737 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) = Σ𝑗 ∈ 𝐷 ((𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) |
| 193 | 95, 83, 80, 105 | fsummulc1f 45586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹) = Σ𝑗 ∈ 𝐷 ((𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) |
| 194 | 193 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑗 ∈ 𝐷 ((𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹) = (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) |
| 195 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹) = (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) |
| 196 | 192, 194,
195 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) = (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) |
| 197 | 106, 80 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹) ∈ ℂ) |
| 198 | 196, 197 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) ∈ ℂ) |
| 199 | 198, 140 | addcomd 11463 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴) + (𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴)) = ((𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) + Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴))) |
| 200 | 42 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) = (𝐺 · ∏𝑖 ∈ 𝐷 𝐴)) |
| 201 | 200 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) = (𝐺 · ∏𝑖 ∈ 𝐷 𝐴)) |
| 202 | 201, 196 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐺 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝐸})𝐴) + Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴)) = ((𝐺 · ∏𝑖 ∈ 𝐷 𝐴) + (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹))) |
| 203 | 141, 199,
202 | 3eqtrrd 2782 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐺 · ∏𝑖 ∈ 𝐷 𝐴) + (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹)) = Σ𝑗 ∈ (𝐷 ∪ {𝐸})(𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴)) |
| 204 | 1, 203 | mpteq2da 5240 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐺 · ∏𝑖 ∈ 𝐷 𝐴) + (Σ𝑗 ∈ 𝐷 (𝐶 · ∏𝑖 ∈ (𝐷 ∖ {𝑗})𝐴) · 𝐹))) = (𝑥 ∈ 𝑋 ↦ Σ𝑗 ∈ (𝐷 ∪ {𝐸})(𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴))) |
| 205 | 47, 108, 204 | 3eqtrd 2781 |
1
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ ∏𝑖 ∈ (𝐷 ∪ {𝐸})𝐴)) = (𝑥 ∈ 𝑋 ↦ Σ𝑗 ∈ (𝐷 ∪ {𝐸})(𝐶 · ∏𝑖 ∈ ((𝐷 ∪ {𝐸}) ∖ {𝑗})𝐴))) |