Metamath Proof Explorer


Theorem 1psubclN

Description: The set of all atoms is a closed projective subspace. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 1psubcl.a
|- A = ( Atoms ` K )
1psubcl.c
|- C = ( PSubCl ` K )
Assertion 1psubclN
|- ( K e. HL -> A e. C )

Proof

Step Hyp Ref Expression
1 1psubcl.a
 |-  A = ( Atoms ` K )
2 1psubcl.c
 |-  C = ( PSubCl ` K )
3 ssidd
 |-  ( K e. HL -> A C_ A )
4 eqid
 |-  ( _|_P ` K ) = ( _|_P ` K )
5 1 4 pol1N
 |-  ( K e. HL -> ( ( _|_P ` K ) ` A ) = (/) )
6 5 fveq2d
 |-  ( K e. HL -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` A ) ) = ( ( _|_P ` K ) ` (/) ) )
7 1 4 pol0N
 |-  ( K e. HL -> ( ( _|_P ` K ) ` (/) ) = A )
8 6 7 eqtrd
 |-  ( K e. HL -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` A ) ) = A )
9 1 4 2 ispsubclN
 |-  ( K e. HL -> ( A e. C <-> ( A C_ A /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` A ) ) = A ) ) )
10 3 8 9 mpbir2and
 |-  ( K e. HL -> A e. C )