Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
2 | 1 | mpofun 7284 |
. . 3
⊢ Fun
(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) |
4 | | gsum2d2.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ Fin) |
5 | | gsum2d2.f |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) |
6 | 5 | ralrimivva 3103 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵) |
7 | 1 | fmpox 7783 |
. . . . 5
⊢
(∀𝑗 ∈
𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
8 | 6, 7 | sylib 221 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
9 | | nfv 1920 |
. . . . . 6
⊢
Ⅎ𝑗𝜑 |
10 | | nfiu1 4912 |
. . . . . . . 8
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
11 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑗𝑈 |
12 | 10, 11 | nfdif 4014 |
. . . . . . 7
⊢
Ⅎ𝑗(∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) |
13 | 12 | nfcri 2886 |
. . . . . 6
⊢
Ⅎ𝑗 𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) |
14 | 9, 13 | nfan 1905 |
. . . . 5
⊢
Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) |
15 | | nfmpo1 7242 |
. . . . . . 7
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
16 | | nfcv 2899 |
. . . . . . 7
⊢
Ⅎ𝑗𝑧 |
17 | 15, 16 | nffv 6678 |
. . . . . 6
⊢
Ⅎ𝑗((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) |
18 | 17 | nfeq1 2914 |
. . . . 5
⊢
Ⅎ𝑗((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 |
19 | | relxp 5537 |
. . . . . . . 8
⊢ Rel
({𝑗} × 𝐶) |
20 | 19 | rgenw 3065 |
. . . . . . 7
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐶) |
21 | | reliun 5654 |
. . . . . . 7
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐶)) |
22 | 20, 21 | mpbir 234 |
. . . . . 6
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
23 | | eldifi 4015 |
. . . . . . 7
⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
24 | 23 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
25 | | elrel 5636 |
. . . . . 6
⊢ ((Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) → ∃𝑗∃𝑘 𝑧 = 〈𝑗, 𝑘〉) |
26 | 22, 24, 25 | sylancr 590 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ∃𝑗∃𝑘 𝑧 = 〈𝑗, 𝑘〉) |
27 | | nfv 1920 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) |
28 | | nfmpo2 7243 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
29 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑧 |
30 | 28, 29 | nffv 6678 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) |
31 | 30 | nfeq1 2914 |
. . . . . 6
⊢
Ⅎ𝑘((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 |
32 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑧 = 〈𝑗, 𝑘〉) |
33 | 32 | fveq2d 6672 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑗, 𝑘〉)) |
34 | | df-ov 7167 |
. . . . . . . . 9
⊢ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑗, 𝑘〉) |
35 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) |
36 | 32, 35 | eqeltrrd 2834 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 〈𝑗, 𝑘〉 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) |
37 | 36 | eldifad 3853 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
38 | | opeliunxp 5584 |
. . . . . . . . . . . 12
⊢
(〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
39 | 37, 38 | sylib 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
40 | 39 | simpld 498 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑗 ∈ 𝐴) |
41 | 39 | simprd 499 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑘 ∈ 𝐶) |
42 | 39, 5 | syldan 594 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑋 ∈ 𝐵) |
43 | 1 | ovmpt4g 7306 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
44 | 40, 41, 42, 43 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
45 | 34, 44 | eqtr3id 2787 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑗, 𝑘〉) = 𝑋) |
46 | | eldifn 4016 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → ¬ 𝑧 ∈ 𝑈) |
47 | 46 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ¬ 𝑧 ∈ 𝑈) |
48 | 32 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → (𝑧 ∈ 𝑈 ↔ 〈𝑗, 𝑘〉 ∈ 𝑈)) |
49 | | df-br 5028 |
. . . . . . . . . . . 12
⊢ (𝑗𝑈𝑘 ↔ 〈𝑗, 𝑘〉 ∈ 𝑈) |
50 | 48, 49 | bitr4di 292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → (𝑧 ∈ 𝑈 ↔ 𝑗𝑈𝑘)) |
51 | 47, 50 | mtbid 327 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ¬ 𝑗𝑈𝑘) |
52 | 39, 51 | jca 515 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) |
53 | | gsum2d2.n |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) |
54 | 52, 53 | syldan 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → 𝑋 = 0 ) |
55 | 33, 45, 54 | 3eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = 〈𝑗, 𝑘〉)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 ) |
56 | 55 | expr 460 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (𝑧 = 〈𝑗, 𝑘〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 )) |
57 | 27, 31, 56 | exlimd 2219 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (∃𝑘 𝑧 = 〈𝑗, 𝑘〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 )) |
58 | 14, 18, 26, 57 | exlimimdd 2220 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑧) = 0 ) |
59 | 8, 58 | suppss 7882 |
. . 3
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ⊆ 𝑈) |
60 | 4, 59 | ssfid 8812 |
. 2
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈
Fin) |
61 | | gsum2d2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
62 | | gsum2d2.r |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) |
63 | 62 | ralrimiva 3096 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐶 ∈ 𝑊) |
64 | 1 | mpoexxg 7792 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 𝐶 ∈ 𝑊) → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V) |
65 | 61, 63, 64 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V) |
66 | | gsum2d2.z |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
67 | 66 | fvexi 6682 |
. . . 4
⊢ 0 ∈
V |
68 | 67 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
69 | | isfsupp 8903 |
. . 3
⊢ (((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∈ V ∧ 0 ∈ V) → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∧ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈
Fin))) |
70 | 65, 68, 69 | syl2anc 587 |
. 2
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ↔ (Fun (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∧ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) supp 0 ) ∈
Fin))) |
71 | 3, 60, 70 | mpbir2and 713 |
1
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ) |