Step | Hyp | Ref
| Expression |
1 | | gsum2d2.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
2 | | gsum2d2.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
3 | | gsum2d2.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ CMnd) |
4 | | gsum2d2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | snex 5324 |
. . . . . 6
⊢ {𝑗} ∈ V |
6 | | gsum2d2.r |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) |
7 | | xpexg 7535 |
. . . . . 6
⊢ (({𝑗} ∈ V ∧ 𝐶 ∈ 𝑊) → ({𝑗} × 𝐶) ∈ V) |
8 | 5, 6, 7 | sylancr 590 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐶) ∈ V) |
9 | 8 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
10 | | iunexg 7736 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
11 | 4, 9, 10 | syl2anc 587 |
. . 3
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
12 | | relxp 5569 |
. . . . . 6
⊢ Rel
({𝑗} × 𝐶) |
13 | 12 | rgenw 3073 |
. . . . 5
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐶) |
14 | | reliun 5686 |
. . . . 5
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐶)) |
15 | 13, 14 | mpbir 234 |
. . . 4
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
16 | 15 | a1i 11 |
. . 3
⊢ (𝜑 → Rel ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
17 | | vex 3412 |
. . . . . 6
⊢ 𝑥 ∈ V |
18 | 17 | eldm2 5770 |
. . . . 5
⊢ (𝑥 ∈ dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
19 | | eliunxp 5706 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))) |
20 | | vex 3412 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
21 | 17, 20 | opth1 5359 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 → 𝑥 = 𝑗) |
22 | 21 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))) → 𝑥 = 𝑗) |
23 | | simprrl 781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))) → 𝑗 ∈ 𝐴) |
24 | 22, 23 | eqeltrd 2838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))) → 𝑥 ∈ 𝐴) |
25 | 24 | ex 416 |
. . . . . . . 8
⊢ (𝜑 → ((〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑥 ∈ 𝐴)) |
26 | 25 | exlimdvv 1942 |
. . . . . . 7
⊢ (𝜑 → (∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑥 ∈ 𝐴)) |
27 | 19, 26 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) → 𝑥 ∈ 𝐴)) |
28 | 27 | exlimdv 1941 |
. . . . 5
⊢ (𝜑 → (∃𝑦〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) → 𝑥 ∈ 𝐴)) |
29 | 18, 28 | syl5bi 245 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) → 𝑥 ∈ 𝐴)) |
30 | 29 | ssrdv 3907 |
. . 3
⊢ (𝜑 → dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ⊆ 𝐴) |
31 | | gsum2d2.f |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) |
32 | 31 | ralrimivva 3112 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵) |
33 | | eqid 2737 |
. . . . 5
⊢ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
34 | 33 | fmpox 7837 |
. . . 4
⊢
(∀𝑗 ∈
𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
35 | 32, 34 | sylib 221 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
36 | | gsum2d2.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ Fin) |
37 | | gsum2d2.n |
. . . 4
⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) |
38 | 1, 2, 3, 4, 6, 31,
36, 37 | gsum2d2lem 19358 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ) |
39 | 1, 2, 3, 11, 16, 4, 30, 35, 38 | gsum2d 19357 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))))) |
40 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑗𝐺 |
41 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑗
Σg |
42 | | nfiu1 4938 |
. . . . . . . 8
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
43 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑗{𝑚} |
44 | 42, 43 | nfima 5937 |
. . . . . . 7
⊢
Ⅎ𝑗(∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) |
45 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑗𝑚 |
46 | | nfmpo1 7291 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
47 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑗𝑛 |
48 | 45, 46, 47 | nfov 7243 |
. . . . . . 7
⊢
Ⅎ𝑗(𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛) |
49 | 44, 48 | nfmpt 5152 |
. . . . . 6
⊢
Ⅎ𝑗(𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) |
50 | 40, 41, 49 | nfov 7243 |
. . . . 5
⊢
Ⅎ𝑗(𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) |
51 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑚(𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) |
52 | | sneq 4551 |
. . . . . . . 8
⊢ (𝑚 = 𝑗 → {𝑚} = {𝑗}) |
53 | 52 | imaeq2d 5929 |
. . . . . . 7
⊢ (𝑚 = 𝑗 → (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) = (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗})) |
54 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑚 = 𝑗 → (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛) = (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) |
55 | 53, 54 | mpteq12dv 5140 |
. . . . . 6
⊢ (𝑚 = 𝑗 → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) |
56 | 55 | oveq2d 7229 |
. . . . 5
⊢ (𝑚 = 𝑗 → (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) = (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) |
57 | 50, 51, 56 | cbvmpt 5156 |
. . . 4
⊢ (𝑚 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) = (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) |
58 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑗 ∈ V |
59 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑘 ∈ V |
60 | 58, 59 | elimasn 5957 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↔ 〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
61 | | opeliunxp 5616 |
. . . . . . . . . . . . 13
⊢
(〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
62 | 60, 61 | bitri 278 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
63 | 62 | baib 539 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝐴 → (𝑘 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↔ 𝑘 ∈ 𝐶)) |
64 | 63 | eqrdv 2735 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝐴 → (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) = 𝐶) |
65 | 64 | mpteq1d 5144 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝐴 → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) |
66 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑗 |
67 | | nfmpo2 7292 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
68 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑛 |
69 | 66, 67, 68 | nfov 7243 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛) |
70 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) |
71 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛) = (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) |
72 | 69, 70, 71 | cbvmpt 5156 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑘 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) |
73 | 65, 72 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐴 → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑘 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘))) |
74 | 73 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑘 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘))) |
75 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑗 ∈ 𝐴) |
76 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑘 ∈ 𝐶) |
77 | 33 | ovmpt4g 7356 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
78 | 75, 76, 31, 77 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
79 | 78 | anassrs 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
80 | 79 | mpteq2dva 5150 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) = (𝑘 ∈ 𝐶 ↦ 𝑋)) |
81 | 74, 80 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑘 ∈ 𝐶 ↦ 𝑋)) |
82 | 81 | oveq2d 7229 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) = (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋))) |
83 | 82 | mpteq2dva 5150 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) = (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))) |
84 | 57, 83 | syl5eq 2790 |
. . 3
⊢ (𝜑 → (𝑚 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) = (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))) |
85 | 84 | oveq2d 7229 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))))) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋))))) |
86 | 39, 85 | eqtrd 2777 |
1
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋))))) |