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 18370 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
11 | | suppssdm 7308 |
. . . . . 6
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
12 | | fdm 6051 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
13 | 8, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
14 | 11, 13 | syl5sseq 3653 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
15 | | relss 5206 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → (Rel 𝐴 → Rel (𝐹 supp 0 ))) |
16 | 14, 5, 15 | sylc 65 |
. . . . . 6
⊢ (𝜑 → Rel (𝐹 supp 0 )) |
17 | | relssdmrn 5656 |
. . . . . . 7
⊢ (Rel
(𝐹 supp 0 ) → (𝐹 supp 0 ) ⊆ (dom (𝐹 supp 0 ) × ran (𝐹 supp 0 ))) |
18 | | ssv 3625 |
. . . . . . . 8
⊢ ran
(𝐹 supp 0 ) ⊆
V |
19 | | xpss2 5229 |
. . . . . . . 8
⊢ (ran
(𝐹 supp 0 ) ⊆ V → (dom
(𝐹 supp 0 ) × ran (𝐹 supp 0 )) ⊆ (dom (𝐹 supp 0 ) ×
V)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ (dom
(𝐹 supp 0 ) × ran (𝐹 supp 0 )) ⊆ (dom (𝐹 supp 0 ) ×
V) |
21 | 17, 20 | syl6ss 3615 |
. . . . . 6
⊢ (Rel
(𝐹 supp 0 ) → (𝐹 supp 0 ) ⊆ (dom (𝐹 supp 0 ) ×
V)) |
22 | 16, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (dom (𝐹 supp 0 ) ×
V)) |
23 | 14, 22 | ssind 3837 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐴 ∩ (dom (𝐹 supp 0 ) ×
V))) |
24 | | df-res 5126 |
. . . 4
⊢ (𝐴 ↾ dom (𝐹 supp 0 )) = (𝐴 ∩ (dom (𝐹 supp 0 ) ×
V)) |
25 | 23, 24 | syl6sseqr 3652 |
. . 3
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐴 ↾ dom (𝐹 supp 0 ))) |
26 | 1, 2, 3, 4, 8, 25,
9 | gsumres 18314 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg 𝐹)) |
27 | | dmss 5323 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → dom (𝐹 supp 0 ) ⊆ dom 𝐴) |
28 | 14, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ dom 𝐴) |
29 | 28, 7 | sstrd 3613 |
. . . . 5
⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ 𝐷) |
30 | 29 | resmptd 5452 |
. . . 4
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 )) = (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
31 | 30 | oveq2d 6666 |
. . 3
⊢ (𝜑 → (𝐺 Σg ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 ))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
32 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | gsum2dlem1 18369 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
33 | 32 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
34 | | eqid 2622 |
. . . . 5
⊢ (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) |
35 | 33, 34 | fmptd 6385 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))):𝐷⟶𝐵) |
36 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑗 ∈ V |
37 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑘 ∈ V |
38 | 36, 37 | elimasn 5490 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) ↔ 〈𝑗, 𝑘〉 ∈ 𝐴) |
39 | 38 | biimpi 206 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) → 〈𝑗, 𝑘〉 ∈ 𝐴) |
40 | 39 | ad2antll 765 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → 〈𝑗, 𝑘〉 ∈ 𝐴) |
41 | | eldifn 3733 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) → ¬ 𝑗 ∈ dom (𝐹 supp 0 )) |
42 | 41 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → ¬ 𝑗 ∈ dom (𝐹 supp 0 )) |
43 | 36, 37 | opeldm 5328 |
. . . . . . . . . . . 12
⊢
(〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ) → 𝑗 ∈ dom (𝐹 supp 0 )) |
44 | 42, 43 | nsyl 135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 )) |
45 | 40, 44 | eldifd 3585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
46 | | df-ov 6653 |
. . . . . . . . . . 11
⊢ (𝑗𝐹𝑘) = (𝐹‘〈𝑗, 𝑘〉) |
47 | | ssid 3624 |
. . . . . . . . . . . . 13
⊢ (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ) |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
49 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) ∈ V |
50 | 2, 49 | eqeltri 2697 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ V) |
52 | 8, 48, 4, 51 | suppssr 7326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝐹‘〈𝑗, 𝑘〉) = 0 ) |
53 | 46, 52 | syl5eq 2668 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 ) |
54 | 45, 53 | syldan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → (𝑗𝐹𝑘) = 0 ) |
55 | 54 | anassrs 680 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) ∧ 𝑘 ∈ (𝐴 “ {𝑗})) → (𝑗𝐹𝑘) = 0 ) |
56 | 55 | mpteq2dva 4744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) |
57 | 56 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 ))) |
58 | | cmnmnd 18208 |
. . . . . . . . 9
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
59 | 3, 58 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Mnd) |
60 | | imaexg 7103 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ {𝑗}) ∈ V) |
61 | 4, 60 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 “ {𝑗}) ∈ V) |
62 | 2 | gsumz 17374 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝐴 “ {𝑗}) ∈ V) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
63 | 59, 61, 62 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
64 | 63 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
65 | 57, 64 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = 0 ) |
66 | 65, 6 | suppss2 7329 |
. . . 4
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ⊆ dom (𝐹 supp 0 )) |
67 | | funmpt 5926 |
. . . . . 6
⊢ Fun
(𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) |
68 | 67 | a1i 11 |
. . . . 5
⊢ (𝜑 → Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
69 | 9 | fsuppimpd 8282 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
70 | | dmfi 8244 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ∈ Fin → dom
(𝐹 supp 0 ) ∈
Fin) |
71 | 69, 70 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 supp 0 ) ∈
Fin) |
72 | | ssfi 8180 |
. . . . . 6
⊢ ((dom
(𝐹 supp 0 ) ∈ Fin ∧ ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ⊆ dom (𝐹 supp 0 )) → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin) |
73 | 71, 66, 72 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin) |
74 | | mptexg 6484 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑊 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∈ V) |
75 | 6, 74 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∈ V) |
76 | | isfsupp 8279 |
. . . . . 6
⊢ (((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∈ V ∧ 0 ∈ V) → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∧ ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin))) |
77 | 75, 51, 76 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∧ ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin))) |
78 | 68, 73, 77 | mpbir2and 957 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ) |
79 | 1, 2, 3, 6, 35, 66, 78 | gsumres 18314 |
. . 3
⊢ (𝜑 → (𝐺 Σg ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 ))) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
80 | 31, 79 | eqtr3d 2658 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
81 | 10, 26, 80 | 3eqtr3d 2664 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |