Step |
Hyp |
Ref |
Expression |
1 |
|
srgsummulcr.b |
|- B = ( Base ` R ) |
2 |
|
srgsummulcr.z |
|- .0. = ( 0g ` R ) |
3 |
|
srgsummulcr.p |
|- .+ = ( +g ` R ) |
4 |
|
srgsummulcr.t |
|- .x. = ( .r ` R ) |
5 |
|
srgsummulcr.r |
|- ( ph -> R e. SRing ) |
6 |
|
srgsummulcr.a |
|- ( ph -> A e. V ) |
7 |
|
srgsummulcr.y |
|- ( ph -> Y e. B ) |
8 |
|
srgsummulcr.x |
|- ( ( ph /\ k e. A ) -> X e. B ) |
9 |
|
srgsummulcr.n |
|- ( ph -> ( k e. A |-> X ) finSupp .0. ) |
10 |
|
srgcmn |
|- ( R e. SRing -> R e. CMnd ) |
11 |
5 10
|
syl |
|- ( ph -> R e. CMnd ) |
12 |
|
srgmnd |
|- ( R e. SRing -> R e. Mnd ) |
13 |
5 12
|
syl |
|- ( ph -> R e. Mnd ) |
14 |
1 4
|
srglmhm |
|- ( ( R e. SRing /\ Y e. B ) -> ( x e. B |-> ( Y .x. x ) ) e. ( R MndHom R ) ) |
15 |
5 7 14
|
syl2anc |
|- ( ph -> ( x e. B |-> ( Y .x. x ) ) e. ( R MndHom R ) ) |
16 |
|
oveq2 |
|- ( x = X -> ( Y .x. x ) = ( Y .x. X ) ) |
17 |
|
oveq2 |
|- ( x = ( R gsum ( k e. A |-> X ) ) -> ( Y .x. x ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) ) |
18 |
1 2 11 13 6 15 8 9 16 17
|
gsummhm2 |
|- ( ph -> ( R gsum ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) ) |