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

Metamath Proof Explorer

Theorem islpln4

Description: The predicate "is a lattice plane". (Contributed by NM, 17-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	islpln4	$⊢ (K \in A \land X \in B) \to (X \in P \leftrightarrow \exists y \in N y C X)$

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	1 2 3 4	islpln	$⊢ K \in A \to (X \in P \leftrightarrow (X \in B \land \exists y \in N y C X))$
6	5	baibd	$⊢ (K \in A \land X \in B) \to (X \in P \leftrightarrow \exists y \in N y C X)$