Metamath Proof Explorer

Theorem lssvscl

Description: Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lssvscl.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
lssvscl.t
lssvscl.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
lssvscl.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion lssvscl

Proof

Step Hyp Ref Expression
1 lssvscl.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 lssvscl.t
3 lssvscl.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
4 lssvscl.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
5 simpll ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({X}\in {B}\wedge {Y}\in {U}\right)\right)\to {W}\in \mathrm{LMod}$
6 simprl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({X}\in {B}\wedge {Y}\in {U}\right)\right)\to {X}\in {B}$
7 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
8 7 4 lssel ${⊢}\left({U}\in {S}\wedge {Y}\in {U}\right)\to {Y}\in {\mathrm{Base}}_{{W}}$
9 8 ad2ant2l ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({X}\in {B}\wedge {Y}\in {U}\right)\right)\to {Y}\in {\mathrm{Base}}_{{W}}$
10 7 1 2 3 lmodvscl
11 5 6 9 10 syl3anc
12 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
13 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
14 7 12 13 lmod0vrid
15 5 11 14 syl2anc
16 simplr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({X}\in {B}\wedge {Y}\in {U}\right)\right)\to {U}\in {S}$
17 simprr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({X}\in {B}\wedge {Y}\in {U}\right)\right)\to {Y}\in {U}$
18 13 4 lss0cl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {0}_{{W}}\in {U}$
19 18 adantr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({X}\in {B}\wedge {Y}\in {U}\right)\right)\to {0}_{{W}}\in {U}$
20 1 3 12 2 4 lsscl
21 16 6 17 19 20 syl13anc
22 15 21 eqeltrrd