| Step | Hyp | Ref
| Expression |
| 1 | | gsumfs2d.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑊) |
| 2 | | gsumfs2d.1 |
. . . . 5
⊢ 0 =
(0g‘𝑊) |
| 3 | | gsumfs2d.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ CMnd) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → 𝑊 ∈ CMnd) |
| 5 | | gsumfs2d.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
| 6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → 𝐴 ∈ 𝑋) |
| 7 | 6 | imaexd 7938 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐴 “ {𝑥}) ∈ V) |
| 8 | | gsumfs2d.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 9 | 8 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
| 10 | 9 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝐹 Fn 𝐴) |
| 11 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝐴 ∈ 𝑋) |
| 12 | 2 | fvexi 6920 |
. . . . . . 7
⊢ 0 ∈
V |
| 13 | 12 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 0 ∈ V) |
| 14 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) |
| 15 | 14 | eldifad 3963 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ (𝐴 “ {𝑥})) |
| 16 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 17 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 18 | 16, 17 | elimasn 6108 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↔ 〈𝑥, 𝑦〉 ∈ 𝐴) |
| 19 | 18 | biimpi 216 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐴 “ {𝑥}) → 〈𝑥, 𝑦〉 ∈ 𝐴) |
| 20 | 15, 19 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 〈𝑥, 𝑦〉 ∈ 𝐴) |
| 21 | 14 | eldifbd 3964 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) |
| 22 | 16, 17 | elimasn 6108 |
. . . . . . . . 9
⊢ (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↔ 〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 )) |
| 23 | 22 | biimpri 228 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 ) → 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) |
| 24 | 21, 23 | nsyl 140 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ 〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 )) |
| 25 | 20, 24 | eldifd 3962 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 〈𝑥, 𝑦〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
| 26 | 10, 11, 13, 25 | fvdifsupp 8196 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → (𝐹‘〈𝑥, 𝑦〉) = 0 ) |
| 27 | | gsumfs2d.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 finSupp 0 ) |
| 28 | 27 | fsuppimpd 9409 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ∈
Fin) |
| 30 | | imafi2 32723 |
. . . . . 6
⊢ ((𝐹 supp 0 ) ∈ Fin →
((𝐹 supp 0 ) “ {𝑥}) ∈ Fin) |
| 31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → ((𝐹 supp 0 ) “ {𝑥}) ∈ Fin) |
| 32 | 8 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹:𝐴⟶𝐵) |
| 33 | 19 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 〈𝑥, 𝑦〉 ∈ 𝐴) |
| 34 | 32, 33 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐵) |
| 35 | | suppssdm 8202 |
. . . . . . . 8
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
| 36 | 35, 8 | fssdm 6755 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
| 37 | 36 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ⊆ 𝐴) |
| 38 | | imass1 6119 |
. . . . . 6
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → ((𝐹 supp 0 ) “ {𝑥}) ⊆ (𝐴 “ {𝑥})) |
| 39 | 37, 38 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → ((𝐹 supp 0 ) “ {𝑥}) ⊆ (𝐴 “ {𝑥})) |
| 40 | 1, 2, 4, 7, 26, 31, 34, 39 | gsummptres2 33056 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))) = (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
| 41 | 40 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))) = (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))))) |
| 42 | 41 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |
| 43 | 5 | dmexd 7925 |
. . 3
⊢ (𝜑 → dom 𝐴 ∈ V) |
| 44 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹 Fn 𝐴) |
| 45 | 5 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐴 ∈ 𝑋) |
| 46 | 12 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 0 ∈ V) |
| 47 | 19 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 〈𝑥, 𝑦〉 ∈ 𝐴) |
| 48 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) |
| 49 | 48 | eldifbd 3964 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ 𝑥 ∈ dom (𝐹 supp 0 )) |
| 50 | 16, 17 | opeldm 5918 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 ) → 𝑥 ∈ dom (𝐹 supp 0 )) |
| 51 | 49, 50 | nsyl 140 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ 〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 )) |
| 52 | 47, 51 | eldifd 3962 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 〈𝑥, 𝑦〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
| 53 | 44, 45, 46, 52 | fvdifsupp 8196 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘〈𝑥, 𝑦〉) = 0 ) |
| 54 | 53 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) |
| 55 | 54 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))) = (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 ))) |
| 56 | 3 | cmnmndd 19822 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Mnd) |
| 57 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → 𝐴 ∈ 𝑋) |
| 58 | 57 | imaexd 7938 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝐴 “ {𝑥}) ∈ V) |
| 59 | 2 | gsumz 18849 |
. . . . 5
⊢ ((𝑊 ∈ Mnd ∧ (𝐴 “ {𝑥}) ∈ V) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 ) |
| 60 | 56, 58, 59 | syl2an2r 685 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 ) |
| 61 | 55, 60 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))) = 0 ) |
| 62 | | dmfi 9375 |
. . . 4
⊢ ((𝐹 supp 0 ) ∈ Fin → dom
(𝐹 supp 0 ) ∈
Fin) |
| 63 | 28, 62 | syl 17 |
. . 3
⊢ (𝜑 → dom (𝐹 supp 0 ) ∈
Fin) |
| 64 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 𝑊 ∈ CMnd) |
| 65 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 𝐴 ∈ 𝑋) |
| 66 | 65 | imaexd 7938 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝐴 “ {𝑥}) ∈ V) |
| 67 | 8 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 𝐹:𝐴⟶𝐵) |
| 68 | 19 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 〈𝑥, 𝑦〉 ∈ 𝐴) |
| 69 | 67, 68 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐵) |
| 70 | 69 | fmpttd 7135 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)):(𝐴 “ {𝑥})⟶𝐵) |
| 71 | 66 | mptexd 7244 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ V) |
| 72 | 70 | ffnd 6737 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)) Fn (𝐴 “ {𝑥})) |
| 73 | 12 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → 0 ∈ V) |
| 74 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝐹 supp 0 ) ∈
Fin) |
| 75 | 74, 30 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → ((𝐹 supp 0 ) “ {𝑥}) ∈ Fin) |
| 76 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)) |
| 77 | | simp-4l 783 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝜑) |
| 78 | | simp-4r 784 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑥 ∈ dom 𝐴) |
| 79 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡) |
| 80 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑡 ∈ (𝐴 “ {𝑥})) |
| 81 | 79, 80 | eqeltrd 2841 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑦 ∈ (𝐴 “ {𝑥})) |
| 82 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) |
| 83 | 79, 82 | eqneltrd 2861 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) |
| 84 | 9 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝐹 Fn 𝐴) |
| 85 | 5 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝐴 ∈ 𝑋) |
| 86 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 0 ∈ V) |
| 87 | 68 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 〈𝑥, 𝑦〉 ∈ 𝐴) |
| 88 | 23 | con3i 154 |
. . . . . . . . . . . 12
⊢ (¬
𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) → ¬ 〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 )) |
| 89 | 88 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ¬ 〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 )) |
| 90 | 87, 89 | eldifd 3962 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 〈𝑥, 𝑦〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
| 91 | 84, 85, 86, 90 | fvdifsupp 8196 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → (𝐹‘〈𝑥, 𝑦〉) = 0 ) |
| 92 | 77, 78, 81, 83, 91 | syl1111anc 841 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → (𝐹‘〈𝑥, 𝑦〉) = 0 ) |
| 93 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 𝑡 ∈ (𝐴 “ {𝑥})) |
| 94 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 0 ∈ V) |
| 95 | 76, 92, 93, 94 | fvmptd2 7024 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))‘𝑡) = 0 ) |
| 96 | 95 | ex 412 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) → (¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}) → ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))‘𝑡) = 0 )) |
| 97 | 96 | orrd 864 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) → (𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}) ∨ ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))‘𝑡) = 0 )) |
| 98 | 71, 72, 73, 75, 97 | finnzfsuppd 9413 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)) finSupp 0 ) |
| 99 | 1, 2, 64, 66, 70, 98 | gsumcl 19933 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))) ∈ 𝐵) |
| 100 | | dmss 5913 |
. . . 4
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → dom (𝐹 supp 0 ) ⊆ dom 𝐴) |
| 101 | 36, 100 | syl 17 |
. . 3
⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ dom 𝐴) |
| 102 | 1, 2, 3, 43, 61, 63, 99, 101 | gsummptres2 33056 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |
| 103 | 8, 36 | feqresmpt 6978 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) = (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))) |
| 104 | 103 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧)))) |
| 105 | | ssidd 4007 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
| 106 | 1, 2, 3, 5, 8, 105, 27 | gsumres 19931 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg 𝐹)) |
| 107 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦(𝐹‘𝑧) |
| 108 | | gsumfs2d.p |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 109 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘𝑧) = (𝐹‘〈𝑥, 𝑦〉)) |
| 110 | | gsumfs2d.r |
. . . . 5
⊢ (𝜑 → Rel 𝐴) |
| 111 | | relss 5791 |
. . . . 5
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → (Rel 𝐴 → Rel (𝐹 supp 0 ))) |
| 112 | 36, 110, 111 | sylc 65 |
. . . 4
⊢ (𝜑 → Rel (𝐹 supp 0 )) |
| 113 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝐹:𝐴⟶𝐵) |
| 114 | 36 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝑧 ∈ 𝐴) |
| 115 | 113, 114 | ffvelcdmd 7105 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → (𝐹‘𝑧) ∈ 𝐵) |
| 116 | 107, 108,
1, 109, 112, 28, 3, 115 | gsummpt2d 33052 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |
| 117 | 104, 106,
116 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |
| 118 | 42, 102, 117 | 3eqtr4rd 2788 |
1
⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |