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

Metamath Proof Explorer

Theorem lplnbase

Description: A lattice plane is a lattice element. (Contributed by NM, 17-Jun-2012)

Ref Expression
Hypotheses lplnbase.b 
|- B = ( Base ` K )
lplnbase.p 
|- P = ( LPlanes ` K )
Assertion lplnbase 
|- ( X e. P -> X e. B )

Proof

Step Hyp Ref Expression
1 lplnbase.b 
 |-  B = ( Base ` K )
2 lplnbase.p 
 |-  P = ( LPlanes ` K )
3 n0i 
 |-  ( X e. P -> -. P = (/) )
4 2 eqeq1i 
 |-  ( P = (/) <-> ( LPlanes ` K ) = (/) )
5 3 4 sylnib 
 |-  ( X e. P -> -. ( LPlanes ` K ) = (/) )
6 fvprc 
 |-  ( -. K e. _V -> ( LPlanes ` K ) = (/) )
7 5 6 nsyl2 
 |-  ( X e. P -> K e. _V )
8 eqid 
 |-  (
9 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
10 1 8 9 2 islpln 
 |-  ( K e. _V -> ( X e. P <-> ( X e. B /\ E. x e. ( LLines ` K ) x (
11 10 simprbda 
 |-  ( ( K e. _V /\ X e. P ) -> X e. B )
12 7 11 mpancom 
 |-  ( X e. P -> X e. B )