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 = K
lplnset.n N = LLines K
lplnset.p P = LPlanes K
Assertion lplni K D Y B X N X C Y Y P

Proof

Step Hyp Ref Expression
1 lplnset.b B = Base K
2 lplnset.c C = K
3 lplnset.n N = LLines K
4 lplnset.p P = LPlanes K
5 simpl2 K D Y B X N X C Y Y B
6 breq1 x = X x C Y X C Y
7 6 rspcev X N X C Y x N x C Y
8 7 3ad2antl3 K D Y B X N X C Y x N x C Y
9 simpl1 K D Y B X N X C Y K D
10 1 2 3 4 islpln K D Y P Y B x N x C Y
11 9 10 syl K D Y B X N X C Y Y P Y B x N x C Y
12 5 8 11 mpbir2and K D Y B X N X C Y Y P