This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐹 ∈ 𝐵 )