# Metamath Proof Explorer

## Theorem cdlemg17dN

Description: TODO: fix comment. (Contributed by NM, 9-May-2013) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 cdlemg12.l
2 cdlemg12.j
3 cdlemg12.m
4 cdlemg12.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdlemg12.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdlemg12.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
7 cdlemg12b.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
8 simp1
9 simp21
10 simpl1
11 simpl2
12 simpl3
13 simpr
14 1 2 3 4 5 6 7 trlval2
15 10 11 12 13 14 syl211anc
16 8 9 15 syl2anc
17 simp11
18 simp12
19 17 18 jca
20 simp22
21 simp13
22 simp23
23 simp33
24 simp31
25 simp32
26 1 2 3 4 5 6 7 cdlemg17b
27 19 9 20 21 22 23 24 25 26 syl323anc
28 27 oveq2d
29 28 oveq1d
30 16 29 eqtrd