Description: A function mapping to a scalar product in which one factor is finitely supported is finitely supported. Formerly part of proof for ply1coe . (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 8-Aug-2019) (Proof shortened by AV, 18-Oct-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mptscmfsuppd.b | |- B = ( Base ` P ) |
|
| mptscmfsuppd.s | |- S = ( Scalar ` P ) |
||
| mptscmfsuppd.n | |- .x. = ( .s ` P ) |
||
| mptscmfsuppd.p | |- ( ph -> P e. LMod ) |
||
| mptscmfsuppd.x | |- ( ph -> X e. V ) |
||
| mptscmfsuppd.z | |- ( ( ph /\ k e. X ) -> Z e. B ) |
||
| mptscmfsuppd.a | |- ( ph -> A : X --> Y ) |
||
| mptscmfsuppd.f | |- ( ph -> A finSupp ( 0g ` S ) ) |
||
| Assertion | mptscmfsuppd | |- ( ph -> ( k e. X |-> ( ( A ` k ) .x. Z ) ) finSupp ( 0g ` P ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mptscmfsuppd.b | |- B = ( Base ` P ) |
|
| 2 | mptscmfsuppd.s | |- S = ( Scalar ` P ) |
|
| 3 | mptscmfsuppd.n | |- .x. = ( .s ` P ) |
|
| 4 | mptscmfsuppd.p | |- ( ph -> P e. LMod ) |
|
| 5 | mptscmfsuppd.x | |- ( ph -> X e. V ) |
|
| 6 | mptscmfsuppd.z | |- ( ( ph /\ k e. X ) -> Z e. B ) |
|
| 7 | mptscmfsuppd.a | |- ( ph -> A : X --> Y ) |
|
| 8 | mptscmfsuppd.f | |- ( ph -> A finSupp ( 0g ` S ) ) |
|
| 9 | 2 | a1i | |- ( ph -> S = ( Scalar ` P ) ) |
| 10 | fvexd | |- ( ( ph /\ k e. X ) -> ( A ` k ) e. _V ) |
|
| 11 | eqid | |- ( 0g ` P ) = ( 0g ` P ) |
|
| 12 | eqid | |- ( 0g ` S ) = ( 0g ` S ) |
|
| 13 | 7 | feqmptd | |- ( ph -> A = ( k e. X |-> ( A ` k ) ) ) |
| 14 | 13 8 | eqbrtrrd | |- ( ph -> ( k e. X |-> ( A ` k ) ) finSupp ( 0g ` S ) ) |
| 15 | 5 4 9 1 10 6 11 12 3 14 | mptscmfsupp0 | |- ( ph -> ( k e. X |-> ( ( A ` k ) .x. Z ) ) finSupp ( 0g ` P ) ) |