Theorem lvoli3

Description: Condition implying a 3-dim lattice volume. (Contributed by NM, 2-Aug-2012)

	Ref	Expression
Hypotheses	lvoli3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lvoli3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	lvoli3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lvoli3.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
	lvoli3.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	lvoli3	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to X\underset{\dot{}}{\vee }Q\in V$$

Proof

Step	Hyp	Ref	Expression
1		lvoli3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lvoli3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		lvoli3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		lvoli3.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
5		lvoli3.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
6		simpl2	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to X\in P$$
7		simpl3	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to Q\in A$$
8		simpr	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to \neg Q\underset{\dot{}}{\le }X$$
9		eqidd	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to X\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }Q$$
10		breq2	$$⊢y=X\to \left(r\underset{\dot{}}{\le }y\leftrightarrow r\underset{\dot{}}{\le }X\right)$$
11	10	notbid	$$⊢y=X\to \left(\neg r\underset{\dot{}}{\le }y\leftrightarrow \neg r\underset{\dot{}}{\le }X\right)$$
12		oveq1	$$⊢y=X\to y\underset{\dot{}}{\vee }r=X\underset{\dot{}}{\vee }r$$
13	12	eqeq2d	$$⊢y=X\to \left(X\underset{\dot{}}{\vee }Q=y\underset{\dot{}}{\vee }r\leftrightarrow X\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }r\right)$$
14	11 13	anbi12d	$$⊢y=X\to \left(\left(\neg r\underset{\dot{}}{\le }y\wedge X\underset{\dot{}}{\vee }Q=y\underset{\dot{}}{\vee }r\right)\leftrightarrow \left(\neg r\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }r\right)\right)$$
15		breq1	$$⊢r=Q\to \left(r\underset{\dot{}}{\le }X\leftrightarrow Q\underset{\dot{}}{\le }X\right)$$
16	15	notbid	$$⊢r=Q\to \left(\neg r\underset{\dot{}}{\le }X\leftrightarrow \neg Q\underset{\dot{}}{\le }X\right)$$
17		oveq2	$$⊢r=Q\to X\underset{\dot{}}{\vee }r=X\underset{\dot{}}{\vee }Q$$
18	17	eqeq2d	$$⊢r=Q\to \left(X\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }r\leftrightarrow X\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }Q\right)$$
19	16 18	anbi12d	$$⊢r=Q\to \left(\left(\neg r\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }r\right)\leftrightarrow \left(\neg Q\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }Q\right)\right)$$
20	14 19	rspc2ev	$$⊢\left(X\in P\wedge Q\in A\wedge \left(\neg Q\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }Q\right)\right)\to \exists y\in P\exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X\underset{\dot{}}{\vee }Q=y\underset{\dot{}}{\vee }r\right)$$
21	6 7 8 9 20	syl112anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to \exists y\in P\exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X\underset{\dot{}}{\vee }Q=y\underset{\dot{}}{\vee }r\right)$$
22		simpl1	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to K\in \mathrm{HL}$$
23	22	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to K\in \mathrm{Lat}$$
24		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
25	24 4	lplnbase	$$⊢X\in P\to X\in {\mathrm{Base}}_K$$
26	6 25	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to X\in {\mathrm{Base}}_K$$
27	24 3	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
28	7 27	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to Q\in {\mathrm{Base}}_K$$
29	24 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in {\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\right)\to X\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
30	23 26 28 29	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to X\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
31	24 1 2 3 4 5	islvol3	$$⊢\left(K\in \mathrm{HL}\wedge X\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\to \left(X\underset{\dot{}}{\vee }Q\in V\leftrightarrow \exists y\in P\exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X\underset{\dot{}}{\vee }Q=y\underset{\dot{}}{\vee }r\right)\right)$$
32	22 30 31	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to \left(X\underset{\dot{}}{\vee }Q\in V\leftrightarrow \exists y\in P\exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X\underset{\dot{}}{\vee }Q=y\underset{\dot{}}{\vee }r\right)\right)$$
33	21 32	mpbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Q\in A\right)\wedge \neg Q\underset{\dot{}}{\le }X\right)\to X\underset{\dot{}}{\vee }Q\in V$$