# Metamath Proof Explorer

## Theorem cdleme35f

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013)

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

### Proof

Step Hyp Ref Expression
1 cdleme35.l
2 cdleme35.j
3 cdleme35.m
4 cdleme35.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdleme35.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdleme35.u
7 cdleme35.f
8 simp11l
9 simp12l
10 simp2rl
11 2 4 hlatjcom
12 8 9 10 11 syl3anc
13 12 oveq2d
14 simp11
15 simp12
16 simp13l
17 simp2l
18 1 2 3 4 5 6 cdleme0a
19 14 15 16 17 18 syl112anc
20 simp12r
21 8 hllatd
22 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
23 22 2 4 hlatjcl
24 8 9 16 23 syl3anc
25 simp11r
26 22 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
27 25 26 syl
28 22 1 3 latmle2
29 21 24 27 28 syl3anc
30 6 29 eqbrtrid
31 breq1
32 30 31 syl5ibcom
33 32 necon3bd
34 20 33 mpd
35 simp3
36 22 1 3 latmle1
37 21 24 27 36 syl3anc
38 6 37 eqbrtrid
39 1 2 4 hlatlej1
40 8 9 16 39 syl3anc
41 22 4 atbase ${⊢}{U}\in {A}\to {U}\in {\mathrm{Base}}_{{K}}$
42 19 41 syl
43 22 4 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
44 9 43 syl
45 22 1 2 latjle12
46 21 42 44 24 45 syl13anc
47 38 40 46 mpbi2and
48 22 4 atbase ${⊢}{R}\in {A}\to {R}\in {\mathrm{Base}}_{{K}}$
49 10 48 syl
50 22 2 4 hlatjcl
51 8 19 9 50 syl3anc
52 22 1 lattr
53 21 49 51 24 52 syl13anc
54 47 53 mpan2d
55 35 54 mtod
56 1 2 3 4 2llnma2
57 8 19 9 10 34 55 56 syl132anc
58 13 57 eqtrd