# Metamath Proof Explorer

## Theorem trlnle

Description: The atom not under the fiducial co-atom W is not less than the trace of a lattice translation. Part of proof of Lemma C in Crawley p. 112. (Contributed by NM, 26-May-2012)

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

### Proof

Step Hyp Ref Expression
1 trlne.l
2 trlne.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 trlne.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 trlne.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
5 trlne.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
6 simpl1l
7 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
8 6 7 syl
9 simpl3l
10 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
11 1 10 2 atnle0
12 8 9 11 syl2anc
13 simpl1
14 simpl3
15 simpl2
16 simpr
17 1 10 2 3 4 5 trl0
18 13 14 15 16 17 syl112anc
19 18 breq2d
20 12 19 mtbird
21 1 2 3 4 5 trlne
23 simpl1l
24 23 7 syl
25 simpl3l
26 simpl1
27 simpl3
28 simpl2
29 simpr
30 1 2 3 4 5 trlat
31 26 27 28 29 30 syl112anc
32 1 2 atncmp
33 24 25 31 32 syl3anc
34 22 33 mpbird
35 20 34 pm2.61dane