Theorem cdleme9b

Description: Utility lemma for Lemma E in Crawley p. 113. (Contributed by NM, 9-Oct-2012)

	Ref	Expression
Hypotheses	cdleme9b.b	|- B = ( Base ` K )
	cdleme9b.j	|- .\/ = ( join ` K )
	cdleme9b.m	|- ./\ = ( meet ` K )
	cdleme9b.a	|- A = ( Atoms ` K )
	cdleme9b.h	|- H = ( LHyp ` K )
	cdleme9b.c	|- C = ( ( P .\/ S ) ./\ W )
Assertion	cdleme9b	|- ( ( K e. HL /\ ( P e. A /\ S e. A /\ W e. H ) ) -> C e. B )

Proof

Step	Hyp	Ref	Expression
1		cdleme9b.b	|- B = ( Base ` K )
2		cdleme9b.j	|- .\/ = ( join ` K )
3		cdleme9b.m	|- ./\ = ( meet ` K )
4		cdleme9b.a	|- A = ( Atoms ` K )
5		cdleme9b.h	|- H = ( LHyp ` K )
6		cdleme9b.c	|- C = ( ( P .\/ S ) ./\ W )
7		hllat	|- ( K e. HL -> K e. Lat )
8	7	adantr	|- ( ( K e. HL /\ ( P e. A /\ S e. A /\ W e. H ) ) -> K e. Lat )
9	1 2 4	hlatjcl	|- ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) e. B )
10	9	3adant3r3	|- ( ( K e. HL /\ ( P e. A /\ S e. A /\ W e. H ) ) -> ( P .\/ S ) e. B )
11		simpr3	|- ( ( K e. HL /\ ( P e. A /\ S e. A /\ W e. H ) ) -> W e. H )
12	1 5	lhpbase	|- ( W e. H -> W e. B )
13	11 12	syl	|- ( ( K e. HL /\ ( P e. A /\ S e. A /\ W e. H ) ) -> W e. B )
14	1 3	latmcl	|- ( ( K e. Lat /\ ( P .\/ S ) e. B /\ W e. B ) -> ( ( P .\/ S ) ./\ W ) e. B )
15	8 10 13 14	syl3anc	|- ( ( K e. HL /\ ( P e. A /\ S e. A /\ W e. H ) ) -> ( ( P .\/ S ) ./\ W ) e. B )
16	6 15	eqeltrid	|- ( ( K e. HL /\ ( P e. A /\ S e. A /\ W e. H ) ) -> C e. B )