Proof of Theorem gsum2d
Step | Hyp | Ref
| Expression |
1 | | gsum2d.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
2 | | gsum2d.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
3 | | gsum2d.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ CMnd) |
4 | | gsum2d.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | gsum2d.r |
. . 3
⊢ (𝜑 → Rel 𝐴) |
6 | | gsum2d.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
7 | | gsum2d.s |
. . 3
⊢ (𝜑 → dom 𝐴 ⊆ 𝐷) |
8 | | gsum2d.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
9 | | gsum2d.w |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | gsum2dlem2 19356 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
11 | | suppssdm 7919 |
. . . . . 6
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
12 | 11, 8 | fssdm 6565 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
13 | | relss 5653 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → (Rel 𝐴 → Rel (𝐹 supp 0 ))) |
14 | 12, 5, 13 | sylc 65 |
. . . . . 6
⊢ (𝜑 → Rel (𝐹 supp 0 )) |
15 | | relssdmrn 6132 |
. . . . . . 7
⊢ (Rel
(𝐹 supp 0 ) → (𝐹 supp 0 ) ⊆ (dom (𝐹 supp 0 ) × ran (𝐹 supp 0 ))) |
16 | | ssv 3925 |
. . . . . . . 8
⊢ ran
(𝐹 supp 0 ) ⊆
V |
17 | | xpss2 5571 |
. . . . . . . 8
⊢ (ran
(𝐹 supp 0 ) ⊆ V → (dom
(𝐹 supp 0 ) × ran (𝐹 supp 0 )) ⊆ (dom (𝐹 supp 0 ) ×
V)) |
18 | 16, 17 | ax-mp 5 |
. . . . . . 7
⊢ (dom
(𝐹 supp 0 ) × ran (𝐹 supp 0 )) ⊆ (dom (𝐹 supp 0 ) ×
V) |
19 | 15, 18 | sstrdi 3913 |
. . . . . 6
⊢ (Rel
(𝐹 supp 0 ) → (𝐹 supp 0 ) ⊆ (dom (𝐹 supp 0 ) ×
V)) |
20 | 14, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (dom (𝐹 supp 0 ) ×
V)) |
21 | 12, 20 | ssind 4147 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐴 ∩ (dom (𝐹 supp 0 ) ×
V))) |
22 | | df-res 5563 |
. . . 4
⊢ (𝐴 ↾ dom (𝐹 supp 0 )) = (𝐴 ∩ (dom (𝐹 supp 0 ) ×
V)) |
23 | 21, 22 | sseqtrrdi 3952 |
. . 3
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐴 ↾ dom (𝐹 supp 0 ))) |
24 | 1, 2, 3, 4, 8, 23,
9 | gsumres 19298 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg 𝐹)) |
25 | | dmss 5771 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → dom (𝐹 supp 0 ) ⊆ dom 𝐴) |
26 | 12, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ dom 𝐴) |
27 | 26, 7 | sstrd 3911 |
. . . . 5
⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ 𝐷) |
28 | 27 | resmptd 5908 |
. . . 4
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 )) = (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
29 | 28 | oveq2d 7229 |
. . 3
⊢ (𝜑 → (𝐺 Σg ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 ))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
30 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | gsum2dlem1 19355 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
31 | 30 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
32 | 31 | fmpttd 6932 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))):𝐷⟶𝐵) |
33 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑗 ∈ V |
34 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑘 ∈ V |
35 | 33, 34 | elimasn 5957 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) ↔ 〈𝑗, 𝑘〉 ∈ 𝐴) |
36 | 35 | biimpi 219 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) → 〈𝑗, 𝑘〉 ∈ 𝐴) |
37 | 36 | ad2antll 729 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → 〈𝑗, 𝑘〉 ∈ 𝐴) |
38 | | eldifn 4042 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) → ¬ 𝑗 ∈ dom (𝐹 supp 0 )) |
39 | 38 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → ¬ 𝑗 ∈ dom (𝐹 supp 0 )) |
40 | 33, 34 | opeldm 5776 |
. . . . . . . . . . . 12
⊢
(〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ) → 𝑗 ∈ dom (𝐹 supp 0 )) |
41 | 39, 40 | nsyl 142 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 )) |
42 | 37, 41 | eldifd 3877 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
43 | | df-ov 7216 |
. . . . . . . . . . 11
⊢ (𝑗𝐹𝑘) = (𝐹‘〈𝑗, 𝑘〉) |
44 | | ssidd 3924 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
45 | 2 | fvexi 6731 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
46 | 45 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ V) |
47 | 8, 44, 4, 46 | suppssr 7938 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝐹‘〈𝑗, 𝑘〉) = 0 ) |
48 | 43, 47 | syl5eq 2790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 ) |
49 | 42, 48 | syldan 594 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → (𝑗𝐹𝑘) = 0 ) |
50 | 49 | anassrs 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) ∧ 𝑘 ∈ (𝐴 “ {𝑗})) → (𝑗𝐹𝑘) = 0 ) |
51 | 50 | mpteq2dva 5150 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) |
52 | 51 | oveq2d 7229 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 ))) |
53 | | cmnmnd 19186 |
. . . . . . . . 9
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
54 | 3, 53 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Mnd) |
55 | | imaexg 7693 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ {𝑗}) ∈ V) |
56 | 4, 55 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 “ {𝑗}) ∈ V) |
57 | 2 | gsumz 18262 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝐴 “ {𝑗}) ∈ V) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
58 | 54, 56, 57 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
59 | 58 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
60 | 52, 59 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = 0 ) |
61 | 60, 6 | suppss2 7942 |
. . . 4
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ⊆ dom (𝐹 supp 0 )) |
62 | | funmpt 6418 |
. . . . . 6
⊢ Fun
(𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) |
63 | 62 | a1i 11 |
. . . . 5
⊢ (𝜑 → Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
64 | 9 | fsuppimpd 8992 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
65 | | dmfi 8954 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ∈ Fin → dom
(𝐹 supp 0 ) ∈
Fin) |
66 | 64, 65 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 supp 0 ) ∈
Fin) |
67 | 66, 61 | ssfid 8898 |
. . . . 5
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin) |
68 | 6 | mptexd 7040 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∈ V) |
69 | | isfsupp 8989 |
. . . . . 6
⊢ (((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∈ V ∧ 0 ∈ V) → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∧ ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin))) |
70 | 68, 46, 69 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∧ ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin))) |
71 | 63, 67, 70 | mpbir2and 713 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ) |
72 | 1, 2, 3, 6, 32, 61, 71 | gsumres 19298 |
. . 3
⊢ (𝜑 → (𝐺 Σg ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 ))) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
73 | 29, 72 | eqtr3d 2779 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
74 | 10, 24, 73 | 3eqtr3d 2785 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |