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 ) )
17 16 3ad2ant1 
 |-  ( ( ( ( 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 ) )
18 15 17 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) -> F = G )