Description: A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | psubclssat.a | |- A = ( Atoms ` K ) |
|
psubclssat.c | |- C = ( PSubCl ` K ) |
||
Assertion | psubclssatN | |- ( ( K e. D /\ X e. C ) -> X C_ A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psubclssat.a | |- A = ( Atoms ` K ) |
|
2 | psubclssat.c | |- C = ( PSubCl ` K ) |
|
3 | eqid | |- ( _|_P ` K ) = ( _|_P ` K ) |
|
4 | 1 3 2 | psubcliN | |- ( ( K e. D /\ X e. C ) -> ( X C_ A /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) |
5 | 4 | simpld | |- ( ( K e. D /\ X e. C ) -> X C_ A ) |