Step | Hyp | Ref
| Expression |
1 | | gsum2d.w |
. . . 4
⊢ (𝜑 → 𝐹 finSupp 0 ) |
2 | 1 | fsuppimpd 8165 |
. . 3
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
3 | | dmfi 8129 |
. . 3
⊢ ((𝐹 supp 0 ) ∈ Fin → dom
(𝐹 supp 0 ) ∈
Fin) |
4 | 2, 3 | syl 17 |
. 2
⊢ (𝜑 → dom (𝐹 supp 0 ) ∈
Fin) |
5 | | reseq2 5312 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐴 ↾ 𝑥) = (𝐴 ↾ ∅)) |
6 | | res0 5321 |
. . . . . . . . 9
⊢ (𝐴 ↾ ∅) =
∅ |
7 | 5, 6 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝐴 ↾ 𝑥) = ∅) |
8 | 7 | reseq2d 5317 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ ∅)) |
9 | | res0 5321 |
. . . . . . 7
⊢ (𝐹 ↾ ∅) =
∅ |
10 | 8, 9 | syl6eq 2660 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐹 ↾ (𝐴 ↾ 𝑥)) = ∅) |
11 | 10 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg
∅)) |
12 | | mpteq1 4665 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
13 | | mpt0 5934 |
. . . . . . 7
⊢ (𝑗 ∈ ∅ ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅ |
14 | 12, 13 | syl6eq 2660 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅) |
15 | 14 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg
∅)) |
16 | 11, 15 | eqeq12d 2625 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg ∅) =
(𝐺
Σg ∅))) |
17 | 16 | imbi2d 329 |
. . 3
⊢ (𝑥 = ∅ → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg ∅) =
(𝐺
Σg ∅)))) |
18 | | reseq2 5312 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴 ↾ 𝑥) = (𝐴 ↾ 𝑦)) |
19 | 18 | reseq2d 5317 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ 𝑦))) |
20 | 19 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))) |
21 | | mpteq1 4665 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
22 | 21 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
23 | 20, 22 | eqeq12d 2625 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
24 | 23 | imbi2d 329 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
25 | | reseq2 5312 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ↾ 𝑥) = (𝐴 ↾ (𝑦 ∪ {𝑧}))) |
26 | 25 | reseq2d 5317 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) |
27 | 26 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))) |
28 | | mpteq1 4665 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
29 | 28 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
30 | 27, 29 | eqeq12d 2625 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
31 | 30 | imbi2d 329 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
32 | | reseq2 5312 |
. . . . . . 7
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝐴 ↾ 𝑥) = (𝐴 ↾ dom (𝐹 supp 0 ))) |
33 | 32 | reseq2d 5317 |
. . . . . 6
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) |
34 | 33 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 ))))) |
35 | | mpteq1 4665 |
. . . . . 6
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
36 | 35 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝐺 Σg
(𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
37 | 34, 36 | eqeq12d 2625 |
. . . 4
⊢ (𝑥 = dom (𝐹 supp 0 ) → ((𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
38 | 37 | imbi2d 329 |
. . 3
⊢ (𝑥 = dom (𝐹 supp 0 ) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
39 | | eqidd 2611 |
. . 3
⊢ (𝜑 → (𝐺 Σg ∅) =
(𝐺
Σg ∅)) |
40 | | oveq1 6556 |
. . . . . 6
⊢ ((𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
41 | | gsum2d.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
42 | | gsum2d.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
43 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
44 | | gsum2d.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ CMnd) |
45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐺 ∈ CMnd) |
46 | | gsum2d.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
47 | | resexg 5362 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V) |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V) |
49 | 48 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V) |
50 | | gsum2d.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
51 | | resss 5342 |
. . . . . . . . . . 11
⊢ (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴 |
52 | | fssres 5983 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵) |
53 | 50, 51, 52 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵) |
54 | 53 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵) |
55 | | ffun 5961 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
56 | 50, 55 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun 𝐹) |
57 | | funres 5843 |
. . . . . . . . . . . 12
⊢ (Fun
𝐹 → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) |
59 | 58 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) |
60 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐹 supp 0 ) ∈
Fin) |
61 | | fex 6394 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
62 | 50, 46, 61 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) |
63 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) ∈ V |
64 | 42, 63 | eqeltri 2684 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
65 | | ressuppss 7201 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 )) |
66 | 62, 64, 65 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 )) |
67 | 66 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 )) |
68 | | ssfi 8065 |
. . . . . . . . . . 11
⊢ (((𝐹 supp 0 ) ∈ Fin ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 )) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin) |
69 | 60, 67, 68 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin) |
70 | | resexg 5362 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ V → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V) |
71 | 62, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V) |
72 | | isfsupp 8162 |
. . . . . . . . . . . 12
⊢ (((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V ∧ 0 ∈ V) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin))) |
73 | 71, 64, 72 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin))) |
74 | 73 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin))) |
75 | 59, 69, 74 | mpbir2and 959 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ) |
76 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ¬ 𝑧 ∈ 𝑦) |
77 | | disjsn 4192 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
78 | 76, 77 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅) |
79 | 78 | reseq2d 5317 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↾ (𝑦 ∩ {𝑧})) = (𝐴 ↾ ∅)) |
80 | | resindi 5332 |
. . . . . . . . . 10
⊢ (𝐴 ↾ (𝑦 ∩ {𝑧})) = ((𝐴 ↾ 𝑦) ∩ (𝐴 ↾ {𝑧})) |
81 | 79, 80, 6 | 3eqtr3g 2667 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐴 ↾ 𝑦) ∩ (𝐴 ↾ {𝑧})) = ∅) |
82 | | resundi 5330 |
. . . . . . . . . 10
⊢ (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴 ↾ 𝑦) ∪ (𝐴 ↾ {𝑧})) |
83 | 82 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴 ↾ 𝑦) ∪ (𝐴 ↾ {𝑧}))) |
84 | 41, 42, 43, 45, 49, 54, 75, 81, 83 | gsumsplit 18151 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧}))))) |
85 | | ssun1 3738 |
. . . . . . . . . . 11
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
86 | | ssres2 5345 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (𝐴 ↾ 𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧}))) |
87 | | resabs1 5347 |
. . . . . . . . . . 11
⊢ ((𝐴 ↾ 𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)) = (𝐹 ↾ (𝐴 ↾ 𝑦))) |
88 | 85, 86, 87 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)) = (𝐹 ↾ (𝐴 ↾ 𝑦)) |
89 | 88 | oveq2i 6560 |
. . . . . . . . 9
⊢ (𝐺 Σg
((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) |
90 | | ssun2 3739 |
. . . . . . . . . . 11
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) |
91 | | ssres2 5345 |
. . . . . . . . . . 11
⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → (𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧}))) |
92 | | resabs1 5347 |
. . . . . . . . . . 11
⊢ ((𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧}))) |
93 | 90, 91, 92 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧})) |
94 | 93 | oveq2i 6560 |
. . . . . . . . 9
⊢ (𝐺 Σg
((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))) |
95 | 89, 94 | oveq12i 6561 |
. . . . . . . 8
⊢ ((𝐺 Σg
((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) |
96 | 84, 95 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
97 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin) |
98 | | gsum2d.r |
. . . . . . . . . . 11
⊢ (𝜑 → Rel 𝐴) |
99 | | gsum2d.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
100 | | gsum2d.s |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐴 ⊆ 𝐷) |
101 | 41, 42, 44, 46, 98, 99, 100, 50, 1 | gsum2dlem1 18192 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
102 | 101 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ 𝑗 ∈ 𝑦) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
103 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
104 | 103 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑧 ∈ V) |
105 | | sneq 4135 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑧 → {𝑗} = {𝑧}) |
106 | 105 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑧 → (𝐴 “ {𝑗}) = (𝐴 “ {𝑧})) |
107 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑧 → (𝑗𝐹𝑘) = (𝑧𝐹𝑘)) |
108 | 106, 107 | mpteq12dv 4663 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑧 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑧 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))) |
110 | 109 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵 ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)) |
111 | 110 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑧 → ((𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) ↔ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵))) |
112 | 111, 101 | chvarv 2251 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵) |
113 | 112 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵) |
114 | 41, 43, 45, 97, 102, 104, 76, 113, 109 | gsumunsn 18182 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))))) |
115 | 105 | reseq2d 5317 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑧 → (𝐴 ↾ {𝑗}) = (𝐴 ↾ {𝑧})) |
116 | 115 | reseq2d 5317 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑧 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝐹 ↾ (𝐴 ↾ {𝑧}))) |
117 | 116 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑧 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) |
118 | 109, 117 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
119 | 118 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑧 → ((𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗})))) ↔ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))) |
120 | | imaexg 6995 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ {𝑗}) ∈ V) |
121 | 46, 120 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 “ {𝑗}) ∈ V) |
122 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑗 ∈ V |
123 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑘 ∈ V |
124 | 122, 123 | elimasn 5409 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) ↔ 〈𝑗, 𝑘〉 ∈ 𝐴) |
125 | | df-ov 6552 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗𝐹𝑘) = (𝐹‘〈𝑗, 𝑘〉) |
126 | 50 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ 𝐴) → (𝐹‘〈𝑗, 𝑘〉) ∈ 𝐵) |
127 | 125, 126 | syl5eqel 2692 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ 𝐴) → (𝑗𝐹𝑘) ∈ 𝐵) |
128 | 124, 127 | sylan2b 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 “ {𝑗})) → (𝑗𝐹𝑘) ∈ 𝐵) |
129 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) |
130 | 128, 129 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)):(𝐴 “ {𝑗})⟶𝐵) |
131 | | funmpt 5840 |
. . . . . . . . . . . . . . 15
⊢ Fun
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) |
133 | | rnfi 8132 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 supp 0 ) ∈ Fin → ran
(𝐹 supp 0 ) ∈
Fin) |
134 | 2, 133 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran (𝐹 supp 0 ) ∈
Fin) |
135 | 124 | biimpi 205 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) → 〈𝑗, 𝑘〉 ∈ 𝐴) |
136 | 122, 123 | opelrn 5278 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ) → 𝑘 ∈ ran (𝐹 supp 0 )) |
137 | 136 | con3i 149 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑘 ∈ ran (𝐹 supp 0 ) → ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 )) |
138 | 135, 137 | anim12i 588 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ (𝐴 “ {𝑗}) ∧ ¬ 𝑘 ∈ ran (𝐹 supp 0 )) → (〈𝑗, 𝑘〉 ∈ 𝐴 ∧ ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ))) |
139 | | eldif 3550 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 )) ↔ (𝑘 ∈ (𝐴 “ {𝑗}) ∧ ¬ 𝑘 ∈ ran (𝐹 supp 0 ))) |
140 | | eldif 3550 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 )) ↔ (〈𝑗, 𝑘〉 ∈ 𝐴 ∧ ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ))) |
141 | 138, 139,
140 | 3imtr4i 280 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 )) → 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
142 | | ssid 3587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ) |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
144 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈ V) |
145 | 50, 143, 46, 144 | suppssr 7213 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝐹‘〈𝑗, 𝑘〉) = 0 ) |
146 | 125, 145 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 ) |
147 | 141, 146 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 ) |
148 | 147, 121 | suppss2 7216 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ⊆ ran (𝐹 supp 0 )) |
149 | | ssfi 8065 |
. . . . . . . . . . . . . . 15
⊢ ((ran
(𝐹 supp 0 ) ∈ Fin ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ⊆ ran (𝐹 supp 0 )) → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈
Fin) |
150 | 134, 148,
149 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈
Fin) |
151 | | mptexg 6389 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 “ {𝑗}) ∈ V → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V) |
152 | 121, 151 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V) |
153 | | isfsupp 8162 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V ∧ 0 ∈ V) → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ↔ (Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈
Fin))) |
154 | 152, 64, 153 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ↔ (Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈
Fin))) |
155 | 132, 150,
154 | mpbir2and 959 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ) |
156 | | 2ndconst 7153 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ V → (2nd
↾ ({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗})) |
157 | 122, 156 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2nd ↾
({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗})) |
158 | 41, 42, 44, 121, 130, 155, 157 | gsumf1o 18140 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))))) |
159 | | 1st2nd2 7096 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
160 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st ‘𝑥) ∈ {𝑗}) |
161 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑥) ∈ {𝑗} → (1st ‘𝑥) = 𝑗) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st ‘𝑥) = 𝑗) |
163 | 162 | opeq1d 4346 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑗, (2nd ‘𝑥)〉) |
164 | 159, 163 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = 〈𝑗, (2nd ‘𝑥)〉) |
165 | 164 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹‘𝑥) = (𝐹‘〈𝑗, (2nd ‘𝑥)〉)) |
166 | | df-ov 6552 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗𝐹(2nd ‘𝑥)) = (𝐹‘〈𝑗, (2nd ‘𝑥)〉) |
167 | 165, 166 | syl6eqr 2662 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹‘𝑥) = (𝑗𝐹(2nd ‘𝑥))) |
168 | 167 | mpteq2ia 4668 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd ‘𝑥))) |
169 | 50 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
170 | 169 | reseq1d 5316 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗}))) |
171 | | resss 5342 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ↾ {𝑗}) ⊆ 𝐴 |
172 | | resmpt 5369 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ↾ {𝑗}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥))) |
173 | 171, 172 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥)) |
174 | | ressn 5588 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ↾ {𝑗}) = ({𝑗} × (𝐴 “ {𝑗})) |
175 | | mpteq1 4665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ↾ {𝑗}) = ({𝑗} × (𝐴 “ {𝑗})) → (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥))) |
176 | 174, 175 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥)) |
177 | 173, 176 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥)) |
178 | 170, 177 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥))) |
179 | | xp2nd 7090 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑗})) |
180 | 179 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗}))) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑗})) |
181 | | fo2nd 7080 |
. . . . . . . . . . . . . . . . . . 19
⊢
2nd :V–onto→V |
182 | | fof 6028 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
183 | 181, 182 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2nd
:V⟶V) |
184 | 183 | feqmptd 6159 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2nd = (𝑥 ∈ V ↦
(2nd ‘𝑥))) |
185 | 184 | reseq1d 5316 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2nd ↾
({𝑗} × (𝐴 “ {𝑗}))) = ((𝑥 ∈ V ↦ (2nd
‘𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗})))) |
186 | | ssv 3588 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑗} × (𝐴 “ {𝑗})) ⊆ V |
187 | | resmpt 5369 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑗} × (𝐴 “ {𝑗})) ⊆ V → ((𝑥 ∈ V ↦ (2nd
‘𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥))) |
188 | 186, 187 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ↦
(2nd ‘𝑥))
↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥)) |
189 | 185, 188 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd ↾
({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥))) |
190 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) |
191 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (2nd ‘𝑥) → (𝑗𝐹𝑘) = (𝑗𝐹(2nd ‘𝑥))) |
192 | 180, 189,
190, 191 | fmptco 6303 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd ‘𝑥)))) |
193 | 168, 178,
192 | 3eqtr4a 2670 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))) |
194 | 193 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))))) |
195 | 158, 194 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗})))) |
196 | 119, 195 | chvarv 2251 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) |
197 | 196 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) |
198 | 197 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
199 | 114, 198 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
200 | 96, 199 | eqeq12d 2625 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))) |
201 | 40, 200 | syl5ibr 235 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
202 | 201 | expcom 450 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
203 | 202 | a2d 29 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) → (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
204 | 17, 24, 31, 38, 39, 203 | findcard2s 8086 |
. 2
⊢ (dom
(𝐹 supp 0 ) ∈ Fin → (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
205 | 4, 204 | mpcom 37 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |