Theorem lssss

Description: A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Hypotheses	lssss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lssss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lssss	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lssss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lssss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
4		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
5		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
6		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
7	3 4 1 5 6 2	islss	⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑈 ) )
8	7	simp1bi	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )