# Metamath Proof Explorer

## Theorem 3dimlem4OLDN

Description: Lemma for 3dim1 . (Contributed by NM, 25-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses 3dim0.j
3dim0.l
3dim0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion 3dimlem4OLDN

### Proof

Step Hyp Ref Expression
1 3dim0.j
2 3dim0.l
3 3dim0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 simp2l
5 simp2r
6 simp11
7 simp2l
8 simp12
9 simp13
10 simp3l
11 10 necomd
12 2 1 3 hlatexch2
13 6 7 8 9 11 12 syl131anc
14 1 3 hlatjcom
15 6 9 7 14 syl3anc
16 15 breq2d
17 13 16 sylibrd
19 5 18 mtod
20 simp3
21 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
22 6 21 syl
23 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
24 23 3 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
25 9 24 syl
26 23 3 atbase ${⊢}{R}\in {A}\to {R}\in {\mathrm{Base}}_{{K}}$
27 7 26 syl
28 23 3 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
29 8 28 syl
30 23 1 latjrot
31 22 25 27 29 30 syl13anc
32 31 breq2d
33 simp2r
34 23 1 3 hlatjcl
35 6 9 7 34 syl3anc
36 simp3r
37 23 2 1 3 hlexch1
38 6 33 8 35 36 37 syl131anc
39 32 38 sylbird