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 ) ) )