Step | Hyp | Ref
| Expression |
1 | | gsumress.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
2 | | gsumress.z |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝑆) |
3 | 1, 2 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ 𝐵) |
4 | | gsumress.c |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
5 | 4 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
6 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0 → (𝑦 + 𝑥) = ( 0 + 𝑥)) |
7 | 6 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → ((𝑦 + 𝑥) = 𝑥 ↔ ( 0 + 𝑥) = 𝑥)) |
8 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0 → (𝑥 + 𝑦) = (𝑥 + 0 )) |
9 | 8 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → ((𝑥 + 𝑦) = 𝑥 ↔ (𝑥 + 0 ) = 𝑥)) |
10 | 7, 9 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
11 | 10 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
12 | 11 | elrab 3331 |
. . . . . . . 8
⊢ ( 0 ∈ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ↔ ( 0 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
13 | 3, 5, 12 | sylanbrc 695 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
14 | 13 | snssd 4281 |
. . . . . 6
⊢ (𝜑 → { 0 } ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
15 | | gsumress.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
16 | | gsumress.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
17 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
18 | | gsumress.o |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
19 | | eqid 2610 |
. . . . . . . . 9
⊢ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} |
20 | 16, 17, 18, 19 | mgmidsssn0 17092 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝑉 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ {(0g‘𝐺)}) |
21 | 15, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ {(0g‘𝐺)}) |
22 | 21, 13 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
{(0g‘𝐺)}) |
23 | | elsni 4142 |
. . . . . . . . 9
⊢ ( 0 ∈
{(0g‘𝐺)}
→ 0
= (0g‘𝐺)) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 =
(0g‘𝐺)) |
25 | 24 | sneqd 4137 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝐺)}) |
26 | 21, 25 | sseqtr4d 3605 |
. . . . . 6
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ { 0 }) |
27 | 14, 26 | eqssd 3585 |
. . . . 5
⊢ (𝜑 → { 0 } = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
28 | 1 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
29 | 28, 4 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
30 | 29 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
31 | 10 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ 𝑆 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
32 | 31 | elrab 3331 |
. . . . . . . . 9
⊢ ( 0 ∈ {𝑦 ∈ 𝑆 ∣ ∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ↔ ( 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
33 | 2, 30, 32 | sylanbrc 695 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ {𝑦 ∈ 𝑆 ∣ ∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
34 | | gsumress.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
35 | 34, 16 | ressbas2 15758 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘𝐻)) |
36 | 1, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 = (Base‘𝐻)) |
37 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝐻)
∈ V |
38 | 36, 37 | syl6eqel 2696 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ V) |
39 | 34, 18 | ressplusg 15818 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ V → + =
(+g‘𝐻)) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → + =
(+g‘𝐻)) |
41 | 40 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 + 𝑥) = (𝑦(+g‘𝐻)𝑥)) |
42 | 41 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 + 𝑥) = 𝑥 ↔ (𝑦(+g‘𝐻)𝑥) = 𝑥)) |
43 | 40 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 + 𝑦) = (𝑥(+g‘𝐻)𝑦)) |
44 | 43 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 + 𝑦) = 𝑥 ↔ (𝑥(+g‘𝐻)𝑦) = 𝑥)) |
45 | 42, 44 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥))) |
46 | 36, 45 | raleqbidv 3129 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥))) |
47 | 36, 46 | rabeqbidv 3168 |
. . . . . . . 8
⊢ (𝜑 → {𝑦 ∈ 𝑆 ∣ ∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
48 | 33, 47 | eleqtrd 2690 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
49 | 48 | snssd 4281 |
. . . . . 6
⊢ (𝜑 → { 0 } ⊆ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
50 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐺 ↾s 𝑆) ∈ V |
51 | 34, 50 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐻 ∈ V |
52 | 51 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ V) |
53 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝐻) =
(Base‘𝐻) |
54 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐻) = (0g‘𝐻) |
55 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝐻) = (+g‘𝐻) |
56 | | eqid 2610 |
. . . . . . . . 9
⊢ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} |
57 | 53, 54, 55, 56 | mgmidsssn0 17092 |
. . . . . . . 8
⊢ (𝐻 ∈ V → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ {(0g‘𝐻)}) |
58 | 52, 57 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ {(0g‘𝐻)}) |
59 | 58, 48 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
{(0g‘𝐻)}) |
60 | | elsni 4142 |
. . . . . . . . 9
⊢ ( 0 ∈
{(0g‘𝐻)}
→ 0
= (0g‘𝐻)) |
61 | 59, 60 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 =
(0g‘𝐻)) |
62 | 61 | sneqd 4137 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝐻)}) |
63 | 58, 62 | sseqtr4d 3605 |
. . . . . 6
⊢ (𝜑 → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ { 0 }) |
64 | 49, 63 | eqssd 3585 |
. . . . 5
⊢ (𝜑 → { 0 } = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
65 | 27, 64 | eqtr3d 2646 |
. . . 4
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
66 | 65 | sseq2d 3596 |
. . 3
⊢ (𝜑 → (ran 𝐹 ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ↔ ran 𝐹 ⊆ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)})) |
67 | 24, 61 | eqtr3d 2646 |
. . 3
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
68 | 40 | seqeq2d 12670 |
. . . . . . . . . 10
⊢ (𝜑 → seq𝑚( + , 𝐹) = seq𝑚((+g‘𝐻), 𝐹)) |
69 | 68 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝜑 → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)) |
70 | 69 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) ↔ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))) |
71 | 70 | anbi2d 736 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
72 | 71 | rexbidv 3034 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
73 | 72 | exbidv 1837 |
. . . . 5
⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
74 | 73 | iotabidv 5789 |
. . . 4
⊢ (𝜑 → (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))) = (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
75 | 40 | seqeq2d 12670 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , (𝐹 ∘ 𝑓)) = seq1((+g‘𝐻), (𝐹 ∘ 𝑓))) |
76 | 75 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝜑 → (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 })))) =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))) |
77 | 76 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝜑 → (𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 })))) ↔ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 })))))) |
78 | 77 | anbi2d 736 |
. . . . . 6
⊢ (𝜑 → ((𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))) ↔ (𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))))) |
79 | 78 | exbidv 1837 |
. . . . 5
⊢ (𝜑 → (∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))) ↔ ∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))))) |
80 | 79 | iotabidv 5789 |
. . . 4
⊢ (𝜑 → (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 })))))) = (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))))) |
81 | 74, 80 | ifeq12d 4056 |
. . 3
⊢ (𝜑 → if(𝐴 ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 }))))))) = if(𝐴 ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 })))))))) |
82 | 66, 67, 81 | ifbieq12d 4063 |
. 2
⊢ (𝜑 → if(ran 𝐹 ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}, (0g‘𝐺), if(𝐴 ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0 })))))))) = if(ran 𝐹 ⊆ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}, (0g‘𝐻), if(𝐴 ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0
}))))))))) |
83 | 27 | difeq2d 3690 |
. . . 4
⊢ (𝜑 → (V ∖ { 0 }) = (V
∖ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)})) |
84 | 83 | imaeq2d 5385 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) = (◡𝐹 “ (V ∖ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}))) |
85 | | gsumress.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
86 | | gsumress.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
87 | 86, 1 | fssd 5970 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
88 | 16, 17, 18, 19, 84, 15, 85, 87 | gsumval 17094 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}, (0g‘𝐺), if(𝐴 ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0
}))))))))) |
89 | 64 | difeq2d 3690 |
. . . 4
⊢ (𝜑 → (V ∖ { 0 }) = (V
∖ {𝑦 ∈
(Base‘𝐻) ∣
∀𝑥 ∈
(Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)})) |
90 | 89 | imaeq2d 5385 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) = (◡𝐹 “ (V ∖ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}))) |
91 | 36 | feq3d 5945 |
. . . 4
⊢ (𝜑 → (𝐹:𝐴⟶𝑆 ↔ 𝐹:𝐴⟶(Base‘𝐻))) |
92 | 86, 91 | mpbid 221 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐻)) |
93 | 53, 54, 55, 56, 90, 52, 85, 92 | gsumval 17094 |
. 2
⊢ (𝜑 → (𝐻 Σg 𝐹) = if(ran 𝐹 ⊆ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}, (0g‘𝐻), if(𝐴 ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ { 0
}))))))))) |
94 | 82, 88, 93 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) |