# Metamath Proof Explorer

## Theorem cdlemd6

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 31-May-2012)

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

### Proof

Step Hyp Ref Expression
1 cdlemd4.l
2 cdlemd4.j
3 cdlemd4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 cdlemd4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
5 cdlemd4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 simp3
7 6 oveq2d
8 7 oveq1d
9 simp1l
10 simp1rl
11 simp21
12 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
13 eqid ${⊢}\mathrm{trL}\left({K}\right)\left({W}\right)=\mathrm{trL}\left({K}\right)\left({W}\right)$
14 1 2 12 3 4 5 13 trlval2
15 9 10 11 14 syl3anc
16 simp1rr
17 1 2 12 3 4 5 13 trlval2
18 9 16 11 17 syl3anc
19 8 15 18 3eqtr4d
20 19 oveq2d
21 6 oveq1d
22 20 21 oveq12d
23 simp22
24 simp23
25 1 2 12 3 4 5 13 cdlemc
26 9 10 11 23 24 25 syl131anc
27 oveq2
28 27 breq2d
29 28 notbid
30 29 biimpd
31 6 24 30 sylc
32 1 2 12 3 4 5 13 cdlemc
33 9 16 11 23 31 32 syl131anc
34 22 26 33 3eqtr4d