Description: A subspace is not empty. (Contributed by NM, 12-Jan-2014) (Revised by Mario Carneiro, 8-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | lssn0.s | ⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) | |
| Assertion | lssn0 | ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ≠ ∅ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lssn0.s | ⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) | |
| 2 | eqid | ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) | |
| 3 | eqid | ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) | |
| 4 | eqid | ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) | |
| 5 | eqid | ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) | |
| 6 | eqid | ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) | |
| 7 | 2 3 4 5 6 1 | islss | ⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑈 ) ) |
| 8 | 7 | simp2bi | ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ≠ ∅ ) |