Theorem lplnbase

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

	Ref	Expression
Hypotheses	lplnbase.b	$$⊢B={\mathrm{Base}}_K$$
	lplnbase.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	lplnbase	$$⊢X\in P\to X\in B$$

Proof

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