Step |
Hyp |
Ref |
Expression |
1 |
|
gsumncl.k |
|- K = ( Base ` M ) |
2 |
|
gsumncl.w |
|- ( ph -> M e. Mnd ) |
3 |
|
gsumncl.p |
|- ( ph -> P e. ( ZZ>= ` N ) ) |
4 |
|
gsumncl.b |
|- ( ( ph /\ k e. ( N ... P ) ) -> B e. K ) |
5 |
|
eqid |
|- ( +g ` M ) = ( +g ` M ) |
6 |
4
|
fmpttd |
|- ( ph -> ( k e. ( N ... P ) |-> B ) : ( N ... P ) --> K ) |
7 |
1 5 2 3 6
|
gsumval2 |
|- ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) = ( seq N ( ( +g ` M ) , ( k e. ( N ... P ) |-> B ) ) ` P ) ) |
8 |
6
|
ffvelrnda |
|- ( ( ph /\ x e. ( N ... P ) ) -> ( ( k e. ( N ... P ) |-> B ) ` x ) e. K ) |
9 |
2
|
adantr |
|- ( ( ph /\ ( x e. K /\ y e. K ) ) -> M e. Mnd ) |
10 |
|
simprl |
|- ( ( ph /\ ( x e. K /\ y e. K ) ) -> x e. K ) |
11 |
|
simprr |
|- ( ( ph /\ ( x e. K /\ y e. K ) ) -> y e. K ) |
12 |
1 5
|
mndcl |
|- ( ( M e. Mnd /\ x e. K /\ y e. K ) -> ( x ( +g ` M ) y ) e. K ) |
13 |
9 10 11 12
|
syl3anc |
|- ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` M ) y ) e. K ) |
14 |
3 8 13
|
seqcl |
|- ( ph -> ( seq N ( ( +g ` M ) , ( k e. ( N ... P ) |-> B ) ) ` P ) e. K ) |
15 |
7 14
|
eqeltrd |
|- ( ph -> ( M gsum ( k e. ( N ... P ) |-> B ) ) e. K ) |