# Metamath Proof Explorer

## Theorem cdlemg31b0N

Description: TODO: Fix comment. (Contributed by NM, 30-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)$
cdlemg31.n
Assertion cdlemg31b0N

### 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 cdlemg31.n
9 simp11
10 simp2ll
11 simp31l
12 simp2rl
13 simp12
14 9 13 jca
15 simp2l
16 simp13
17 simp33
18 1 4 5 6 7 trlat
19 14 15 16 17 18 syl112anc
20 simp2r
21 1 5 6 7 trlle
22 14 16 21 syl2anc
23 19 22 jca
24 simp31
25 simp32
26 25 necomd
27 1 2 4 5 lhp2atne
28 14 20 10 23 24 26 27 syl321anc
29 28 necomd
30 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
31 2 3 30 4 2atmat0
32 9 10 11 12 19 29 31 syl33anc
33 8 eleq1i
34 8 eqeq1i
35 33 34 orbi12i
36 32 35 sylibr