Theorem islpln2

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 25-Jun-2012)

	Ref	Expression
Hypotheses	islpln5.b	$$⊢B={\mathrm{Base}}_K$$
	islpln5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	islpln5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	islpln5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	islpln5.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	islpln2	$$⊢K\in \mathrm{HL}\to \left(X\in P\leftrightarrow \left(X\in B\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islpln5.b	$$⊢B={\mathrm{Base}}_K$$
2		islpln5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		islpln5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		islpln5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		islpln5.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
6	1 5	lplnbase	$$⊢X\in P\to X\in B$$
7	6	pm4.71ri	$$⊢X\in P\leftrightarrow \left(X\in B\wedge X\in P\right)$$
8	1 2 3 4 5	islpln5	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(X\in P\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
9	8	pm5.32da	$$⊢K\in \mathrm{HL}\to \left(\left(X\in B\wedge X\in P\right)\leftrightarrow \left(X\in B\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
10	7 9	bitrid	$$⊢K\in \mathrm{HL}\to \left(X\in P\leftrightarrow \left(X\in B\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$