# Metamath Proof Explorer

## Theorem cdlemd

Description: If two translations agree at any atom not under the fiducial co-atom W , then they are equal. Lemma D in Crawley p. 113. (Contributed by NM, 2-Jun-2012)

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

### Proof

Step Hyp Ref Expression
1 cdlemd.l
2 cdlemd.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 cdlemd.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 cdlemd.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
5 simpl11
6 simpl12
7 simpl13
8 6 7 jca
9 simpr
10 simpl2
11 simpl3
12 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
13 1 12 2 3 4 cdlemd9
14 5 8 9 10 11 13 syl311anc
15 14 ralrimiva
16 2 3 4 ltrneq2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to \left(\forall {q}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({q}\right)={G}\left({q}\right)↔{F}={G}\right)$
17 16 3ad2ant1
18 15 17 mpbid