Theorem cdleme9b

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

	Ref	Expression
Hypotheses	cdleme9b.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdleme9b.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme9b.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme9b.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme9b.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme9b.c	⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
Assertion	cdleme9b	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) → 𝐶 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cdleme9b.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdleme9b.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme9b.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme9b.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme9b.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme9b.c	⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
7		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
8	7	adantr	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) → 𝐾 ∈ Lat )
9	1 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ 𝐵 )
10	9	3adant3r3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ 𝐵 )
11		simpr3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) → 𝑊 ∈ 𝐻 )
12	1 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
13	11 12	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) → 𝑊 ∈ 𝐵 )
14	1 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 )
15	8 10 13 14	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 )
16	6 15	eqeltrid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) ) → 𝐶 ∈ 𝐵 )