Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
2 | 1 | mpt2fun 6660 |
. . 3
⊢ Fun
(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) |
4 | | gsum2d2.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ Fin) |
5 | | gsum2d2.f |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) |
6 | 5 | ralrimivva 2954 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵) |
7 | 1 | fmpt2x 7125 |
. . . . 5
⊢
(∀𝑗 ∈
𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
8 | 6, 7 | sylib 207 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
9 | | relxp 5150 |
. . . . . . . 8
⊢ Rel
({𝑗} × 𝐶) |
10 | 9 | rgenw 2908 |
. . . . . . 7
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐶) |
11 | | reliun 5162 |
. . . . . . 7
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐶)) |
12 | 10, 11 | mpbir 220 |
. . . . . 6
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
13 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
14 | 13 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
15 | | elrel 5145 |
. . . . . 6
⊢ ((Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) → ∃𝑗∃𝑘 𝑧 = 〈𝑗, 𝑘〉) |
16 | 12, 14, 15 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ∃𝑗∃𝑘 𝑧 = 〈𝑗, 𝑘〉) |
17 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
18 | | nfiu1 4486 |
. . . . . . . . 9
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
19 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑈 |
20 | 18, 19 | nfdif 3693 |
. . . . . . . 8
⊢
Ⅎ𝑗(∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) |
21 | 20 | nfcri 2745 |
. . . . . . 7
⊢
Ⅎ𝑗 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) |
22 | 17, 21 | nfan 1816 |
. . . . . 6
⊢
Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) |
23 | | nfmpt21 6620 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
24 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑗𝑧 |
25 | 23, 24 | nffv 6110 |
. . . . . . 7
⊢
Ⅎ𝑗((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) |
26 | 25 | nfeq1 2764 |
. . . . . 6
⊢
Ⅎ𝑗((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 |
27 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) |
28 | | nfmpt22 6621 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
29 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝑧 |
30 | 28, 29 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) |
31 | 30 | nfeq1 2764 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 |
32 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑧 = 〈𝑗, 𝑘〉) |
33 | 32 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑗, 𝑘〉)) |
34 | | df-ov 6552 |
. . . . . . . . . 10
⊢ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑗, 𝑘〉) |
35 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) |
36 | 32, 35 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 〈𝑗, 𝑘〉 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) |
37 | 36 | eldifad 3552 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
38 | | opeliunxp 5093 |
. . . . . . . . . . . . 13
⊢
(〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
39 | 37, 38 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
40 | 39 | simpld 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑗 ∈ 𝐴) |
41 | 39 | simprd 478 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑘 ∈ 𝐶) |
42 | 39, 5 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑋 ∈ 𝐵) |
43 | 1 | ovmpt4g 6681 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
44 | 40, 41, 42, 43 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
45 | 34, 44 | syl5eqr 2658 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑗, 𝑘〉) = 𝑋) |
46 | | eldifn 3695 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → ¬ 𝑧 ∈ 𝑈) |
47 | 46 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ¬ 𝑧 ∈ 𝑈) |
48 | 32 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → (𝑧 ∈ 𝑈 ↔ 〈𝑗, 𝑘〉 ∈ 𝑈)) |
49 | | df-br 4584 |
. . . . . . . . . . . . 13
⊢ (𝑗𝑈𝑘 ↔ 〈𝑗, 𝑘〉 ∈ 𝑈) |
50 | 48, 49 | syl6bbr 277 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → (𝑧 ∈ 𝑈 ↔ 𝑗𝑈𝑘)) |
51 | 47, 50 | mtbid 313 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ¬ 𝑗𝑈𝑘) |
52 | 39, 51 | jca 553 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) |
53 | | gsum2d2.n |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) |
54 | 52, 53 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑋 = 0 ) |
55 | 33, 45, 54 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 ) |
56 | 55 | expr 641 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (𝑧 = 〈𝑗, 𝑘〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 )) |
57 | 27, 31, 56 | exlimd 2074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (∃𝑘 𝑧 = 〈𝑗, 𝑘〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 )) |
58 | 22, 26, 57 | exlimd 2074 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (∃𝑗∃𝑘 𝑧 = 〈𝑗, 𝑘〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 )) |
59 | 16, 58 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 ) |
60 | 8, 59 | suppss 7212 |
. . 3
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ⊆ 𝑈) |
61 | | ssfi 8065 |
. . 3
⊢ ((𝑈 ∈ Fin ∧ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ⊆ 𝑈) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈
Fin) |
62 | 4, 60, 61 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈
Fin) |
63 | | gsum2d2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
64 | | gsum2d2.r |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) |
65 | 64 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐶 ∈ 𝑊) |
66 | 1 | mpt2exxg 7133 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 𝐶 ∈ 𝑊) → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V) |
67 | 63, 65, 66 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V) |
68 | | gsum2d2.z |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
69 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝐺) ∈ V |
70 | 68, 69 | eqeltri 2684 |
. . . 4
⊢ 0 ∈
V |
71 | 70 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
72 | | isfsupp 8162 |
. . 3
⊢ (((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V ∧ 0 ∈ V) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∧ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈
Fin))) |
73 | 67, 71, 72 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∧ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈
Fin))) |
74 | 3, 62, 73 | mpbir2and 959 |
1
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ) |