Theorem cdleme42a

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 3-Mar-2013)

	Ref	Expression
Hypotheses	cdleme42.b	$$⊢B={\mathrm{Base}}_K$$
	cdleme42.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme42.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme42.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme42.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme42.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme42.v	$$⊢V=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
Assertion	cdleme42a	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to R\underset{\dot{}}{\vee }S=R\underset{\dot{}}{\vee }V$$

Proof

Step	Hyp	Ref	Expression
1		cdleme42.b	$$⊢B={\mathrm{Base}}_K$$
2		cdleme42.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdleme42.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdleme42.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		cdleme42.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		cdleme42.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		cdleme42.v	$$⊢V=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
8		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
9	2 3 8 5 6	lhpjat2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to R\underset{\dot{}}{\vee }W=\mathrm{1.}\left(K\right)$$
10	9	3adant3	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to R\underset{\dot{}}{\vee }W=\mathrm{1.}\left(K\right)$$
11	10	oveq2d	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }W\right)=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)$$
12	7	oveq2i	$$⊢R\underset{\dot{}}{\vee }V=R\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
13		simp1l	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to K\in \mathrm{HL}$$
14		simp2l	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to R\in A$$
15		simp3l	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to S\in A$$
16	1 3 5	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge S\in A\right)\to R\underset{\dot{}}{\vee }S\in B$$
17	13 14 15 16	syl3anc	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to R\underset{\dot{}}{\vee }S\in B$$
18		simp1r	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to W\in H$$
19	1 6	lhpbase	$$⊢W\in H\to W\in B$$
20	18 19	syl	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to W\in B$$
21	2 3 5	hlatlej1	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge S\in A\right)\to R\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
22	13 14 15 21	syl3anc	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to R\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
23	1 2 3 4 5	atmod3i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(R\in A\wedge R\underset{\dot{}}{\vee }S\in B\wedge W\in B\right)\wedge R\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\to R\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }W\right)$$
24	13 14 17 20 22 23	syl131anc	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to R\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }W\right)$$
25	12 24	eqtr2id	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }W\right)=R\underset{\dot{}}{\vee }V$$
26		hlol	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OL}$$
27	13 26	syl	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to K\in \mathrm{OL}$$
28	1 4 8	olm11	$$⊢\left(K\in \mathrm{OL}\wedge R\underset{\dot{}}{\vee }S\in B\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=R\underset{\dot{}}{\vee }S$$
29	27 17 28	syl2anc	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=R\underset{\dot{}}{\vee }S$$
30	11 25 29	3eqtr3rd	$$⊢\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 \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to R\underset{\dot{}}{\vee }S=R\underset{\dot{}}{\vee }V$$