# Metamath Proof Explorer

## Theorem cdlemksel

Description: Part of proof of Lemma K of Crawley p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki ? (Contributed by NM, 26-Jun-2013)

Ref Expression
Hypotheses cdlemk.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemk.l
cdlemk.j
cdlemk.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemk.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemk.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemk.m
cdlemk.s
Assertion cdlemksel

### Proof

Step Hyp Ref Expression
1 cdlemk.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk.l
3 cdlemk.j
4 cdlemk.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdlemk.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdlemk.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
7 cdlemk.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
8 cdlemk.m
9 cdlemk.s
10 simp13
11 1 2 3 4 5 6 7 8 9 cdlemksv
12 10 11 syl
13 eqid
14 1 2 3 4 5 6 7 8 13 cdlemki
15 12 14 eqeltrd