This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )