# 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
`|- .<_ = ( le ` K )`
cdlemd.a
`|- A = ( Atoms ` K )`
cdlemd.h
`|- H = ( LHyp ` K )`
cdlemd.t
`|- T = ( ( LTrn ` K ) ` W )`
Assertion cdlemd
`|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) -> F = G )`

### Proof

Step Hyp Ref Expression
1 cdlemd.l
` |-  .<_ = ( le ` K )`
2 cdlemd.a
` |-  A = ( Atoms ` K )`
3 cdlemd.h
` |-  H = ( LHyp ` K )`
4 cdlemd.t
` |-  T = ( ( LTrn ` K ) ` W )`
5 simpl11
` |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) /\ q e. A ) -> ( K e. HL /\ W e. H ) )`
6 simpl12
` |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) /\ q e. A ) -> F e. T )`
7 simpl13
` |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) /\ q e. A ) -> G e. T )`
8 6 7 jca
` |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) /\ q e. A ) -> ( F e. T /\ G e. T ) )`
9 simpr
` |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) /\ q e. A ) -> q e. A )`
10 simpl2
` |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) /\ q e. A ) -> ( P e. A /\ -. P .<_ W ) )`
11 simpl3
` |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) /\ q e. A ) -> ( F ` P ) = ( G ` P ) )`
12 eqid
` |-  ( join ` K ) = ( join ` K )`
13 1 12 2 3 4 cdlemd9
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ q e. A ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) -> ( F ` q ) = ( G ` q ) )`
14 5 8 9 10 11 13 syl311anc
` |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) /\ q e. A ) -> ( F ` q ) = ( G ` q ) )`
15 14 ralrimiva
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) -> A. q e. A ( F ` q ) = ( G ` q ) )`
16 2 3 4 ltrneq2
` |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( A. q e. A ( F ` q ) = ( G ` q ) <-> F = G ) )`
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) -> ( A. q e. A ( F ` q ) = ( G ` q ) <-> F = G ) )`
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) -> F = G )`