Theorem cdleme20y

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Hypotheses	cdleme20z.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme20z.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme20z.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme20z.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	cdleme20y	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(S\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }R\right)=R$$

Proof

Step	Hyp	Ref	Expression
1		cdleme20z.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme20z.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme20z.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdleme20z.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		simp1	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to K\in \mathrm{HL}$$
6		simp22	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\in A$$
7		simp23	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to T\in A$$
8		simp21	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\in A$$
9		simp3	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
10	1 2 3 4	2llnma2rN	$$⊢\left(K\in \mathrm{HL}\wedge \left(S\in A\wedge T\in A\wedge R\in A\right)\wedge \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(S\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }R\right)=R$$
11	5 6 7 8 9 10	syl131anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge S\in A\wedge T\in A\right)\wedge \left(S\ne T\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(S\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }R\right)=R$$