Metamath Proof Explorer


Theorem lplnneat

Description: No lattice plane is an atom. (Contributed by NM, 15-Jul-2012)

Ref Expression
Hypotheses lplnneat.a
|- A = ( Atoms ` K )
lplnneat.p
|- P = ( LPlanes ` K )
Assertion lplnneat
|- ( ( K e. HL /\ X e. P ) -> -. X e. A )

Proof

Step Hyp Ref Expression
1 lplnneat.a
 |-  A = ( Atoms ` K )
2 lplnneat.p
 |-  P = ( LPlanes ` K )
3 hllat
 |-  ( K e. HL -> K e. Lat )
4 eqid
 |-  ( Base ` K ) = ( Base ` K )
5 4 2 lplnbase
 |-  ( X e. P -> X e. ( Base ` K ) )
6 eqid
 |-  ( le ` K ) = ( le ` K )
7 4 6 latref
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) ) -> X ( le ` K ) X )
8 3 5 7 syl2an
 |-  ( ( K e. HL /\ X e. P ) -> X ( le ` K ) X )
9 6 1 2 lplnnleat
 |-  ( ( K e. HL /\ X e. P /\ X e. A ) -> -. X ( le ` K ) X )
10 9 3expia
 |-  ( ( K e. HL /\ X e. P ) -> ( X e. A -> -. X ( le ` K ) X ) )
11 8 10 mt2d
 |-  ( ( K e. HL /\ X e. P ) -> -. X e. A )