# Metamath Proof Explorer

## Theorem lcdvscl

Description: The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses lcdvscl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
lcdvscl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lcdvscl.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
lcdvscl.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
lcdvscl.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
lcdvscl.v ${⊢}{V}={\mathrm{Base}}_{{C}}$
lcdvscl.t
lcdvscl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
lcdvscl.x ${⊢}{\phi }\to {X}\in {R}$
lcdvscl.g ${⊢}{\phi }\to {G}\in {V}$
Assertion lcdvscl

### Proof

Step Hyp Ref Expression
1 lcdvscl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lcdvscl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 lcdvscl.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
4 lcdvscl.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
5 lcdvscl.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
6 lcdvscl.v ${⊢}{V}={\mathrm{Base}}_{{C}}$
7 lcdvscl.t
8 lcdvscl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 lcdvscl.x ${⊢}{\phi }\to {X}\in {R}$
10 lcdvscl.g ${⊢}{\phi }\to {G}\in {V}$
11 1 5 8 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
12 eqid ${⊢}\mathrm{Scalar}\left({C}\right)=\mathrm{Scalar}\left({C}\right)$
13 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
14 1 2 3 4 5 12 13 8 lcdsbase ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}={R}$
15 9 14 eleqtrrd ${⊢}{\phi }\to {X}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
16 6 12 7 13 lmodvscl
17 11 15 10 16 syl3anc