Step | Hyp | Ref
| Expression |
1 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (𝑦 + 𝑥) = ( 0 + 𝑥)) |
2 | 1 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑦 = 0 → ((𝑦 + 𝑥) = 𝑥 ↔ ( 0 + 𝑥) = 𝑥)) |
3 | 2 | ovanraleqv 7237 |
. . . . . . . 8
⊢ (𝑦 = 0 → (∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
4 | | gsumress.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
5 | | gsumress.z |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝑆) |
6 | 4, 5 | sseldd 3902 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ 𝐵) |
7 | | gsumress.c |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
8 | 7 | ralrimiva 3105 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
9 | 3, 6, 8 | elrabd 3604 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
10 | 9 | snssd 4722 |
. . . . . 6
⊢ (𝜑 → { 0 } ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
11 | | gsumress.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
12 | | gsumress.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
13 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
14 | | gsumress.o |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
15 | | eqid 2737 |
. . . . . . . . 9
⊢ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} |
16 | 12, 13, 14, 15 | mgmidsssn0 18144 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝑉 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ {(0g‘𝐺)}) |
17 | 11, 16 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ {(0g‘𝐺)}) |
18 | 17, 9 | sseldd 3902 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
{(0g‘𝐺)}) |
19 | | elsni 4558 |
. . . . . . . . 9
⊢ ( 0 ∈
{(0g‘𝐺)}
→ 0
= (0g‘𝐺)) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 =
(0g‘𝐺)) |
21 | 20 | sneqd 4553 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝐺)}) |
22 | 17, 21 | sseqtrrd 3942 |
. . . . . 6
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ { 0 }) |
23 | 10, 22 | eqssd 3918 |
. . . . 5
⊢ (𝜑 → { 0 } = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
24 | 2 | ovanraleqv 7237 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ 𝑆 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
25 | 4 | sselda 3901 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
26 | 25, 7 | syldan 594 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
27 | 26 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
28 | 24, 5, 27 | elrabd 3604 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ {𝑦 ∈ 𝑆 ∣ ∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
29 | | gsumress.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
30 | 29, 12 | ressbas2 16791 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘𝐻)) |
31 | 4, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 = (Base‘𝐻)) |
32 | | fvex 6730 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝐻)
∈ V |
33 | 31, 32 | eqeltrdi 2846 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ V) |
34 | 29, 14 | ressplusg 16834 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ V → + =
(+g‘𝐻)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → + =
(+g‘𝐻)) |
36 | 35 | oveqd 7230 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 + 𝑥) = (𝑦(+g‘𝐻)𝑥)) |
37 | 36 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 + 𝑥) = 𝑥 ↔ (𝑦(+g‘𝐻)𝑥) = 𝑥)) |
38 | 35 | oveqd 7230 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 + 𝑦) = (𝑥(+g‘𝐻)𝑦)) |
39 | 38 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 + 𝑦) = 𝑥 ↔ (𝑥(+g‘𝐻)𝑦) = 𝑥)) |
40 | 37, 39 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥))) |
41 | 31, 40 | raleqbidv 3313 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥))) |
42 | 31, 41 | rabeqbidv 3396 |
. . . . . . . 8
⊢ (𝜑 → {𝑦 ∈ 𝑆 ∣ ∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
43 | 28, 42 | eleqtrd 2840 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
44 | 43 | snssd 4722 |
. . . . . 6
⊢ (𝜑 → { 0 } ⊆ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
45 | 29 | ovexi 7247 |
. . . . . . . . 9
⊢ 𝐻 ∈ V |
46 | 45 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ V) |
47 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐻) =
(Base‘𝐻) |
48 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝐻) = (0g‘𝐻) |
49 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝐻) = (+g‘𝐻) |
50 | | eqid 2737 |
. . . . . . . . 9
⊢ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} |
51 | 47, 48, 49, 50 | mgmidsssn0 18144 |
. . . . . . . 8
⊢ (𝐻 ∈ V → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ {(0g‘𝐻)}) |
52 | 46, 51 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ {(0g‘𝐻)}) |
53 | 52, 43 | sseldd 3902 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
{(0g‘𝐻)}) |
54 | | elsni 4558 |
. . . . . . . . 9
⊢ ( 0 ∈
{(0g‘𝐻)}
→ 0
= (0g‘𝐻)) |
55 | 53, 54 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 =
(0g‘𝐻)) |
56 | 55 | sneqd 4553 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝐻)}) |
57 | 52, 56 | sseqtrrd 3942 |
. . . . . 6
⊢ (𝜑 → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ { 0 }) |
58 | 44, 57 | eqssd 3918 |
. . . . 5
⊢ (𝜑 → { 0 } = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
59 | 23, 58 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
60 | 59 | sseq2d 3933 |
. . 3
⊢ (𝜑 → (ran 𝐹 ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ↔ ran 𝐹 ⊆ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)})) |
61 | 20, 55 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
62 | 35 | seqeq2d 13581 |
. . . . . . . . . 10
⊢ (𝜑 → seq𝑚( + , 𝐹) = seq𝑚((+g‘𝐻), 𝐹)) |
63 | 62 | fveq1d 6719 |
. . . . . . . . 9
⊢ (𝜑 → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)) |
64 | 63 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) ↔ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))) |
65 | 64 | anbi2d 632 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
66 | 65 | rexbidv 3216 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
67 | 66 | exbidv 1929 |
. . . . 5
⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
68 | 67 | iotabidv 6364 |
. . . 4
⊢ (𝜑 → (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))) = (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
69 | 35 | seqeq2d 13581 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , (𝐹 ∘ 𝑓)) = seq1((+g‘𝐻), (𝐹 ∘ 𝑓))) |
70 | 69 | fveq1d 6719 |
. . . . . . . 8
⊢ (𝜑 → (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))) =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) |
71 | 70 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝜑 → (𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))) ↔ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))))) |
72 | 71 | anbi2d 632 |
. . . . . 6
⊢ (𝜑 → ((𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) ↔ (𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))))) |
73 | 72 | exbidv 1929 |
. . . . 5
⊢ (𝜑 → (∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) ↔ ∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))))) |
74 | 73 | iotabidv 6364 |
. . . 4
⊢ (𝜑 → (℩𝑧∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))))) = (℩𝑧∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))))) |
75 | 68, 74 | ifeq12d 4460 |
. . 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 })))))))) |
76 | 60, 61, 75 | ifbieq12d 4467 |
. 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
}))))))))) |
77 | 23 | difeq2d 4037 |
. . . 4
⊢ (𝜑 → (V ∖ { 0 }) = (V
∖ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)})) |
78 | 77 | imaeq2d 5929 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) = (◡𝐹 “ (V ∖ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}))) |
79 | | gsumress.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
80 | | gsumress.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
81 | 80, 4 | fssd 6563 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
82 | 12, 13, 14, 15, 78, 11, 79, 81 | gsumval 18149 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}, (0g‘𝐺), if(𝐴 ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0
}))))))))) |
83 | 58 | difeq2d 4037 |
. . . 4
⊢ (𝜑 → (V ∖ { 0 }) = (V
∖ {𝑦 ∈
(Base‘𝐻) ∣
∀𝑥 ∈
(Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)})) |
84 | 83 | imaeq2d 5929 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) = (◡𝐹 “ (V ∖ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}))) |
85 | 31 | feq3d 6532 |
. . . 4
⊢ (𝜑 → (𝐹:𝐴⟶𝑆 ↔ 𝐹:𝐴⟶(Base‘𝐻))) |
86 | 80, 85 | mpbid 235 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐻)) |
87 | 47, 48, 49, 50, 84, 46, 79, 86 | gsumval 18149 |
. 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
}))))))))) |
88 | 76, 82, 87 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) |