Metamath Proof Explorer

Theorem lssvacl

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

Ref Expression
Hypotheses lssvacl.p ⊢ + = ( +g ‘ 𝑊 )
lssvacl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lssvacl ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 lssvacl.p ⊢ + = ( +g ‘ 𝑊 )
2 lssvacl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 simpll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑊 ∈ LMod )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 4 2 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
6 5 ad2ant2lr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
7 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
9 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
10 4 7 8 9 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 𝑋 )
11 3 6 10 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 𝑋 )
12 11 oveq1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + 𝑌 ) = ( 𝑋 + 𝑌 ) )
13 simplr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑆 )
14 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
15 7 14 9 lmod1cl ⊢ ( 𝑊 ∈ LMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
16 15 ad2antrr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 simprl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑋 ∈ 𝑈 )
18 simprr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑌 ∈ 𝑈 )
19 7 14 1 8 2 lsscl ⊢ ( ( 𝑈 ∈ 𝑆 ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + 𝑌 ) ∈ 𝑈 )
20 13 16 17 18 19 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) + 𝑌 ) ∈ 𝑈 )
21 12 20 eqeltrrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝑈 )