# Metamath Proof Explorer

## Theorem cdlemc2

Description: Part of proof of Lemma C in Crawley p. 112. (Contributed by NM, 25-May-2012)

Ref Expression
Hypotheses cdlemc2.l
cdlemc2.j
cdlemc2.m
cdlemc2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemc2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemc2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
Assertion cdlemc2

### Proof

Step Hyp Ref Expression
1 cdlemc2.l
2 cdlemc2.j
3 cdlemc2.m
4 cdlemc2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdlemc2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdlemc2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
7 simp1l
8 simp3ll
9 simp3rl
10 1 2 4 hlatlej2
11 7 8 9 10 syl3anc
12 simp1
13 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
14 13 4 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
15 9 14 syl
16 simp3l
17 13 1 2 3 4 5 cdlemc1
18 12 15 16 17 syl3anc
19 11 18 breqtrrd
20 simp2
21 7 hllatd
22 13 4 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
23 8 22 syl
24 13 2 latjcl
25 21 23 15 24 syl3anc
26 simp1r
27 13 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
28 26 27 syl
29 13 3 latmcl
30 21 25 28 29 syl3anc
31 13 2 latjcl
32 21 23 30 31 syl3anc
33 13 1 5 6 ltrnle
34 12 20 15 32 33 syl112anc
35 19 34 mpbid
36 13 2 5 6 ltrnj
37 12 20 23 30 36 syl112anc
38 13 1 3 latmle2
39 21 25 28 38 syl3anc
40 13 1 5 6 ltrnval1
41 12 20 30 39 40 syl112anc
42 41 oveq2d
43 37 42 eqtrd
44 35 43 breqtrd