Theorem 4atex2-0cOLDN

Description: Same as 4atex2 except that S and T are zero. TODO: do we need this one or 4atex2-0aOLDN or 4atex2-0bOLDN ? (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-0cOLDN	$$⊢\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 T=\mathrm{0.}\left(K\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		simp21l	$$⊢\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 T=\mathrm{0.}\left(K\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 P\in A$$
6		simp21r	$$⊢\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 T=\mathrm{0.}\left(K\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 P\underset{\dot{}}{\le }W$$
7		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 T=\mathrm{0.}\left(K\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)$$
8	7	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 T=\mathrm{0.}\left(K\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 }P=\mathrm{0.}\left(K\right)\underset{\dot{}}{\vee }P$$
9		simp32	$$⊢\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 T=\mathrm{0.}\left(K\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=\mathrm{0.}\left(K\right)$$
10	9	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 T=\mathrm{0.}\left(K\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 }P=\mathrm{0.}\left(K\right)\underset{\dot{}}{\vee }P$$
11	8 10	eqtr4d	$$⊢\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 T=\mathrm{0.}\left(K\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 }P=T\underset{\dot{}}{\vee }P$$
12		breq1	$$⊢z=P\to \left(z\underset{\dot{}}{\le }W\leftrightarrow P\underset{\dot{}}{\le }W\right)$$
13	12	notbid	$$⊢z=P\to \left(\neg z\underset{\dot{}}{\le }W\leftrightarrow \neg P\underset{\dot{}}{\le }W\right)$$
14		oveq2	$$⊢z=P\to S\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }P$$
15		oveq2	$$⊢z=P\to T\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }P$$
16	14 15	eqeq12d	$$⊢z=P\to \left(S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\leftrightarrow S\underset{\dot{}}{\vee }P=T\underset{\dot{}}{\vee }P\right)$$
17	13 16	anbi12d	$$⊢z=P\to \left(\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }P=T\underset{\dot{}}{\vee }P\right)\right)$$
18	17	rspcev	$$⊢\left(P\in A\wedge \left(\neg P\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }P=T\underset{\dot{}}{\vee }P\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)$$
19	5 6 11 18	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 T=\mathrm{0.}\left(K\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)$$