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

Metamath Proof Explorer

Theorem lplni

Description: Condition implying a lattice plane. (Contributed by NM, 20-Jun-2012)

Ref Expression
Hypotheses lplnset.b 
|- B = ( Base ` K )
lplnset.c 
|- C = (
lplnset.n 
|- N = ( LLines ` K )
lplnset.p 
|- P = ( LPlanes ` K )
Assertion lplni 
|- ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> Y e. P )

Proof

Step Hyp Ref Expression
1 lplnset.b 
 |-  B = ( Base ` K )
2 lplnset.c 
 |-  C = (
3 lplnset.n 
 |-  N = ( LLines ` K )
4 lplnset.p 
 |-  P = ( LPlanes ` K )
5 simpl2 
 |-  ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> Y e. B )
6 breq1 
 |-  ( x = X -> ( x C Y <-> X C Y ) )
7 6 rspcev 
 |-  ( ( X e. N /\ X C Y ) -> E. x e. N x C Y )
8 7 3ad2antl3 
 |-  ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> E. x e. N x C Y )
9 simpl1 
 |-  ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> K e. D )
10 1 2 3 4 islpln 
 |-  ( K e. D -> ( Y e. P <-> ( Y e. B /\ E. x e. N x C Y ) ) )
11 9 10 syl 
 |-  ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> ( Y e. P <-> ( Y e. B /\ E. x e. N x C Y ) ) )
12 5 8 11 mpbir2and 
 |-  ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> Y e. P )