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 | ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 ) |
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 | ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 ) |