# Metamath Proof Explorer

## Theorem cdleme3c

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 6-Jun-2012)

Ref Expression
Hypotheses cdleme1.l
cdleme1.j
cdleme1.m
cdleme1.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdleme1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleme1.u
cdleme1.f
cdleme3c.z
Assertion cdleme3c

### Proof

Step Hyp Ref Expression
1 cdleme1.l
2 cdleme1.j
3 cdleme1.m
4 cdleme1.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdleme1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdleme1.u
7 cdleme1.f
8 cdleme3c.z
9 simpll
10 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
12 simpr3l
13 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
14 13 4 atbase ${⊢}{R}\in {A}\to {R}\in {\mathrm{Base}}_{{K}}$
15 12 14 syl
16 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
18 13 8 op0cl
19 17 18 syl
20 13 2 latjcl
21 11 15 19 20 syl3anc
22 simpl
23 simpr1l
24 simpr2l
25 1 2 3 4 5 6 7 13 cdleme1b ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\right)\to {F}\in {\mathrm{Base}}_{{K}}$
26 22 23 24 12 25 syl13anc
27 13 2 latjcl
28 11 15 26 27 syl3anc
29 13 4 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
30 23 29 syl
31 13 4 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
32 24 31 syl
33 13 2 latjcl
34 11 30 32 33 syl3anc
35 13 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
37 13 1 3 latmle2
38 11 34 36 37 syl3anc
39 6 38 eqbrtrid
40 simpr3r
41 nbrne2
42 39 40 41 syl2anc
43 42 necomd
44 1 2 3 4 5 6 lhpat2
46 eqid ${⊢}{⋖}_{{K}}={⋖}_{{K}}$
47 2 46 4 atcvr1
48 9 12 45 47 syl3anc
49 43 48 mpbid
50 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$