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 HL W H f 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 K = K
6 eqid Atoms K = Atoms K
7 5 6 2 lhpexle3 K HL W H u Atoms K u K W u X u Y u Z
8 df-rex u Atoms K u K W u X u Y u Z u u Atoms K u K W u X u Y u Z
9 7 8 sylib K HL W H u u Atoms K u K W u X u Y u Z
10 1 5 6 2 3 4 cdlemfnid K HL W H u Atoms K u K W f T R f = u f I B
11 10 adantrrr K HL W H u Atoms K u K W u X u Y u Z f 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 f T R f = u f I B f T u = R f f I B
15 11 14 sylib K HL W H u Atoms K u K W u X u Y u Z f T u = R f f I B
16 simprrr K HL W H u Atoms K u K W u X u Y u Z u X u Y u Z
17 15 16 jca K HL W H u Atoms K u K W u X u Y u Z f T u = R f f I B u X u Y u Z
18 17 ex K HL W H u Atoms K u K W u X u Y u Z f T u = R f f I B u X u Y u Z
19 18 eximdv K HL W H u u Atoms K u K W u X u Y u Z u f T u = R f f I B u X u Y u Z
20 9 19 mpd K HL W H u f T u = R f f I B u X u Y u Z
21 rexcom4 f T u u = R f f I B u X u Y u Z u f 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 u u = R f f I B u X u Y u Z u u = R f f I B u X u Y u Z
24 fvex R f 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 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 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 f T u u = R f f I B u X u Y u Z f T f I B R f X R f Y R f Z
33 r19.41v f T u = R f f I B u X u Y u Z f T u = R f f I B u X u Y u Z
34 33 exbii u f T u = R f f I B u X u Y u Z u f T u = R f f I B u X u Y u Z
35 21 32 34 3bitr3ri u f T u = R f f I B u X u Y u Z f T f I B R f X R f Y R f Z
36 20 35 sylib K HL W H f T f I B R f X R f Y R f Z