# Metamath Proof Explorer

## Theorem lincvalsng

Description: The linear combination over a singleton. (Contributed by AV, 25-May-2019)

Ref Expression
Hypotheses lincvalsn.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
lincvalsn.s ${⊢}{S}=\mathrm{Scalar}\left({M}\right)$
lincvalsn.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
lincvalsn.t
Assertion lincvalsng

### Proof

Step Hyp Ref Expression
1 lincvalsn.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 lincvalsn.s ${⊢}{S}=\mathrm{Scalar}\left({M}\right)$
3 lincvalsn.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
4 lincvalsn.t
5 simp1 ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to {M}\in \mathrm{LMod}$
6 simp2 ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to {V}\in {B}$
7 2 fveq2i ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
8 3 7 eqtri ${⊢}{R}={\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
9 8 eleq2i ${⊢}{Y}\in {R}↔{Y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
10 9 biimpi ${⊢}{Y}\in {R}\to {Y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
11 10 3ad2ant3 ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to {Y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
12 fvexd ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}\in \mathrm{V}$
13 eqid ${⊢}\left\{⟨{V},{Y}⟩\right\}=\left\{⟨{V},{Y}⟩\right\}$
14 13 mapsnop ${⊢}\left({V}\in {B}\wedge {Y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}\wedge {\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}\in \mathrm{V}\right)\to \left\{⟨{V},{Y}⟩\right\}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\left\{{V}\right\}}\right)$
15 6 11 12 14 syl3anc ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to \left\{⟨{V},{Y}⟩\right\}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\left\{{V}\right\}}\right)$
16 snelpwi ${⊢}{V}\in {\mathrm{Base}}_{{M}}\to \left\{{V}\right\}\in 𝒫{\mathrm{Base}}_{{M}}$
17 16 1 eleq2s ${⊢}{V}\in {B}\to \left\{{V}\right\}\in 𝒫{\mathrm{Base}}_{{M}}$
18 17 3ad2ant2 ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to \left\{{V}\right\}\in 𝒫{\mathrm{Base}}_{{M}}$
19 lincval ${⊢}\left({M}\in \mathrm{LMod}\wedge \left\{⟨{V},{Y}⟩\right\}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\left\{{V}\right\}}\right)\wedge \left\{{V}\right\}\in 𝒫{\mathrm{Base}}_{{M}}\right)\to \left\{⟨{V},{Y}⟩\right\}\mathrm{linC}\left({M}\right)\left\{{V}\right\}=\underset{{v}\in \left\{{V}\right\}}{{\sum }_{{M}}}\left(\left\{⟨{V},{Y}⟩\right\}\left({v}\right){\cdot }_{{M}}{v}\right)$
20 5 15 18 19 syl3anc ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to \left\{⟨{V},{Y}⟩\right\}\mathrm{linC}\left({M}\right)\left\{{V}\right\}=\underset{{v}\in \left\{{V}\right\}}{{\sum }_{{M}}}\left(\left\{⟨{V},{Y}⟩\right\}\left({v}\right){\cdot }_{{M}}{v}\right)$
21 lmodgrp ${⊢}{M}\in \mathrm{LMod}\to {M}\in \mathrm{Grp}$
22 grpmnd ${⊢}{M}\in \mathrm{Grp}\to {M}\in \mathrm{Mnd}$
23 21 22 syl ${⊢}{M}\in \mathrm{LMod}\to {M}\in \mathrm{Mnd}$
24 23 3ad2ant1 ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to {M}\in \mathrm{Mnd}$
25 fvsng ${⊢}\left({V}\in {B}\wedge {Y}\in {R}\right)\to \left\{⟨{V},{Y}⟩\right\}\left({V}\right)={Y}$
26 25 3adant1 ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to \left\{⟨{V},{Y}⟩\right\}\left({V}\right)={Y}$
27 26 oveq1d ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to \left\{⟨{V},{Y}⟩\right\}\left({V}\right){\cdot }_{{M}}{V}={Y}{\cdot }_{{M}}{V}$
28 eqid ${⊢}{\cdot }_{{M}}={\cdot }_{{M}}$
29 1 2 28 3 lmodvscl ${⊢}\left({M}\in \mathrm{LMod}\wedge {Y}\in {R}\wedge {V}\in {B}\right)\to {Y}{\cdot }_{{M}}{V}\in {B}$
30 29 3com23 ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to {Y}{\cdot }_{{M}}{V}\in {B}$
31 27 30 eqeltrd ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to \left\{⟨{V},{Y}⟩\right\}\left({V}\right){\cdot }_{{M}}{V}\in {B}$
32 fveq2 ${⊢}{v}={V}\to \left\{⟨{V},{Y}⟩\right\}\left({v}\right)=\left\{⟨{V},{Y}⟩\right\}\left({V}\right)$
33 id ${⊢}{v}={V}\to {v}={V}$
34 32 33 oveq12d ${⊢}{v}={V}\to \left\{⟨{V},{Y}⟩\right\}\left({v}\right){\cdot }_{{M}}{v}=\left\{⟨{V},{Y}⟩\right\}\left({V}\right){\cdot }_{{M}}{V}$
35 1 34 gsumsn ${⊢}\left({M}\in \mathrm{Mnd}\wedge {V}\in {B}\wedge \left\{⟨{V},{Y}⟩\right\}\left({V}\right){\cdot }_{{M}}{V}\in {B}\right)\to \underset{{v}\in \left\{{V}\right\}}{{\sum }_{{M}}}\left(\left\{⟨{V},{Y}⟩\right\}\left({v}\right){\cdot }_{{M}}{v}\right)=\left\{⟨{V},{Y}⟩\right\}\left({V}\right){\cdot }_{{M}}{V}$
36 24 6 31 35 syl3anc ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to \underset{{v}\in \left\{{V}\right\}}{{\sum }_{{M}}}\left(\left\{⟨{V},{Y}⟩\right\}\left({v}\right){\cdot }_{{M}}{v}\right)=\left\{⟨{V},{Y}⟩\right\}\left({V}\right){\cdot }_{{M}}{V}$
37 4 eqcomi
38 37 a1i
39 eqidd ${⊢}\left({M}\in \mathrm{LMod}\wedge {V}\in {B}\wedge {Y}\in {R}\right)\to {V}={V}$
40 38 26 39 oveq123d
41 20 36 40 3eqtrd