Theorem islln2

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

	Ref	Expression
Hypotheses	islln3.b	$$⊢B={\mathrm{Base}}_K$$
	islln3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	islln3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	islln3.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
Assertion	islln2	$$⊢K\in \mathrm{HL}\to \left(X\in N\leftrightarrow \left(X\in B\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge X=p\underset{\dot{}}{\vee }q\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islln3.b	$$⊢B={\mathrm{Base}}_K$$
2		islln3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		islln3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		islln3.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
5	1 4	llnbase	$$⊢X\in N\to X\in B$$
6	5	pm4.71ri	$$⊢X\in N\leftrightarrow \left(X\in B\wedge X\in N\right)$$
7	1 2 3 4	islln3	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(X\in N\leftrightarrow \exists p\in A\exists q\in A\left(p\ne q\wedge X=p\underset{\dot{}}{\vee }q\right)\right)$$
8	7	pm5.32da	$$⊢K\in \mathrm{HL}\to \left(\left(X\in B\wedge X\in N\right)\leftrightarrow \left(X\in B\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge X=p\underset{\dot{}}{\vee }q\right)\right)\right)$$
9	6 8	bitrid	$$⊢K\in \mathrm{HL}\to \left(X\in N\leftrightarrow \left(X\in B\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge X=p\underset{\dot{}}{\vee }q\right)\right)\right)$$