Step | Hyp | Ref
| Expression |
1 | | gsum2d.w |
. . . 4
⊢ (𝜑 → 𝐹 finSupp 0 ) |
2 | 1 | fsuppimpd 8570 |
. . 3
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
3 | | dmfi 8532 |
. . 3
⊢ ((𝐹 supp 0 ) ∈ Fin → dom
(𝐹 supp 0 ) ∈
Fin) |
4 | 2, 3 | syl 17 |
. 2
⊢ (𝜑 → dom (𝐹 supp 0 ) ∈
Fin) |
5 | | reseq2 5637 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐴 ↾ 𝑥) = (𝐴 ↾ ∅)) |
6 | | res0 5646 |
. . . . . . . . 9
⊢ (𝐴 ↾ ∅) =
∅ |
7 | 5, 6 | syl6eq 2830 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝐴 ↾ 𝑥) = ∅) |
8 | 7 | reseq2d 5642 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ ∅)) |
9 | | res0 5646 |
. . . . . . 7
⊢ (𝐹 ↾ ∅) =
∅ |
10 | 8, 9 | syl6eq 2830 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐹 ↾ (𝐴 ↾ 𝑥)) = ∅) |
11 | 10 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg
∅)) |
12 | | mpteq1 4972 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
13 | | mpt0 6267 |
. . . . . . 7
⊢ (𝑗 ∈ ∅ ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅ |
14 | 12, 13 | syl6eq 2830 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅) |
15 | 14 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg
∅)) |
16 | 11, 15 | eqeq12d 2793 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg ∅) =
(𝐺
Σg ∅))) |
17 | 16 | imbi2d 332 |
. . 3
⊢ (𝑥 = ∅ → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg ∅) =
(𝐺
Σg ∅)))) |
18 | | reseq2 5637 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴 ↾ 𝑥) = (𝐴 ↾ 𝑦)) |
19 | 18 | reseq2d 5642 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ 𝑦))) |
20 | 19 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))) |
21 | | mpteq1 4972 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
22 | 21 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
23 | 20, 22 | eqeq12d 2793 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
24 | 23 | imbi2d 332 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
25 | | reseq2 5637 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ↾ 𝑥) = (𝐴 ↾ (𝑦 ∪ {𝑧}))) |
26 | 25 | reseq2d 5642 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) |
27 | 26 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))) |
28 | | mpteq1 4972 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
29 | 28 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
30 | 27, 29 | eqeq12d 2793 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
31 | 30 | imbi2d 332 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
32 | | reseq2 5637 |
. . . . . . 7
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝐴 ↾ 𝑥) = (𝐴 ↾ dom (𝐹 supp 0 ))) |
33 | 32 | reseq2d 5642 |
. . . . . 6
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) |
34 | 33 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 ))))) |
35 | | mpteq1 4972 |
. . . . . 6
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) |
36 | 35 | oveq2d 6938 |
. . . . 5
⊢ (𝑥 = dom (𝐹 supp 0 ) → (𝐺 Σg
(𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |
37 | 34, 36 | eqeq12d 2793 |
. . . 4
⊢ (𝑥 = dom (𝐹 supp 0 ) → ((𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
38 | 37 | imbi2d 332 |
. . 3
⊢ (𝑥 = dom (𝐹 supp 0 ) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
39 | | eqidd 2779 |
. . 3
⊢ (𝜑 → (𝐺 Σg ∅) =
(𝐺
Σg ∅)) |
40 | | oveq1 6929 |
. . . . . 6
⊢ ((𝐺 Σg
(𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
41 | | gsum2d.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
42 | | gsum2d.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
43 | | eqid 2778 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
44 | | gsum2d.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ CMnd) |
45 | 44 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐺 ∈ CMnd) |
46 | | gsum2d.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
47 | | resexg 5692 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V) |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V) |
49 | 48 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V) |
50 | | gsum2d.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
51 | | resss 5671 |
. . . . . . . . . . 11
⊢ (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴 |
52 | | fssres 6320 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵) |
53 | 50, 51, 52 | sylancl 580 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵) |
54 | 53 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵) |
55 | 50 | ffund 6295 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun 𝐹) |
56 | | funres 6177 |
. . . . . . . . . . . 12
⊢ (Fun
𝐹 → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) |
58 | 57 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) |
59 | 2 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐹 supp 0 ) ∈
Fin) |
60 | | fex 6761 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
61 | 50, 46, 60 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) |
62 | 42 | fvexi 6460 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
63 | | ressuppss 7595 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 )) |
64 | 61, 62, 63 | sylancl 580 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 )) |
65 | 64 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 )) |
66 | 59, 65 | ssfid 8471 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin) |
67 | | resexg 5692 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ V → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V) |
68 | 61, 67 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V) |
69 | | isfsupp 8567 |
. . . . . . . . . . . 12
⊢ (((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V ∧ 0 ∈ V) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin))) |
70 | 68, 62, 69 | sylancl 580 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin))) |
71 | 70 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈
Fin))) |
72 | 58, 66, 71 | mpbir2and 703 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ) |
73 | | simprr 763 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ¬ 𝑧 ∈ 𝑦) |
74 | | disjsn 4478 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
75 | 73, 74 | sylibr 226 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅) |
76 | 75 | reseq2d 5642 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↾ (𝑦 ∩ {𝑧})) = (𝐴 ↾ ∅)) |
77 | | resindi 5662 |
. . . . . . . . . 10
⊢ (𝐴 ↾ (𝑦 ∩ {𝑧})) = ((𝐴 ↾ 𝑦) ∩ (𝐴 ↾ {𝑧})) |
78 | 76, 77, 6 | 3eqtr3g 2837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐴 ↾ 𝑦) ∩ (𝐴 ↾ {𝑧})) = ∅) |
79 | | resundi 5660 |
. . . . . . . . . 10
⊢ (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴 ↾ 𝑦) ∪ (𝐴 ↾ {𝑧})) |
80 | 79 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴 ↾ 𝑦) ∪ (𝐴 ↾ {𝑧}))) |
81 | 41, 42, 43, 45, 49, 54, 72, 78, 80 | gsumsplit 18714 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧}))))) |
82 | | ssun1 3999 |
. . . . . . . . . . 11
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
83 | | ssres2 5674 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (𝐴 ↾ 𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧}))) |
84 | | resabs1 5676 |
. . . . . . . . . . 11
⊢ ((𝐴 ↾ 𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)) = (𝐹 ↾ (𝐴 ↾ 𝑦))) |
85 | 82, 83, 84 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)) = (𝐹 ↾ (𝐴 ↾ 𝑦)) |
86 | 85 | oveq2i 6933 |
. . . . . . . . 9
⊢ (𝐺 Σg
((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) |
87 | | ssun2 4000 |
. . . . . . . . . . 11
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) |
88 | | ssres2 5674 |
. . . . . . . . . . 11
⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → (𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧}))) |
89 | | resabs1 5676 |
. . . . . . . . . . 11
⊢ ((𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧}))) |
90 | 87, 88, 89 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧})) |
91 | 90 | oveq2i 6933 |
. . . . . . . . 9
⊢ (𝐺 Σg
((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))) |
92 | 86, 91 | oveq12i 6934 |
. . . . . . . 8
⊢ ((𝐺 Σg
((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) |
93 | 81, 92 | syl6eq 2830 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
94 | | simprl 761 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin) |
95 | | gsum2d.r |
. . . . . . . . . . 11
⊢ (𝜑 → Rel 𝐴) |
96 | | gsum2d.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
97 | | gsum2d.s |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐴 ⊆ 𝐷) |
98 | 41, 42, 44, 46, 95, 96, 97, 50, 1 | gsum2dlem1 18755 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
99 | 98 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ 𝑗 ∈ 𝑦) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
100 | | vex 3401 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
101 | 100 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑧 ∈ V) |
102 | | sneq 4408 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑧 → {𝑗} = {𝑧}) |
103 | 102 | imaeq2d 5720 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑧 → (𝐴 “ {𝑗}) = (𝐴 “ {𝑧})) |
104 | | oveq1 6929 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑧 → (𝑗𝐹𝑘) = (𝑧𝐹𝑘)) |
105 | 103, 104 | mpteq12dv 4969 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑧 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) |
106 | 105 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑧 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))) |
107 | 106 | eleq1d 2844 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵 ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)) |
108 | 107 | imbi2d 332 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑧 → ((𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) ↔ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵))) |
109 | 108, 98 | chvarv 2361 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵) |
110 | 109 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵) |
111 | 41, 43, 45, 94, 99, 101, 73, 110, 106 | gsumunsn 18745 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))))) |
112 | 102 | reseq2d 5642 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑧 → (𝐴 ↾ {𝑗}) = (𝐴 ↾ {𝑧})) |
113 | 112 | reseq2d 5642 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑧 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝐹 ↾ (𝐴 ↾ {𝑧}))) |
114 | 113 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑧 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) |
115 | 106, 114 | eqeq12d 2793 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
116 | 115 | imbi2d 332 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑧 → ((𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗})))) ↔ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))) |
117 | | imaexg 7382 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ {𝑗}) ∈ V) |
118 | 46, 117 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 “ {𝑗}) ∈ V) |
119 | | vex 3401 |
. . . . . . . . . . . . . . . 16
⊢ 𝑗 ∈ V |
120 | | vex 3401 |
. . . . . . . . . . . . . . . 16
⊢ 𝑘 ∈ V |
121 | 119, 120 | elimasn 5744 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) ↔ 〈𝑗, 𝑘〉 ∈ 𝐴) |
122 | | df-ov 6925 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗𝐹𝑘) = (𝐹‘〈𝑗, 𝑘〉) |
123 | 50 | ffvelrnda 6623 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ 𝐴) → (𝐹‘〈𝑗, 𝑘〉) ∈ 𝐵) |
124 | 122, 123 | syl5eqel 2863 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ 𝐴) → (𝑗𝐹𝑘) ∈ 𝐵) |
125 | 121, 124 | sylan2b 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 “ {𝑗})) → (𝑗𝐹𝑘) ∈ 𝐵) |
126 | 125 | fmpttd 6649 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)):(𝐴 “ {𝑗})⟶𝐵) |
127 | | funmpt 6173 |
. . . . . . . . . . . . . . 15
⊢ Fun
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) |
129 | | rnfi 8537 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 supp 0 ) ∈ Fin → ran
(𝐹 supp 0 ) ∈
Fin) |
130 | 2, 129 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran (𝐹 supp 0 ) ∈
Fin) |
131 | 121 | biimpi 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (𝐴 “ {𝑗}) → 〈𝑗, 𝑘〉 ∈ 𝐴) |
132 | 119, 120 | opelrn 5603 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ) → 𝑘 ∈ ran (𝐹 supp 0 )) |
133 | 132 | con3i 152 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑘 ∈ ran (𝐹 supp 0 ) → ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 )) |
134 | 131, 133 | anim12i 606 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ (𝐴 “ {𝑗}) ∧ ¬ 𝑘 ∈ ran (𝐹 supp 0 )) → (〈𝑗, 𝑘〉 ∈ 𝐴 ∧ ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ))) |
135 | | eldif 3802 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 )) ↔ (𝑘 ∈ (𝐴 “ {𝑗}) ∧ ¬ 𝑘 ∈ ran (𝐹 supp 0 ))) |
136 | | eldif 3802 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 )) ↔ (〈𝑗, 𝑘〉 ∈ 𝐴 ∧ ¬ 〈𝑗, 𝑘〉 ∈ (𝐹 supp 0 ))) |
137 | 134, 135,
136 | 3imtr4i 284 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 )) → 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) |
138 | | ssidd 3843 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
139 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈ V) |
140 | 50, 138, 46, 139 | suppssr 7608 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝐹‘〈𝑗, 𝑘〉) = 0 ) |
141 | 122, 140 | syl5eq 2826 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 〈𝑗, 𝑘〉 ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 ) |
142 | 137, 141 | sylan2 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 ) |
143 | 142, 118 | suppss2 7611 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ⊆ ran (𝐹 supp 0 )) |
144 | 130, 143 | ssfid 8471 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈
Fin) |
145 | 118 | mptexd 6759 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V) |
146 | | isfsupp 8567 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V ∧ 0 ∈ V) → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ↔ (Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈
Fin))) |
147 | 145, 62, 146 | sylancl 580 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ↔ (Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈
Fin))) |
148 | 128, 144,
147 | mpbir2and 703 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ) |
149 | | 2ndconst 7547 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ V → (2nd
↾ ({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗})) |
150 | 119, 149 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2nd ↾
({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗})) |
151 | 41, 42, 44, 118, 126, 148, 150 | gsumf1o 18703 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))))) |
152 | | 1st2nd2 7484 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
153 | | xp1st 7477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st ‘𝑥) ∈ {𝑗}) |
154 | | elsni 4415 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑥) ∈ {𝑗} → (1st ‘𝑥) = 𝑗) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st ‘𝑥) = 𝑗) |
156 | 155 | opeq1d 4642 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈𝑗, (2nd ‘𝑥)〉) |
157 | 152, 156 | eqtrd 2814 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = 〈𝑗, (2nd ‘𝑥)〉) |
158 | 157 | fveq2d 6450 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹‘𝑥) = (𝐹‘〈𝑗, (2nd ‘𝑥)〉)) |
159 | | df-ov 6925 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗𝐹(2nd ‘𝑥)) = (𝐹‘〈𝑗, (2nd ‘𝑥)〉) |
160 | 158, 159 | syl6eqr 2832 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹‘𝑥) = (𝑗𝐹(2nd ‘𝑥))) |
161 | 160 | mpteq2ia 4975 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd ‘𝑥))) |
162 | 50 | feqmptd 6509 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
163 | 162 | reseq1d 5641 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗}))) |
164 | | resss 5671 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ↾ {𝑗}) ⊆ 𝐴 |
165 | | resmpt 5699 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ↾ {𝑗}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥))) |
166 | 164, 165 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥)) |
167 | | ressn 5925 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ↾ {𝑗}) = ({𝑗} × (𝐴 “ {𝑗})) |
168 | 167 | mpteq1i 4974 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥)) |
169 | 166, 168 | eqtri 2802 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥)) |
170 | 163, 169 | syl6eq 2830 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥))) |
171 | | xp2nd 7478 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑗})) |
172 | 171 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗}))) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑗})) |
173 | | fo2nd 7466 |
. . . . . . . . . . . . . . . . . . 19
⊢
2nd :V–onto→V |
174 | | fof 6366 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
175 | 173, 174 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2nd
:V⟶V) |
176 | 175 | feqmptd 6509 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2nd = (𝑥 ∈ V ↦
(2nd ‘𝑥))) |
177 | 176 | reseq1d 5641 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2nd ↾
({𝑗} × (𝐴 “ {𝑗}))) = ((𝑥 ∈ V ↦ (2nd
‘𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗})))) |
178 | | ssv 3844 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑗} × (𝐴 “ {𝑗})) ⊆ V |
179 | | resmpt 5699 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑗} × (𝐴 “ {𝑗})) ⊆ V → ((𝑥 ∈ V ↦ (2nd
‘𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥))) |
180 | 178, 179 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ↦
(2nd ‘𝑥))
↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥)) |
181 | 177, 180 | syl6eq 2830 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd ↾
({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥))) |
182 | | eqidd 2779 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) |
183 | | oveq2 6930 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (2nd ‘𝑥) → (𝑗𝐹𝑘) = (𝑗𝐹(2nd ‘𝑥))) |
184 | 172, 181,
182, 183 | fmptco 6661 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd ‘𝑥)))) |
185 | 161, 170,
184 | 3eqtr4a 2840 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))) |
186 | 185 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))))) |
187 | 151, 186 | eqtr4d 2817 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗})))) |
188 | 116, 187 | chvarv 2361 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) |
189 | 188 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) |
190 | 189 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
191 | 111, 190 | eqtrd 2814 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))) |
192 | 93, 191 | eqeq12d 2793 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))) |
193 | 40, 192 | syl5ibr 238 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
194 | 193 | expcom 404 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
195 | 194 | a2d 29 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) → (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))) |
196 | 17, 24, 31, 38, 39, 195 | findcard2s 8489 |
. 2
⊢ (dom
(𝐹 supp 0 ) ∈ Fin → (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))) |
197 | 4, 196 | mpcom 38 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg
(𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) |