Theorem islpln4

Description: The predicate "is a lattice plane". (Contributed by NM, 17-Jun-2012)

	Ref	Expression
Hypotheses	lplnset.b	$$⊢B={\mathrm{Base}}_K$$
	lplnset.c	$$⊢C={⋖}_K$$
	lplnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
	lplnset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	islpln4	$$⊢\left(K\in A\wedge X\in B\right)\to \left(X\in P\leftrightarrow \exists y\in NyCX\right)$$

Proof

Step	Hyp	Ref	Expression
1		lplnset.b	$$⊢B={\mathrm{Base}}_K$$
2		lplnset.c	$$⊢C={⋖}_K$$
3		lplnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
4		lplnset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
5	1 2 3 4	islpln	$$⊢K\in A\to \left(X\in P\leftrightarrow \left(X\in B\wedge \exists y\in NyCX\right)\right)$$
6	5	baibd	$$⊢\left(K\in A\wedge X\in B\right)\to \left(X\in P\leftrightarrow \exists y\in NyCX\right)$$