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 3974 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 𝑦 ∈ (𝐴 “ {𝑥})) |
16 | | vex 3481 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
17 | | vex 3481 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
18 | 16, 17 | elimasn 6109 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐴 “ {𝑥}) ↔ 〈𝑥, 𝑦〉 ∈ 𝐴) |
19 | 18 | biimpi 216 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐴 “ {𝑥}) → 〈𝑥, 𝑦〉 ∈ 𝐴) |
20 | 15, 19 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 〈𝑥, 𝑦〉 ∈ 𝐴) |
21 | 14 | eldifbd 3975 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) |
22 | 16, 17 | elimasn 6109 |
. . . . . . . . 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 3973 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → 〈𝑥, 𝑦〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
26 | 10, 11, 13, 25 | fvdifsupp 8194 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ ((𝐴 “ {𝑥}) ∖ ((𝐹 supp 0 ) “ {𝑥}))) → (𝐹‘〈𝑥, 𝑦〉) = 0 ) |
27 | | gsumfs2d.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 finSupp 0 ) |
28 | 27 | fsuppimpd 9406 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ∈
Fin) |
30 | | imafi2 32728 |
. . . . . 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 7104 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐵) |
35 | | suppssdm 8200 |
. . . . . . . 8
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
36 | 35, 8 | fssdm 6755 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
37 | 36 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝐹 supp 0 ) ⊆ 𝐴) |
38 | | imass1 6121 |
. . . . . 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 33038 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 supp 0 )) → (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))) = (𝑊 Σg (𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
41 | 40 | mpteq2dva 5247 |
. . 3
⊢ (𝜑 → (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))) = (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))))) |
42 | 41 | oveq2d 7446 |
. 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 3975 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ 𝑥 ∈ dom (𝐹 supp 0 )) |
50 | 16, 17 | opeldm 5920 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 ) → 𝑥 ∈ dom (𝐹 supp 0 )) |
51 | 49, 50 | nsyl 140 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → ¬ 〈𝑥, 𝑦〉 ∈ (𝐹 supp 0 )) |
52 | 47, 51 | eldifd 3973 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → 〈𝑥, 𝑦〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
53 | 44, 45, 46, 52 | fvdifsupp 8194 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘〈𝑥, 𝑦〉) = 0 ) |
54 | 53 | mpteq2dva 5247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)) = (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) |
55 | 54 | oveq2d 7446 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))) = (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 ))) |
56 | 3 | cmnmndd 19836 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Mnd) |
57 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → 𝐴 ∈ 𝑋) |
58 | 57 | imaexd 7938 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝐴 “ {𝑥}) ∈ V) |
59 | 2 | gsumz 18861 |
. . . . 5
⊢ ((𝑊 ∈ Mnd ∧ (𝐴 “ {𝑥}) ∈ V) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 ) |
60 | 56, 58, 59 | syl2an2r 685 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ 0 )) = 0 ) |
61 | 55, 60 | eqtrd 2774 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐴 ∖ dom (𝐹 supp 0 ))) → (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))) = 0 ) |
62 | | dmfi 9372 |
. . . 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 7104 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐵) |
70 | 69 | fmpttd 7134 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)):(𝐴 “ {𝑥})⟶𝐵) |
71 | 66 | mptexd 7243 |
. . . . 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 2734 |
. . . . . . . 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 2838 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → 𝑦 ∈ (𝐴 “ {𝑥})) |
82 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) ∧ 𝑦 = 𝑡) → ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) |
83 | 79, 82 | eqneltrd 2858 |
. . . . . . . . 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 3973 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → 〈𝑥, 𝑦〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
91 | 84, 85, 86, 90 | fvdifsupp 8194 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑦 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥})) → (𝐹‘〈𝑥, 𝑦〉) = 0 ) |
92 | 77, 78, 81, 83, 91 | syl1111anc 840 |
. . . . . . . 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 7023 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) ∧ ¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥})) → ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))‘𝑡) = 0 ) |
96 | 95 | ex 412 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) → (¬ 𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}) → ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))‘𝑡) = 0 )) |
97 | 96 | orrd 863 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐴) ∧ 𝑡 ∈ (𝐴 “ {𝑥})) → (𝑡 ∈ ((𝐹 supp 0 ) “ {𝑥}) ∨ ((𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))‘𝑡) = 0 )) |
98 | 71, 72, 73, 75, 97 | finnzfsuppd 9410 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)) finSupp 0 ) |
99 | 1, 2, 64, 66, 70, 98 | gsumcl 19947 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐴) → (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))) ∈ 𝐵) |
100 | | dmss 5915 |
. . . 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 33038 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉))))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |
103 | 8, 36 | feqresmpt 6977 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) = (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))) |
104 | 103 | oveq2d 7446 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧)))) |
105 | | ssidd 4018 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
106 | 1, 2, 3, 5, 8, 105, 27 | gsumres 19945 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝑊 Σg 𝐹)) |
107 | | nfcv 2902 |
. . . 4
⊢
Ⅎ𝑦(𝐹‘𝑧) |
108 | | gsumfs2d.p |
. . . 4
⊢
Ⅎ𝑥𝜑 |
109 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘𝑧) = (𝐹‘〈𝑥, 𝑦〉)) |
110 | | gsumfs2d.r |
. . . . 5
⊢ (𝜑 → Rel 𝐴) |
111 | | relss 5793 |
. . . . 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 3994 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → 𝑧 ∈ 𝐴) |
115 | 113, 114 | ffvelcdmd 7104 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 supp 0 )) → (𝐹‘𝑧) ∈ 𝐵) |
116 | 107, 108,
1, 109, 112, 28, 3, 115 | gsummpt2d 33034 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑧))) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |
117 | 104, 106,
116 | 3eqtr3d 2782 |
. 2
⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom (𝐹 supp 0 ) ↦ (𝑊 Σg
(𝑦 ∈ ((𝐹 supp 0 ) “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |
118 | 42, 102, 117 | 3eqtr4rd 2785 |
1
⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘〈𝑥, 𝑦〉)))))) |