Metamath Proof Explorer

Theorem cdlemedb

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. D represents s_2. (Contributed by NM, 20-Nov-2012)

Ref Expression
Hypotheses cdlemeda.l ⊢ ≤ ˙ = ≤ K
cdlemeda.j ⊢ ∨ ˙ = join ⁡ K
cdlemeda.m ⊢ ∧ ˙ = meet ⁡ K
cdlemeda.a ⊢ A = Atoms ⁡ K
cdlemeda.h ⊢ H = LHyp ⁡ K
cdlemeda.d ⊢ D = R ∨ ˙ S ∧ ˙ W
cdlemedb.b ⊢ B = Base K
Assertion cdlemedb ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → D ∈ B

Proof

Step Hyp Ref Expression
1 cdlemeda.l ⊢ ≤ ˙ = ≤ K
2 cdlemeda.j ⊢ ∨ ˙ = join ⁡ K
3 cdlemeda.m ⊢ ∧ ˙ = meet ⁡ K
4 cdlemeda.a ⊢ A = Atoms ⁡ K
5 cdlemeda.h ⊢ H = LHyp ⁡ K
6 cdlemeda.d ⊢ D = R ∨ ˙ S ∧ ˙ W
7 cdlemedb.b ⊢ B = Base K
8 hllat ⊢ K ∈ HL → K ∈ Lat
9 8 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → K ∈ Lat
10 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → K ∈ HL
11 simprl ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → R ∈ A
12 simprr ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → S ∈ A
13 7 2 4 hlatjcl ⊢ K ∈ HL ∧ R ∈ A ∧ S ∈ A → R ∨ ˙ S ∈ B
14 10 11 12 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → R ∨ ˙ S ∈ B
15 7 5 lhpbase ⊢ W ∈ H → W ∈ B
16 15 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → W ∈ B
17 7 3 latmcl ⊢ K ∈ Lat ∧ R ∨ ˙ S ∈ B ∧ W ∈ B → R ∨ ˙ S ∧ ˙ W ∈ B
18 9 14 16 17 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → R ∨ ˙ S ∧ ˙ W ∈ B
19 6 18 eqeltrid ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ A ∧ S ∈ A → D ∈ B