Description: A closed subspace is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cssss.v | |- V = ( Base ` W ) |
|
cssss.c | |- C = ( ClSubSp ` W ) |
||
Assertion | cssss | |- ( S e. C -> S C_ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cssss.v | |- V = ( Base ` W ) |
|
2 | cssss.c | |- C = ( ClSubSp ` W ) |
|
3 | eqid | |- ( ocv ` W ) = ( ocv ` W ) |
|
4 | 3 2 | cssi | |- ( S e. C -> S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) ) |
5 | 1 3 | ocvss | |- ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) C_ V |
6 | 4 5 | eqsstrdi | |- ( S e. C -> S C_ V ) |