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 18193 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
11 | | suppssdm 7195 |
. . . . . 6
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
12 | | fdm 5964 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
13 | 8, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
14 | 11, 13 | syl5sseq 3616 |
. . . . 5
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
15 | | relss 5129 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → (Rel 𝐴 → Rel (𝐹 supp 0 ))) |
16 | 14, 5, 15 | sylc 63 |
. . . . . 6
⊢ (𝜑 → Rel (𝐹 supp 0 )) |
17 | | relssdmrn 5573 |
. . . . . . 7
⊢ (Rel
(𝐹 supp 0 ) → (𝐹 supp 0 ) ⊆ (dom (𝐹 supp 0 ) × ran (𝐹 supp 0 ))) |
18 | | ssv 3588 |
. . . . . . . 8
⊢ ran
(𝐹 supp 0 ) ⊆
V |
19 | | xpss2 5152 |
. . . . . . . 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 3580 |
. . . . . 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 3799 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐴 ∩ (dom (𝐹 supp 0 ) ×
V))) |
24 | | df-res 5050 |
. . . 4
⊢ (𝐴 ↾ dom (𝐹 supp 0 )) = (𝐴 ∩ (dom (𝐹 supp 0 ) ×
V)) |
25 | 23, 24 | syl6sseqr 3615 |
. . 3
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐴 ↾ dom (𝐹 supp 0 ))) |
26 | 1, 2, 3, 4, 8, 25,
9 | gsumres 18137 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg 𝐹)) |
27 | | dmss 5245 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ⊆ 𝐴 → dom (𝐹 supp 0 ) ⊆ dom 𝐴) |
28 | 14, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ dom 𝐴) |
29 | 28, 7 | sstrd 3578 |
. . . . 5
⊢ (𝜑 → dom (𝐹 supp 0 ) ⊆ 𝐷) |
30 | 29 | resmptd 5371 |
. . . 4
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 )) = (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
31 | 30 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (𝐺 Σg ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 ))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
32 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | gsum2dlem1 18192 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
33 | 32 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
34 | | eqid 2610 |
. . . . 5
⊢ (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) |
35 | 33, 34 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))):𝐷⟶𝐵) |
36 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑗 ∈ V |
37 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑘 ∈ V |
38 | 36, 37 | elimasn 5409 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) ↔ 〈𝑗, 𝑘〉 ∈ 𝐴) |
39 | 38 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) → 〈𝑗, 𝑘〉 ∈ 𝐴) |
40 | 39 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → 〈𝑗, 𝑘〉 ∈ 𝐴) |
41 | | eldifn 3695 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) → ¬ 𝑗 ∈ dom (𝐹 supp 0 )) |
42 | 41 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → ¬ 𝑗 ∈ dom (𝐹 supp 0 )) |
43 | 36, 37 | opeldm 5250 |
. . . . . . . . . . . 12
⊢
(〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ) → 𝑗 ∈ dom (𝐹 supp 0 )) |
44 | 42, 43 | nsyl 134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 )) |
45 | 40, 44 | eldifd 3551 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
46 | | df-ov 6552 |
. . . . . . . . . . 11
⊢ (𝑗𝐹𝑘) = (𝐹‘〈𝑗, 𝑘〉) |
47 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ) |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
49 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) ∈ V |
50 | 2, 49 | eqeltri 2684 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ V) |
52 | 8, 48, 4, 51 | suppssr 7213 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝐹‘〈𝑗, 𝑘〉) = 0 ) |
53 | 46, 52 | syl5eq 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 ) |
54 | 45, 53 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 )) ∧ 𝑘 ∈ (𝐴 “ {𝑗}))) → (𝑗𝐹𝑘) = 0 ) |
55 | 54 | anassrs 678 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) ∧ 𝑘 ∈ (𝐴 “ {𝑗})) → (𝑗𝐹𝑘) = 0 ) |
56 | 55 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) |
57 | 56 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 ))) |
58 | | cmnmnd 18031 |
. . . . . . . . 9
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
59 | 3, 58 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Mnd) |
60 | | imaexg 6995 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ {𝑗}) ∈ V) |
61 | 4, 60 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 “ {𝑗}) ∈ V) |
62 | 2 | gsumz 17197 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝐴 “ {𝑗}) ∈ V) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
63 | 59, 61, 62 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
64 | 63 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ 0 )) = 0 ) |
65 | 57, 64 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐷 ∖ dom (𝐹 supp 0 ))) → (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = 0 ) |
66 | 65, 6 | suppss2 7216 |
. . . 4
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ⊆ dom (𝐹 supp 0 )) |
67 | | funmpt 5840 |
. . . . . 6
⊢ Fun
(𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) |
68 | 67 | a1i 11 |
. . . . 5
⊢ (𝜑 → Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
69 | 9 | fsuppimpd 8165 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
70 | | dmfi 8129 |
. . . . . . 7
⊢ ((𝐹 supp 0 ) ∈ Fin → dom
(𝐹 supp 0 ) ∈
Fin) |
71 | 69, 70 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 supp 0 ) ∈
Fin) |
72 | | ssfi 8065 |
. . . . . 6
⊢ ((dom
(𝐹 supp 0 ) ∈ Fin ∧ ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ⊆ dom (𝐹 supp 0 )) → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin) |
73 | 71, 66, 72 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin) |
74 | | mptexg 6389 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑊 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∈ V) |
75 | 6, 74 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∈ V) |
76 | | isfsupp 8162 |
. . . . . 6
⊢ (((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∈ V ∧ 0 ∈ V) → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∧ ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin))) |
77 | 75, 51, 76 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ∧ ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) supp 0 ) ∈
Fin))) |
78 | 68, 73, 77 | mpbir2and 959 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) finSupp 0 ) |
79 | 1, 2, 3, 6, 35, 66, 78 | gsumres 18137 |
. . 3
⊢ (𝜑 → (𝐺 Σg ((𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) ↾ dom (𝐹 supp 0 ))) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
80 | 31, 79 | eqtr3d 2646 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
81 | 10, 26, 80 | 3eqtr3d 2652 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |