Metamath Proof Explorer

Theorem cdleme9b

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

Ref Expression
Hypotheses cdleme9b.b ⊢ B = Base K
cdleme9b.j ⊢ ∨ ˙ = join ⁡ K
cdleme9b.m ⊢ ∧ ˙ = meet ⁡ K
cdleme9b.a ⊢ A = Atoms ⁡ K
cdleme9b.h ⊢ H = LHyp ⁡ K
cdleme9b.c ⊢ C = P ∨ ˙ S ∧ ˙ W
Assertion cdleme9b ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ W ∈ H → C ∈ B

Proof

Step Hyp Ref Expression
1 cdleme9b.b ⊢ B = Base K
2 cdleme9b.j ⊢ ∨ ˙ = join ⁡ K
3 cdleme9b.m ⊢ ∧ ˙ = meet ⁡ K
4 cdleme9b.a ⊢ A = Atoms ⁡ K
5 cdleme9b.h ⊢ H = LHyp ⁡ K
6 cdleme9b.c ⊢ C = P ∨ ˙ S ∧ ˙ W
7 hllat ⊢ K ∈ HL → K ∈ Lat
8 7 adantr ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ W ∈ H → K ∈ Lat
9 1 2 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A → P ∨ ˙ S ∈ B
10 9 3adant3r3 ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ W ∈ H → P ∨ ˙ S ∈ B
11 simpr3 ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ W ∈ H → W ∈ H
12 1 5 lhpbase ⊢ W ∈ H → W ∈ B
13 11 12 syl ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ W ∈ H → W ∈ B
14 1 3 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ S ∈ B ∧ W ∈ B → P ∨ ˙ S ∧ ˙ W ∈ B
15 8 10 13 14 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ W ∈ H → P ∨ ˙ S ∧ ˙ W ∈ B
16 6 15 eqeltrid ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ W ∈ H → C ∈ B