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 ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝑈 )