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

Metamath Proof Explorer

Theorem cdlemftr0

Description: Special case of cdlemf showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013)

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

Proof

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