This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemftr1

Description: Part of proof of Lemma G of Crawley p. 116, sixth line of third paragraph on p. 117: there is "a translation h, different from the identity, such that tr h =/= tr f." (Contributed by NM, 25-Jul-2013)

Ref Expression
Hypotheses cdlemftr.b 
|- B = ( Base ` K )
cdlemftr.h 
|- H = ( LHyp ` K )
cdlemftr.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemftr.r 
|- R = ( ( trL ` K ) ` W )
Assertion cdlemftr1 
|- ( ( K e. HL /\ W e. H ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X ) )

Proof

Step Hyp Ref Expression
1 cdlemftr.b 
 |-  B = ( Base ` K )
2 cdlemftr.h 
 |-  H = ( LHyp ` K )
3 cdlemftr.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 cdlemftr.r 
 |-  R = ( ( trL ` K ) ` W )
5 1 2 3 4 cdlemftr2 
 |-  ( ( K e. HL /\ W e. H ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X /\ ( R ` f ) =/= X ) )
6 3simpa 
 |-  ( ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X /\ ( R ` f ) =/= X ) -> ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X ) )
7 6 reximi 
 |-  ( E. f e. T ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X /\ ( R ` f ) =/= X ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X ) )
8 5 7 syl 
 |-  ( ( K e. HL /\ W e. H ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X ) )