Theorem cdleme42d

Description: Part of proof of Lemma E in Crawley p. 113. Match ( s .\/ ( x ./\ W ) ) = x . (Contributed by NM, 6-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	cdleme42d	$$⊢\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 }V\right)\underset{\dot{}}{\wedge }W\right)=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	7	oveq2i	$$⊢R\underset{\dot{}}{\vee }V=R\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
9	1 2 3 4 5 6 7	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$$
10	9	oveq1d	$$⊢\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 }W=\left(R\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\wedge }W$$
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 R\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)=R\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\wedge }W\right)$$
12	8 11	syl5req	$$⊢\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 }V\right)\underset{\dot{}}{\wedge }W\right)=R\underset{\dot{}}{\vee }V$$