Step | Hyp | Ref
| Expression |
1 | | df-gsum 15926 |
. . 3
⊢
Σg = (𝑤 ∈ V, 𝑔 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))))))) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → Σg
= (𝑤 ∈ V, 𝑔 ∈ V ↦
⦋{𝑥 ∈
(Base‘𝑤) ∣
∀𝑦 ∈
(Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))))))) |
3 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → 𝑤 = 𝐺) |
4 | 3 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺)) |
5 | | gsumval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
6 | 4, 5 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵) |
7 | 3 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (+g‘𝑤) = (+g‘𝐺)) |
8 | | gsumval.p |
. . . . . . . . . . 11
⊢ + =
(+g‘𝐺) |
9 | 7, 8 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (+g‘𝑤) = + ) |
10 | 9 | oveqd 6566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (𝑥(+g‘𝑤)𝑦) = (𝑥 + 𝑦)) |
11 | 10 | eqeq1d 2612 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ((𝑥(+g‘𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦)) |
12 | 9 | oveqd 6566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (𝑦(+g‘𝑤)𝑥) = (𝑦 + 𝑥)) |
13 | 12 | eqeq1d 2612 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ((𝑦(+g‘𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦)) |
14 | 11, 13 | anbi12d 743 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
15 | 6, 14 | raleqbidv 3129 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
16 | 6, 15 | rabeqbidv 3168 |
. . . . 5
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) |
17 | | gsumval.o |
. . . . . 6
⊢ 𝑂 = {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} |
18 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦)) |
19 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑦 → 𝑡 = 𝑦) |
20 | 18, 19 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦)) |
21 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠)) |
22 | 21, 19 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦)) |
23 | 20, 22 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))) |
24 | 23 | cbvralv 3147 |
. . . . . . . 8
⊢
(∀𝑡 ∈
𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦 ∈ 𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)) |
25 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦)) |
26 | 25 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦)) |
27 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑥 → (𝑦 + 𝑠) = (𝑦 + 𝑥)) |
28 | 27 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → ((𝑦 + 𝑠) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦)) |
29 | 26, 28 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑠 = 𝑥 → (((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
30 | 29 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑠 = 𝑥 → (∀𝑦 ∈ 𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
31 | 24, 30 | syl5bb 271 |
. . . . . . 7
⊢ (𝑠 = 𝑥 → (∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
32 | 31 | cbvrabv 3172 |
. . . . . 6
⊢ {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} |
33 | 17, 32 | eqtri 2632 |
. . . . 5
⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} |
34 | 16, 33 | syl6eqr 2662 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} = 𝑂) |
35 | 34 | csbeq1d 3506 |
. . 3
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))))) = ⦋𝑂 / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))))))) |
36 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
37 | 5, 36 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
38 | 17, 37 | rabex2 4742 |
. . . . 5
⊢ 𝑂 ∈ V |
39 | 38 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → 𝑂 ∈ V) |
40 | | simplrr 797 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹) |
41 | 40 | rneqd 5274 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹) |
42 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂) |
43 | 41, 42 | sseq12d 3597 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔 ⊆ 𝑜 ↔ ran 𝐹 ⊆ 𝑂)) |
44 | 3 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺) |
45 | 44 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g‘𝑤) = (0g‘𝐺)) |
46 | | gsumval.z |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
47 | 45, 46 | syl6eqr 2662 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g‘𝑤) = 0 ) |
48 | 40 | dmeqd 5248 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹) |
49 | | gsumvalx.a |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
50 | 49 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴) |
51 | 48, 50 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴) |
52 | 51 | eleq1d 2672 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...)) |
53 | 51 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛))) |
54 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+g‘𝑤) = + ) |
55 | 54 | seqeq2d 12670 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g‘𝑤), 𝑔) = seq𝑚( + , 𝑔)) |
56 | 40 | seqeq3d 12671 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹)) |
57 | 55, 56 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g‘𝑤), 𝑔) = seq𝑚( + , 𝐹)) |
58 | 57 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+g‘𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛)) |
59 | 58 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) |
60 | 53, 59 | anbi12d 743 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
61 | 60 | rexbidv 3034 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
62 | 61 | exbidv 1837 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
63 | 62 | iotabidv 5789 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))) = (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
64 | 42 | difeq2d 3690 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂)) |
65 | 64 | imaeq2d 5385 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝐹 “ (V ∖ 𝑜)) = (◡𝐹 “ (V ∖ 𝑂))) |
66 | 40 | cnveqd 5220 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ◡𝑔 = ◡𝐹) |
67 | 66 | imaeq1d 5384 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝑔 “ (V ∖ 𝑜)) = (◡𝐹 “ (V ∖ 𝑜))) |
68 | | gsumval.w |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 = (◡𝐹 “ (V ∖ 𝑂))) |
69 | 68 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (◡𝐹 “ (V ∖ 𝑂))) |
70 | 65, 67, 69 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝑔 “ (V ∖ 𝑜)) = 𝑊) |
71 | 70 | sbceq1d 3407 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))))) |
72 | | gsumvalx.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ 𝑋) |
73 | | cnvexg 7005 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝑋 → ◡𝐹 ∈ V) |
74 | | imaexg 6995 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 ∈ V → (◡𝐹 “ (V ∖ 𝑂)) ∈ V) |
75 | 72, 73, 74 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ (V ∖ 𝑂)) ∈ V) |
76 | 68, 75 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ V) |
77 | 76 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V) |
78 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑊 → (#‘𝑦) = (#‘𝑊)) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (#‘𝑦) = (#‘𝑊)) |
80 | 79 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(#‘𝑦)) = (1...(#‘𝑊))) |
81 | | f1oeq2 6041 |
. . . . . . . . . . . . 13
⊢
((1...(#‘𝑦)) =
(1...(#‘𝑊)) →
(𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑦)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑦)) |
83 | | f1oeq3 6042 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑊 → (𝑓:(1...(#‘𝑊))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) |
84 | 83 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑊))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) |
85 | 82, 84 | bitrd 267 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) |
86 | 54 | seqeq2d 12670 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝑔 ∘ 𝑓))) |
87 | 40 | coeq1d 5205 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 ∘ 𝑓) = (𝐹 ∘ 𝑓)) |
88 | 87 | seqeq3d 12671 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓))) |
89 | 86, 88 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓))) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓))) |
91 | 90, 79 | fveq12d 6109 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)) = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) |
92 | 91 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))) |
93 | 85, 92 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))) |
94 | 77, 93 | sbcied 3439 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))) |
95 | 71, 94 | bitrd 267 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))) |
96 | 95 | exbidv 1837 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ ∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))) |
97 | 96 | iotabidv 5789 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))) = (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))) |
98 | 52, 63, 97 | ifbieq12d 4063 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))))) = if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))) |
99 | 43, 47, 98 | ifbieq12d 4063 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(ran 𝑔 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))))) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))))) |
100 | 39, 99 | csbied 3526 |
. . 3
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ⦋𝑂 / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))))) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))))) |
101 | 35, 100 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))))) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))))) |
102 | | gsumval.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
103 | 102 | elexd 3187 |
. 2
⊢ (𝜑 → 𝐺 ∈ V) |
104 | 72 | elexd 3187 |
. 2
⊢ (𝜑 → 𝐹 ∈ V) |
105 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝐺) ∈ V |
106 | 46, 105 | eqeltri 2684 |
. . . 4
⊢ 0 ∈
V |
107 | | iotaex 5785 |
. . . . 5
⊢
(℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V |
108 | | iotaex 5785 |
. . . . 5
⊢
(℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))) ∈ V |
109 | 107, 108 | ifex 4106 |
. . . 4
⊢ if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))) ∈ V |
110 | 106, 109 | ifex 4106 |
. . 3
⊢ if(ran
𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))) ∈ V |
111 | 110 | a1i 11 |
. 2
⊢ (𝜑 → if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))) ∈ V) |
112 | 2, 101, 103, 104, 111 | ovmpt2d 6686 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))))) |