Theorem cdlemedb

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. D represents s_2. (Contributed by NM, 20-Nov-2012)

	Ref	Expression
Hypotheses	cdlemeda.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemeda.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemeda.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemeda.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemeda.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemeda.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
	cdlemedb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
Assertion	cdlemedb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐷 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cdlemeda.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemeda.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemeda.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdlemeda.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemeda.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemeda.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
7		cdlemedb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
8		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9	8	ad2antrr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
10		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
11		simprl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
12		simprr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
13	7 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 )
14	10 11 12 13	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 )
15	7 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
16	15	ad2antlr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑊 ∈ 𝐵 )
17	7 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 )
18	9 14 16 17	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 )
19	6 18	eqeltrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐷 ∈ 𝐵 )