Theorem islvol2

Description: The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012)

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

Proof

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