Step | Hyp | Ref
| Expression |
1 | | df-gsum 17181 |
. . 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 767 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → 𝑤 = 𝐺) |
4 | 3 | fveq2d 6796 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺)) |
5 | | gsumval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵) |
7 | 3 | fveq2d 6796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (+g‘𝑤) = (+g‘𝐺)) |
8 | | gsumval.p |
. . . . . . . . . . 11
⊢ + =
(+g‘𝐺) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (+g‘𝑤) = + ) |
10 | 9 | oveqd 7312 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (𝑥(+g‘𝑤)𝑦) = (𝑥 + 𝑦)) |
11 | 10 | eqeq1d 2735 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ((𝑥(+g‘𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦)) |
12 | 9 | oveqd 7312 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (𝑦(+g‘𝑤)𝑥) = (𝑦 + 𝑥)) |
13 | 12 | eqeq1d 2735 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ((𝑦(+g‘𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦)) |
14 | 11, 13 | anbi12d 630 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
15 | 6, 14 | raleqbidv 3338 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
16 | 6, 15 | rabeqbidv 3422 |
. . . . 5
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) |
17 | | gsumval.o |
. . . . . 6
⊢ 𝑂 = {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} |
18 | | oveq2 7303 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦)) |
19 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑦 → 𝑡 = 𝑦) |
20 | 18, 19 | eqeq12d 2749 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦)) |
21 | | oveq1 7302 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠)) |
22 | 21, 19 | eqeq12d 2749 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦)) |
23 | 20, 22 | anbi12d 630 |
. . . . . . . . 9
⊢ (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))) |
24 | 23 | cbvralvw 3385 |
. . . . . . . 8
⊢
(∀𝑡 ∈
𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦 ∈ 𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)) |
25 | | oveq1 7302 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦)) |
26 | 25 | eqeq1d 2735 |
. . . . . . . . 9
⊢ (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦)) |
27 | 26 | ovanraleqv 7319 |
. . . . . . . 8
⊢ (𝑠 = 𝑥 → (∀𝑦 ∈ 𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
28 | 24, 27 | bitrid 282 |
. . . . . . 7
⊢ (𝑠 = 𝑥 → (∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦))) |
29 | 28 | cbvrabv 3428 |
. . . . . 6
⊢ {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} |
30 | 17, 29 | eqtri 2761 |
. . . . 5
⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} |
31 | 16, 30 | eqtr4di 2791 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} = 𝑂) |
32 | 31 | csbeq1d 3838 |
. . 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‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))))))) |
33 | 5 | fvexi 6806 |
. . . . . 6
⊢ 𝐵 ∈ V |
34 | 17, 33 | rabex2 5261 |
. . . . 5
⊢ 𝑂 ∈ V |
35 | 34 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → 𝑂 ∈ V) |
36 | | simplrr 774 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹) |
37 | 36 | rneqd 5850 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹) |
38 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂) |
39 | 37, 38 | sseq12d 3956 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔 ⊆ 𝑜 ↔ ran 𝐹 ⊆ 𝑂)) |
40 | 3 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺) |
41 | 40 | fveq2d 6796 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g‘𝑤) = (0g‘𝐺)) |
42 | | gsumval.z |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
43 | 41, 42 | eqtr4di 2791 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g‘𝑤) = 0 ) |
44 | 36 | dmeqd 5818 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹) |
45 | | gsumvalx.a |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
46 | 45 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴) |
47 | 44, 46 | eqtrd 2773 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴) |
48 | 47 | eleq1d 2818 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...)) |
49 | 47 | eqeq1d 2735 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛))) |
50 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+g‘𝑤) = + ) |
51 | 50 | seqeq2d 13756 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g‘𝑤), 𝑔) = seq𝑚( + , 𝑔)) |
52 | 36 | seqeq3d 13757 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹)) |
53 | 51, 52 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g‘𝑤), 𝑔) = seq𝑚( + , 𝐹)) |
54 | 53 | fveq1d 6794 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+g‘𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛)) |
55 | 54 | eqeq2d 2744 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) |
56 | 49, 55 | anbi12d 630 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
57 | 56 | rexbidv 3169 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
58 | 57 | exbidv 1920 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
59 | 58 | iotabidv 6431 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))) = (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
60 | 38 | difeq2d 4060 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂)) |
61 | 60 | imaeq2d 5970 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝐹 “ (V ∖ 𝑜)) = (◡𝐹 “ (V ∖ 𝑂))) |
62 | 36 | cnveqd 5788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ◡𝑔 = ◡𝐹) |
63 | 62 | imaeq1d 5969 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝑔 “ (V ∖ 𝑜)) = (◡𝐹 “ (V ∖ 𝑜))) |
64 | | gsumval.w |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 = (◡𝐹 “ (V ∖ 𝑂))) |
65 | 64 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (◡𝐹 “ (V ∖ 𝑂))) |
66 | 61, 63, 65 | 3eqtr4d 2783 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝑔 “ (V ∖ 𝑜)) = 𝑊) |
67 | 66 | sbceq1d 3723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))))) |
68 | | gsumvalx.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ 𝑋) |
69 | | cnvexg 7791 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝑋 → ◡𝐹 ∈ V) |
70 | | imaexg 7782 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 ∈ V → (◡𝐹 “ (V ∖ 𝑂)) ∈ V) |
71 | 68, 69, 70 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ (V ∖ 𝑂)) ∈ V) |
72 | 64, 71 | eqeltrd 2834 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ V) |
73 | 72 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V) |
74 | | fveq2 6792 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑊 → (♯‘𝑦) = (♯‘𝑊)) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (♯‘𝑦) = (♯‘𝑊)) |
76 | 75 | oveq2d 7311 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(♯‘𝑦)) = (1...(♯‘𝑊))) |
77 | 76 | f1oeq2d 6730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑦)) |
78 | | f1oeq3 6724 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑊 → (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑦 ↔ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) |
79 | 78 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑦 ↔ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) |
80 | 77, 79 | bitrd 278 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) |
81 | 50 | seqeq2d 13756 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝑔 ∘ 𝑓))) |
82 | 36 | coeq1d 5774 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 ∘ 𝑓) = (𝐹 ∘ 𝑓)) |
83 | 82 | seqeq3d 13757 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓))) |
84 | 81, 83 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓))) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓))) |
86 | 85, 75 | fveq12d 6799 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))) |
87 | 86 | eqeq2d 2744 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))) |
88 | 80, 87 | anbi12d 630 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))) |
89 | 73, 88 | sbcied 3763 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))) |
90 | 67, 89 | bitrd 278 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))) |
91 | 90 | exbidv 1920 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ ∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))) |
92 | 91 | iotabidv 6431 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)))) = (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))) |
93 | 48, 59, 92 | ifbieq12d 4490 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))))) = if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))) |
94 | 39, 43, 93 | ifbieq12d 4490 |
. . . 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( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))))) |
95 | 35, 94 | csbied 3872 |
. . 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( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))))) |
96 | 32, 95 | eqtrd 2773 |
. 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( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))))) |
97 | | gsumval.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
98 | 97 | elexd 3454 |
. 2
⊢ (𝜑 → 𝐺 ∈ V) |
99 | 68 | elexd 3454 |
. 2
⊢ (𝜑 → 𝐹 ∈ V) |
100 | 42 | fvexi 6806 |
. . . 4
⊢ 0 ∈
V |
101 | | iotaex 6420 |
. . . . 5
⊢
(℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V |
102 | | iotaex 6420 |
. . . . 5
⊢
(℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))) ∈ V |
103 | 101, 102 | ifex 4512 |
. . . 4
⊢ if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))) ∈ V |
104 | 100, 103 | ifex 4512 |
. . 3
⊢ if(ran
𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))) ∈ V |
105 | 104 | a1i 11 |
. 2
⊢ (𝜑 → if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))) ∈ V) |
106 | 2, 96, 98, 99, 105 | ovmpod 7445 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))))) |