| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (𝑦 + 𝑥) = ( 0 + 𝑥)) |
| 2 | 1 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑦 = 0 → ((𝑦 + 𝑥) = 𝑥 ↔ ( 0 + 𝑥) = 𝑥)) |
| 3 | 2 | ovanraleqv 7455 |
. . . . . . . 8
⊢ (𝑦 = 0 → (∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
| 4 | | gsumress.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
| 5 | | gsumress.z |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝑆) |
| 6 | 4, 5 | sseldd 3984 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ 𝐵) |
| 7 | | gsumress.c |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
| 8 | 7 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
| 9 | 3, 6, 8 | elrabd 3694 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
| 10 | 9 | snssd 4809 |
. . . . . 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 18685 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝑉 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ {(0g‘𝐺)}) |
| 17 | 11, 16 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ {(0g‘𝐺)}) |
| 18 | 17, 9 | sseldd 3984 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
{(0g‘𝐺)}) |
| 19 | | elsni 4643 |
. . . . . . . . 9
⊢ ( 0 ∈
{(0g‘𝐺)}
→ 0
= (0g‘𝐺)) |
| 20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 =
(0g‘𝐺)) |
| 21 | 20 | sneqd 4638 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝐺)}) |
| 22 | 17, 21 | sseqtrrd 4021 |
. . . . . 6
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ⊆ { 0 }) |
| 23 | 10, 22 | eqssd 4001 |
. . . . 5
⊢ (𝜑 → { 0 } = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
| 24 | 2 | ovanraleqv 7455 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ 𝑆 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |
| 25 | 4 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
| 26 | 25, 7 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
| 27 | 26 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
| 28 | 24, 5, 27 | elrabd 3694 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ {𝑦 ∈ 𝑆 ∣ ∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}) |
| 29 | | gsumress.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
| 30 | 29, 12 | ressbas2 17283 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘𝐻)) |
| 31 | 4, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 = (Base‘𝐻)) |
| 32 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝐻)
∈ V |
| 33 | 31, 32 | eqeltrdi 2849 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ V) |
| 34 | 29, 14 | ressplusg 17334 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ V → + =
(+g‘𝐻)) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → + =
(+g‘𝐻)) |
| 36 | 35 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 + 𝑥) = (𝑦(+g‘𝐻)𝑥)) |
| 37 | 36 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 + 𝑥) = 𝑥 ↔ (𝑦(+g‘𝐻)𝑥) = 𝑥)) |
| 38 | 35 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 + 𝑦) = (𝑥(+g‘𝐻)𝑦)) |
| 39 | 38 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 + 𝑦) = 𝑥 ↔ (𝑥(+g‘𝐻)𝑦) = 𝑥)) |
| 40 | 37, 39 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥))) |
| 41 | 31, 40 | raleqbidv 3346 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥) ↔ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥))) |
| 42 | 31, 41 | rabeqbidv 3455 |
. . . . . . . 8
⊢ (𝜑 → {𝑦 ∈ 𝑆 ∣ ∀𝑥 ∈ 𝑆 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
| 43 | 28, 42 | eleqtrd 2843 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
| 44 | 43 | snssd 4809 |
. . . . . 6
⊢ (𝜑 → { 0 } ⊆ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
| 45 | 29 | ovexi 7465 |
. . . . . . . . 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 18685 |
. . . . . . . 8
⊢ (𝐻 ∈ V → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ {(0g‘𝐻)}) |
| 52 | 46, 51 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ {(0g‘𝐻)}) |
| 53 | 52, 43 | sseldd 3984 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
{(0g‘𝐻)}) |
| 54 | | elsni 4643 |
. . . . . . . . 9
⊢ ( 0 ∈
{(0g‘𝐻)}
→ 0
= (0g‘𝐻)) |
| 55 | 53, 54 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 =
(0g‘𝐻)) |
| 56 | 55 | sneqd 4638 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝐻)}) |
| 57 | 52, 56 | sseqtrrd 4021 |
. . . . . 6
⊢ (𝜑 → {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)} ⊆ { 0 }) |
| 58 | 44, 57 | eqssd 4001 |
. . . . 5
⊢ (𝜑 → { 0 } = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
| 59 | 23, 58 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} = {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}) |
| 60 | 59 | sseq2d 4016 |
. . 3
⊢ (𝜑 → (ran 𝐹 ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)} ↔ ran 𝐹 ⊆ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)})) |
| 61 | 20, 55 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
| 62 | 35 | seqeq2d 14049 |
. . . . . . . . . 10
⊢ (𝜑 → seq𝑚( + , 𝐹) = seq𝑚((+g‘𝐻), 𝐹)) |
| 63 | 62 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝜑 → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)) |
| 64 | 63 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) ↔ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛))) |
| 65 | 64 | anbi2d 630 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
| 66 | 65 | rexbidv 3179 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
| 67 | 66 | exbidv 1921 |
. . . . 5
⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
| 68 | 67 | iotabidv 6545 |
. . . 4
⊢ (𝜑 → (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))) = (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚((+g‘𝐻), 𝐹)‘𝑛)))) |
| 69 | 35 | seqeq2d 14049 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , (𝐹 ∘ 𝑓)) = seq1((+g‘𝐻), (𝐹 ∘ 𝑓))) |
| 70 | 69 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝜑 → (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))) =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 }))))) |
| 71 | 70 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝜑 → (𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))) ↔ 𝑧 =
(seq1((+g‘𝐻), (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0 })))))) |
| 72 | 71 | anbi2d 630 |
. . . . . 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 1921 |
. . . . 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 6545 |
. . . 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 4547 |
. . 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 4554 |
. 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 4126 |
. . . 4
⊢ (𝜑 → (V ∖ { 0 }) = (V
∖ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)})) |
| 78 | 77 | imaeq2d 6078 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) = (◡𝐹 “ (V ∖ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}))) |
| 79 | | gsumress.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
| 80 | | gsumress.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
| 81 | 80, 4 | fssd 6753 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 82 | 12, 13, 14, 15, 78, 11, 79, 81 | gsumval 18690 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑦) = 𝑥)}, (0g‘𝐺), if(𝐴 ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(♯‘(◡𝐹 “ (V ∖ { 0 }))))–1-1-onto→(◡𝐹 “ (V ∖ { 0 })) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘(◡𝐹 “ (V ∖ { 0
}))))))))) |
| 83 | 58 | difeq2d 4126 |
. . . 4
⊢ (𝜑 → (V ∖ { 0 }) = (V
∖ {𝑦 ∈
(Base‘𝐻) ∣
∀𝑥 ∈
(Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)})) |
| 84 | 83 | imaeq2d 6078 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) = (◡𝐹 “ (V ∖ {𝑦 ∈ (Base‘𝐻) ∣ ∀𝑥 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑥) = 𝑥 ∧ (𝑥(+g‘𝐻)𝑦) = 𝑥)}))) |
| 85 | 31 | feq3d 6723 |
. . . 4
⊢ (𝜑 → (𝐹:𝐴⟶𝑆 ↔ 𝐹:𝐴⟶(Base‘𝐻))) |
| 86 | 80, 85 | mpbid 232 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐻)) |
| 87 | 47, 48, 49, 50, 84, 46, 79, 86 | gsumval 18690 |
. 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 𝐹)) |