This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = Scalar ⁡ W
lssvscl.t ⊢ · ˙ = ⋅ W
lssvscl.b ⊢ B = Base F
lssvscl.s ⊢ S = LSubSp ⁡ W
Assertion lssvscl ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → X · ˙ Y ∈ U

Proof

Step Hyp Ref Expression
1 lssvscl.f ⊢ F = Scalar ⁡ W
2 lssvscl.t ⊢ · ˙ = ⋅ W
3 lssvscl.b ⊢ B = Base F
4 lssvscl.s ⊢ S = LSubSp ⁡ W
5 simpll ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → W ∈ LMod
6 simprl ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → X ∈ B
7 eqid ⊢ Base W = Base W
8 7 4 lssel ⊢ U ∈ S ∧ Y ∈ U → Y ∈ Base W
9 8 ad2ant2l ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → Y ∈ Base W
10 7 1 2 3 lmodvscl ⊢ W ∈ LMod ∧ X ∈ B ∧ Y ∈ Base W → X · ˙ Y ∈ Base W
11 5 6 9 10 syl3anc ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → X · ˙ Y ∈ Base W
12 eqid ⊢ + W = + W
13 eqid ⊢ 0 W = 0 W
14 7 12 13 lmod0vrid ⊢ W ∈ LMod ∧ X · ˙ Y ∈ Base W → X · ˙ Y + W 0 W = X · ˙ Y
15 5 11 14 syl2anc ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → X · ˙ Y + W 0 W = X · ˙ Y
16 simplr ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → U ∈ S
17 simprr ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → Y ∈ U
18 13 4 lss0cl ⊢ W ∈ LMod ∧ U ∈ S → 0 W ∈ U
19 18 adantr ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → 0 W ∈ U
20 1 3 12 2 4 lsscl ⊢ U ∈ S ∧ X ∈ B ∧ Y ∈ U ∧ 0 W ∈ U → X · ˙ Y + W 0 W ∈ U
21 16 6 17 19 20 syl13anc ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → X · ˙ Y + W 0 W ∈ U
22 15 21 eqeltrrd ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ B ∧ Y ∈ U → X · ˙ Y ∈ U