Theorem 4atex2-0aOLDN

Description: Same as 4atex2 except that S is zero. (Contributed by NM, 27-May-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	4that.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	4that.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	4that.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	4that.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	4atex2-0aOLDN	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)$$

Proof

Step	Hyp	Ref	Expression
1		4that.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		4that.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		4that.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		4that.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		simp32l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to T\in A$$
6		simp32r	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \neg T\underset{\dot{}}{\le }W$$
7		simp1l	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to K\in \mathrm{HL}$$
8		hlol	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OL}$$
9	7 8	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to K\in \mathrm{OL}$$
10		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
11	10 3	atbase	$$⊢T\in A\to T\in {\mathrm{Base}}_K$$
12	5 11	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to T\in {\mathrm{Base}}_K$$
13		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
14	10 2 13	olj02	$$⊢\left(K\in \mathrm{OL}\wedge T\in {\mathrm{Base}}_K\right)\to \mathrm{0.}\left(K\right)\underset{\dot{}}{\vee }T=T$$
15	9 12 14	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \mathrm{0.}\left(K\right)\underset{\dot{}}{\vee }T=T$$
16		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to S=\mathrm{0.}\left(K\right)$$
17	16	oveq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to S\underset{\dot{}}{\vee }T=\mathrm{0.}\left(K\right)\underset{\dot{}}{\vee }T$$
18	2 3	hlatjidm	$$⊢\left(K\in \mathrm{HL}\wedge T\in A\right)\to T\underset{\dot{}}{\vee }T=T$$
19	7 5 18	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to T\underset{\dot{}}{\vee }T=T$$
20	15 17 19	3eqtr4d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to S\underset{\dot{}}{\vee }T=T\underset{\dot{}}{\vee }T$$
21		breq1	$$⊢z=T\to \left(z\underset{\dot{}}{\le }W\leftrightarrow T\underset{\dot{}}{\le }W\right)$$
22	21	notbid	$$⊢z=T\to \left(\neg z\underset{\dot{}}{\le }W\leftrightarrow \neg T\underset{\dot{}}{\le }W\right)$$
23		oveq2	$$⊢z=T\to S\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }T$$
24		oveq2	$$⊢z=T\to T\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }T$$
25	23 24	eqeq12d	$$⊢z=T\to \left(S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\leftrightarrow S\underset{\dot{}}{\vee }T=T\underset{\dot{}}{\vee }T\right)$$
26	22 25	anbi12d	$$⊢z=T\to \left(\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)\leftrightarrow \left(\neg T\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }T=T\underset{\dot{}}{\vee }T\right)\right)$$
27	26	rspcev	$$⊢\left(T\in A\wedge \left(\neg T\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }T=T\underset{\dot{}}{\vee }T\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)$$
28	5 6 20 27	syl12anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge S=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)$$