Description: Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lmodvscld.v | |- V = ( Base ` W ) |
|
| lmodvscld.f | |- F = ( Scalar ` W ) |
||
| lmodvscld.s | |- .x. = ( .s ` W ) |
||
| lmodvscld.k | |- K = ( Base ` F ) |
||
| lmodvscld.w | |- ( ph -> W e. LMod ) |
||
| lmodvscld.r | |- ( ph -> R e. K ) |
||
| lmodvscld.x | |- ( ph -> X e. V ) |
||
| Assertion | lmodvscld | |- ( ph -> ( R .x. X ) e. V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lmodvscld.v | |- V = ( Base ` W ) |
|
| 2 | lmodvscld.f | |- F = ( Scalar ` W ) |
|
| 3 | lmodvscld.s | |- .x. = ( .s ` W ) |
|
| 4 | lmodvscld.k | |- K = ( Base ` F ) |
|
| 5 | lmodvscld.w | |- ( ph -> W e. LMod ) |
|
| 6 | lmodvscld.r | |- ( ph -> R e. K ) |
|
| 7 | lmodvscld.x | |- ( ph -> X e. V ) |
|
| 8 | 1 2 3 4 | lmodvscl | |- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V ) |
| 9 | 5 6 7 8 | syl3anc | |- ( ph -> ( R .x. X ) e. V ) |