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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lssvscl.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lssvscl.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
lssvscl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lssvscl ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 lssvscl.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 lssvscl.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lssvscl.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 lssvscl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
5 simpll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑊 ∈ LMod )
6 simprl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
7 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
8 7 4 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
9 8 ad2ant2l ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
10 7 1 2 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
11 5 6 9 10 syl3anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
12 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
13 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
14 7 12 13 lmod0vrid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑋 · 𝑌 ) )
15 5 11 14 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑋 · 𝑌 ) )
16 simplr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑆 )
17 simprr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑌 ∈ 𝑈 )
18 13 4 lss0cl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
19 18 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
20 1 3 12 2 4 lsscl ⊢ ( ( 𝑈 ∈ 𝑆 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ∈ 𝑈 )
21 16 6 17 19 20 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ∈ 𝑈 )
22 15 21 eqeltrrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )