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 \in D \land Y \in B \land X \in N) \land X C Y) \to Y \in P$

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 \in D \land Y \in B \land X \in N) \land X C Y) \to Y \in B$
6		breq1	$⊢ x = X \to (x C Y \leftrightarrow X C Y)$
7	6	rspcev	$⊢ (X \in N \land X C Y) \to \exists x \in N x C Y$
8	7	3ad2antl3	$⊢ ((K \in D \land Y \in B \land X \in N) \land X C Y) \to \exists x \in N x C Y$
9		simpl1	$⊢ ((K \in D \land Y \in B \land X \in N) \land X C Y) \to K \in D$
10	1 2 3 4	islpln	$⊢ K \in D \to (Y \in P \leftrightarrow (Y \in B \land \exists x \in N x C Y))$
11	9 10	syl	$⊢ ((K \in D \land Y \in B \land X \in N) \land X C Y) \to (Y \in P \leftrightarrow (Y \in B \land \exists x \in N x C Y))$
12	5 8 11	mpbir2and	$⊢ ((K \in D \land Y \in B \land X \in N) \land X C Y) \to Y \in P$

Metamath Proof Explorer