# Metamath Proof Explorer

## Theorem ltrnel

Description: The lattice translation of an atom not under the fiducial co-atom is also an atom not under the fiducial co-atom. Remark below Lemma B in Crawley p. 112. (Contributed by NM, 22-May-2012)

Ref Expression
Hypotheses ltrnel.l
ltrnel.a $⊢ A = Atoms ⁡ K$
ltrnel.h $⊢ H = LHyp ⁡ K$
ltrnel.t $⊢ T = LTrn ⁡ K ⁡ W$
Assertion ltrnel

### Proof

Step Hyp Ref Expression
1 ltrnel.l
2 ltrnel.a $⊢ A = Atoms ⁡ K$
3 ltrnel.h $⊢ H = LHyp ⁡ K$
4 ltrnel.t $⊢ T = LTrn ⁡ K ⁡ W$
5 simp3l
6 eqid $⊢ Base K = Base K$
7 6 2 atbase $⊢ P ∈ A → P ∈ Base K$
9 6 2 3 4 ltrnatb $⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ Base K → P ∈ A ↔ F ⁡ P ∈ A$
10 8 9 syl3an3
11 5 10 mpbid
12 simp3r
13 simp1
14 simp2
15 5 7 syl
16 simp1r
17 6 3 lhpbase $⊢ W ∈ H → W ∈ Base K$
18 16 17 syl
19 6 1 3 4 ltrnle
20 13 14 15 18 19 syl112anc
21 simp1l
22 21 hllatd
23 6 1 latref
24 22 18 23 syl2anc
25 6 1 3 4 ltrnval1
26 13 14 18 24 25 syl112anc
27 26 breq2d
28 20 27 bitrd
29 12 28 mtbid
30 11 29 jca