Metamath Proof Explorer

Theorem cdleme

Description: Lemma E in Crawley p. 113. If p,q are atoms not under hyperplane w, then there is a unique translation f such that f(p) = q. (Contributed by NM, 11-Apr-2013)

Ref Expression
Hypotheses cdleme.l 
|- .<_ = ( le ` K )
cdleme.a 
|- A = ( Atoms ` K )
cdleme.h 
|- H = ( LHyp ` K )
cdleme.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion cdleme 
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> E! f e. T ( f ` P ) = Q )

Proof

Step Hyp Ref Expression
1 cdleme.l 
 |-  .<_ = ( le ` K )
2 cdleme.a 
 |-  A = ( Atoms ` K )
3 cdleme.h 
 |-  H = ( LHyp ` K )
4 cdleme.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 1 2 3 4 cdleme50ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> E. f e. T ( f ` P ) = Q )
6 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f e. T /\ z e. T ) /\ ( ( f ` P ) = Q /\ ( z ` P ) = Q ) ) -> ( K e. HL /\ W e. H ) )
7 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f e. T /\ z e. T ) /\ ( ( f ` P ) = Q /\ ( z ` P ) = Q ) ) -> f e. T )
8 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f e. T /\ z e. T ) /\ ( ( f ` P ) = Q /\ ( z ` P ) = Q ) ) -> z e. T )
9 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f e. T /\ z e. T ) /\ ( ( f ` P ) = Q /\ ( z ` P ) = Q ) ) -> ( P e. A /\ -. P .<_ W ) )
10 eqtr3 
 |-  ( ( ( f ` P ) = Q /\ ( z ` P ) = Q ) -> ( f ` P ) = ( z ` P ) )
11 10 3ad2ant3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f e. T /\ z e. T ) /\ ( ( f ` P ) = Q /\ ( z ` P ) = Q ) ) -> ( f ` P ) = ( z ` P ) )
12 1 2 3 4 cdlemd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ z e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( f ` P ) = ( z ` P ) ) -> f = z )
13 6 7 8 9 11 12 syl311anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f e. T /\ z e. T ) /\ ( ( f ` P ) = Q /\ ( z ` P ) = Q ) ) -> f = z )
14 13 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( f e. T /\ z e. T ) -> ( ( ( f ` P ) = Q /\ ( z ` P ) = Q ) -> f = z ) ) )
15 14 ralrimivv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> A. f e. T A. z e. T ( ( ( f ` P ) = Q /\ ( z ` P ) = Q ) -> f = z ) )
16 fveq1 
 |-  ( f = z -> ( f ` P ) = ( z ` P ) )
17 16 eqeq1d 
 |-  ( f = z -> ( ( f ` P ) = Q <-> ( z ` P ) = Q ) )
18 17 reu4 
 |-  ( E! f e. T ( f ` P ) = Q <-> ( E. f e. T ( f ` P ) = Q /\ A. f e. T A. z e. T ( ( ( f ` P ) = Q /\ ( z ` P ) = Q ) -> f = z ) ) )
19 5 15 18 sylanbrc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> E! f e. T ( f ` P ) = Q )