Theorem cdlemefs29pre00N

Description: FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat . (Contributed by NM, 27-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemefs29.b	$$⊢B={\mathrm{Base}}_K$$
	cdlemefs29.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemefs29.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemefs29.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdlemefs29.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemefs29.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	cdlemefs29pre00N	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge s\in A\right)\to \left(\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge s\underset{\dot{}}{\vee }\left(R\underset{\dot{}}{\wedge }W\right)=R\right)\leftrightarrow \left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(R\underset{\dot{}}{\wedge }W\right)=R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemefs29.b	$$⊢B={\mathrm{Base}}_K$$
2		cdlemefs29.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdlemefs29.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdlemefs29.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		cdlemefs29.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		cdlemefs29.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		breq1	$$⊢s=R\to \left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
8	1 2 3 4 5 6 7	cdlemefrs29pre00	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge s\in A\right)\to \left(\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge s\underset{\dot{}}{\vee }\left(R\underset{\dot{}}{\wedge }W\right)=R\right)\leftrightarrow \left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(R\underset{\dot{}}{\wedge }W\right)=R\right)\right)$$