Theorem cvrat42

Description: Commuted version of cvrat4 . (Contributed by NM, 28-Jan-2012)

	Ref	Expression
Hypotheses	cvrat4.b	$$⊢B={\mathrm{Base}}_K$$
	cvrat4.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cvrat4.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cvrat4.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	cvrat4.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	cvrat42	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\to \left(\left(X\ne \underset{\dot{}}{0}\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to \exists r\in A\left(r\underset{\dot{}}{\le }X\wedge P\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }Q\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cvrat4.b	$$⊢B={\mathrm{Base}}_K$$
2		cvrat4.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cvrat4.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cvrat4.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
5		cvrat4.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6	1 2 3 4 5	cvrat4	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\to \left(\left(X\ne \underset{\dot{}}{0}\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to \exists r\in A\left(r\underset{\dot{}}{\le }X\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right)\right)$$
7		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
8	7	ad2antrr	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\wedge r\in A\right)\to K\in \mathrm{Lat}$$
9		simplr3	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\wedge r\in A\right)\to Q\in A$$
10	1 5	atbase	$$⊢Q\in A\to Q\in B$$
11	9 10	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\wedge r\in A\right)\to Q\in B$$
12	1 5	atbase	$$⊢r\in A\to r\in B$$
13	12	adantl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\wedge r\in A\right)\to r\in B$$
14	1 3	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge Q\in B\wedge r\in B\right)\to Q\underset{\dot{}}{\vee }r=r\underset{\dot{}}{\vee }Q$$
15	8 11 13 14	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\wedge r\in A\right)\to Q\underset{\dot{}}{\vee }r=r\underset{\dot{}}{\vee }Q$$
16	15	breq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\wedge r\in A\right)\to \left(P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\leftrightarrow P\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }Q\right)\right)$$
17	16	anbi2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\wedge r\in A\right)\to \left(\left(r\underset{\dot{}}{\le }X\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(r\underset{\dot{}}{\le }X\wedge P\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }Q\right)\right)\right)$$
18	17	rexbidva	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\to \left(\exists r\in A\left(r\underset{\dot{}}{\le }X\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists r\in A\left(r\underset{\dot{}}{\le }X\wedge P\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }Q\right)\right)\right)$$
19	6 18	sylibd	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in B\wedge P\in A\wedge Q\in A\right)\right)\to \left(\left(X\ne \underset{\dot{}}{0}\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to \exists r\in A\left(r\underset{\dot{}}{\le }X\wedge P\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }Q\right)\right)\right)$$