Metamath Proof Explorer

Theorem cdlemftr3

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

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 eqid 
 |-  ( le ` K ) = ( le ` K )
6 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
7 5 6 2 lhpexle3 
 |-  ( ( K e. HL /\ W e. H ) -> E. u e. ( Atoms ` K ) ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) )
8 df-rex 
 |-  ( E. u e. ( Atoms ` K ) ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> E. u ( u e. ( Atoms ` K ) /\ ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) )
9 7 8 sylib 
 |-  ( ( K e. HL /\ W e. H ) -> E. u ( u e. ( Atoms ` K ) /\ ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) )
10 1 5 6 2 3 4 cdlemfnid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( u e. ( Atoms ` K ) /\ u ( le ` K ) W ) ) -> E. f e. T ( ( R ` f ) = u /\ f =/= ( _I |` B ) ) )
11 10 adantrrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( u e. ( Atoms ` K ) /\ ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) ) -> E. f e. T ( ( R ` f ) = u /\ f =/= ( _I |` B ) ) )
12 eqcom 
 |-  ( ( R ` f ) = u <-> u = ( R ` f ) )
13 12 anbi1i 
 |-  ( ( ( R ` f ) = u /\ f =/= ( _I |` B ) ) <-> ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) )
14 13 rexbii 
 |-  ( E. f e. T ( ( R ` f ) = u /\ f =/= ( _I |` B ) ) <-> E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) )
15 11 14 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( u e. ( Atoms ` K ) /\ ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) ) -> E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) )
16 simprrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( u e. ( Atoms ` K ) /\ ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) ) -> ( u =/= X /\ u =/= Y /\ u =/= Z ) )
17 15 16 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( u e. ( Atoms ` K ) /\ ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) ) -> ( E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) )
18 17 ex 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( u e. ( Atoms ` K ) /\ ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) -> ( E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) )
19 18 eximdv 
 |-  ( ( K e. HL /\ W e. H ) -> ( E. u ( u e. ( Atoms ` K ) /\ ( u ( le ` K ) W /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) -> E. u ( E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) )
20 9 19 mpd 
 |-  ( ( K e. HL /\ W e. H ) -> E. u ( E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) )
21 rexcom4 
 |-  ( E. f e. T E. u ( ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> E. u E. f e. T ( ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) )
22 anass 
 |-  ( ( ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> ( u = ( R ` f ) /\ ( f =/= ( _I |` B ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) )
23 22 exbii 
 |-  ( E. u ( ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> E. u ( u = ( R ` f ) /\ ( f =/= ( _I |` B ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) )
24 fvex 
 |-  ( R ` f ) e. _V
25 neeq1 
 |-  ( u = ( R ` f ) -> ( u =/= X <-> ( R ` f ) =/= X ) )
26 neeq1 
 |-  ( u = ( R ` f ) -> ( u =/= Y <-> ( R ` f ) =/= Y ) )
27 neeq1 
 |-  ( u = ( R ` f ) -> ( u =/= Z <-> ( R ` f ) =/= Z ) )
28 25 26 27 3anbi123d 
 |-  ( u = ( R ` f ) -> ( ( u =/= X /\ u =/= Y /\ u =/= Z ) <-> ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Z ) ) )
29 28 anbi2d 
 |-  ( u = ( R ` f ) -> ( ( f =/= ( _I |` B ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Z ) ) ) )
30 24 29 ceqsexv 
 |-  ( E. u ( u = ( R ` f ) /\ ( f =/= ( _I |` B ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) ) <-> ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Z ) ) )
31 23 30 bitri 
 |-  ( E. u ( ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Z ) ) )
32 31 rexbii 
 |-  ( E. f e. T E. u ( ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> E. f e. T ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Z ) ) )
33 r19.41v 
 |-  ( E. f e. T ( ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> ( E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) )
34 33 exbii 
 |-  ( E. u E. f e. T ( ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> E. u ( E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) )
35 21 32 34 3bitr3ri 
 |-  ( E. u ( E. f e. T ( u = ( R ` f ) /\ f =/= ( _I |` B ) ) /\ ( u =/= X /\ u =/= Y /\ u =/= Z ) ) <-> E. f e. T ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Z ) ) )
36 20 35 sylib 
 |-  ( ( K e. HL /\ W e. H ) -> E. f e. T ( f =/= ( _I |` B ) /\ ( ( R ` f ) =/= X /\ ( R ` f ) =/= Y /\ ( R ` f ) =/= Z ) ) )