Theorem cdleme1b

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma showing F is a lattice element. F represents their f(r). (Contributed by NM, 6-Jun-2012)

	Ref	Expression
Hypotheses	cdleme1.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme1.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme1.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme1.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	cdleme1.f	⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
	cdleme1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
Assertion	cdleme1b	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐹 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme1.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme1.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme1.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		cdleme1.f	⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
8		cdleme1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
9		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
10	9	ad2antrr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
11		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
12	8 4	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵 )
13	11 12	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐵 )
14	1 2 3 4 5 6 8	cdleme0aa	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑈 ∈ 𝐵 )
15	14	3adant3r3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑈 ∈ 𝐵 )
16	8 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) → ( 𝑅 ∨ 𝑈 ) ∈ 𝐵 )
17	10 13 15 16	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑈 ) ∈ 𝐵 )
18		simpr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
19	8 4	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
20	18 19	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐵 )
21		simpr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
22	8 4	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
23	21 22	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐵 )
24	8 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑅 ) ∈ 𝐵 )
25	10 23 13 24	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑅 ) ∈ 𝐵 )
26	8 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
27	26	ad2antlr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑊 ∈ 𝐵 )
28	8 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑅 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ 𝐵 )
29	10 25 27 28	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ 𝐵 )
30	8 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ 𝐵 )
31	10 20 29 30	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ 𝐵 )
32	8 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑈 ) ∈ 𝐵 ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ 𝐵 ) → ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ∈ 𝐵 )
33	10 17 31 32	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ∈ 𝐵 )
34	7 33	eqeltrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐹 ∈ 𝐵 )