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

Metamath Proof Explorer

Theorem cdlemftr2

Description: Special case of cdlemf showing existence of non-identity translation with trace different from any 2 given lattice elements. (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 cdlemftr2 
|- ( ( K e. HL /\ W e. H ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X /\ ( R ` f ) =/= Y ) )

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 cdlemftr3 
 |-  ( ( K e. HL /\ W e. H ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Y ) ) )
6 simpl 
 |-  ( ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Y ) ) -> f =/= ( _I |` B ) )
7 simpr1 
 |-  ( ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Y ) ) -> ( R ` f ) =/= X )
8 simpr2 
 |-  ( ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Y ) ) -> ( R ` f ) =/= Y )
9 6 7 8 3jca 
 |-  ( ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Y ) ) -> ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X /\ ( R ` f ) =/= Y ) )
10 9 reximi 
 |-  ( E. f e. T ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Y ) ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X /\ ( R ` f ) =/= Y ) )
11 5 10 syl 
 |-  ( ( K e. HL /\ W e. H ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( R ` f ) =/= X /\ ( R ` f ) =/= Y ) )