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 | |- V = ( Base ` W ) |
|
| lssss.s | |- S = ( LSubSp ` W ) |
||
| Assertion | lssss | |- ( U e. S -> U C_ V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lssss.v | |- V = ( Base ` W ) |
|
| 2 | lssss.s | |- S = ( LSubSp ` W ) |
|
| 3 | eqid | |- ( Scalar ` W ) = ( Scalar ` W ) |
|
| 4 | eqid | |- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
|
| 5 | eqid | |- ( +g ` W ) = ( +g ` W ) |
|
| 6 | eqid | |- ( .s ` W ) = ( .s ` W ) |
|
| 7 | 3 4 1 5 6 2 | islss | |- ( U e. S <-> ( U C_ V /\ 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 | simp1bi | |- ( U e. S -> U C_ V ) |