Description: A subspace is not empty. (Contributed by NM, 12-Jan-2014) (Revised by Mario Carneiro, 8-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | lssn0.s | |- S = ( LSubSp ` W ) |
|
| Assertion | lssn0 | |- ( U e. S -> U =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lssn0.s | |- S = ( LSubSp ` W ) |
|
| 2 | eqid | |- ( Scalar ` W ) = ( Scalar ` W ) |
|
| 3 | eqid | |- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
|
| 4 | eqid | |- ( Base ` W ) = ( Base ` W ) |
|
| 5 | eqid | |- ( +g ` W ) = ( +g ` W ) |
|
| 6 | eqid | |- ( .s ` W ) = ( .s ` W ) |
|
| 7 | 2 3 4 5 6 1 | islss | |- ( U e. S <-> ( U C_ ( Base ` W ) /\ U =/= (/) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. a e. U A. b e. U ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. U ) ) |
| 8 | 7 | simp2bi | |- ( U e. S -> U =/= (/) ) |