Theorem cdlemeulpq

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 5-Dec-2012)

	Ref	Expression
Hypotheses	cdleme0.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme0.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme0.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme0.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion	cdlemeulpq	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme0.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme0.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme0.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme0.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
8	7	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
9		simprl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
10		simprr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
13	7 9 10 12	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
14	11 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
15	14	ad2antlr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
16	11 1 3	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑄 ) )
17	8 13 15 16	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑄 ) )
18	6 17	eqbrtrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) )