lplnbase

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

Step	Hyp	Ref	Expression
1		lplnbase.b	$⊢ B = {Base}_{K}$
2		lplnbase.p	$⊢ P = LPlanes (K)$
3		n0i	$⊢ X \in P \to \neg P = \emptyset$
4	2	eqeq1i	$⊢ P = \emptyset \leftrightarrow LPlanes (K) = \emptyset$
5	3 4	sylnib	$⊢ X \in P \to \neg LPlanes (K) = \emptyset$
6		fvprc	$⊢ \neg K \in V \to LPlanes (K) = \emptyset$
7	5 6	nsyl2	$⊢ X \in P \to K \in V$
8		eqid	$⊢ ⋖_{K} = ⋖_{K}$
9		eqid	$⊢ LLines (K) = LLines (K)$
10	1 8 9 2	islpln	$⊢ K \in V \to (X \in P \leftrightarrow (X \in B \land \exists x \in LLines (K) x ⋖_{K} X))$
11	10	simprbda	$⊢ (K \in V \land X \in P) \to X \in B$
12	7 11	mpancom	$⊢ X \in P \to X \in B$

Metamath Proof Explorer