Description: The linear combination over a singleton. (Contributed by AV, 12-Apr-2019) (Proof shortened by AV, 25-May-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lincvalsn.b | ⊢ 𝐵 = ( Base ‘ 𝑀 ) | |
| lincvalsn.s | ⊢ 𝑆 = ( Scalar ‘ 𝑀 ) | ||
| lincvalsn.r | ⊢ 𝑅 = ( Base ‘ 𝑆 ) | ||
| lincvalsn.t | ⊢ · = ( ·𝑠 ‘ 𝑀 ) | ||
| lincvalsn.f | ⊢ 𝐹 = { ⟨ 𝑉 , 𝑌 ⟩ } | ||
| Assertion | lincvalsn | ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lincvalsn.b | ⊢ 𝐵 = ( Base ‘ 𝑀 ) | |
| 2 | lincvalsn.s | ⊢ 𝑆 = ( Scalar ‘ 𝑀 ) | |
| 3 | lincvalsn.r | ⊢ 𝑅 = ( Base ‘ 𝑆 ) | |
| 4 | lincvalsn.t | ⊢ · = ( ·𝑠 ‘ 𝑀 ) | |
| 5 | lincvalsn.f | ⊢ 𝐹 = { ⟨ 𝑉 , 𝑌 ⟩ } | |
| 6 | 5 | oveq1i | ⊢ ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } ) |
| 7 | 1 2 3 4 | lincvalsng | ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) ) |
| 8 | 6 7 | syl5eq | ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) ) |