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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemftr.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemftr.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemftr.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemftr3 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemftr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemftr.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 cdlemftr.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 cdlemftr.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7 5 6 2 lhpexle3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) )
8 df-rex ⊢ ( ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) )
9 7 8 sylib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑢 ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) )
10 1 5 6 2 3 4 cdlemfnid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ( le ‘ 𝐾 ) 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) = 𝑢 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) )
11 10 adantrrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) ) → ∃ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) = 𝑢 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) )
12 eqcom ⊢ ( ( 𝑅 ‘ 𝑓 ) = 𝑢 ↔ 𝑢 = ( 𝑅 ‘ 𝑓 ) )
13 12 anbi1i ⊢ ( ( ( 𝑅 ‘ 𝑓 ) = 𝑢 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ↔ ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) )
14 13 rexbii ⊢ ( ∃ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) = 𝑢 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ↔ ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) )
15 11 14 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) )
16 simprrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) ) → ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) )
17 15 16 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) ) → ( ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) )
18 17 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) → ( ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) )
19 18 eximdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ∃ 𝑢 ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) → ∃ 𝑢 ( ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) )
20 9 19 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑢 ( ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) )
21 rexcom4 ⊢ ( ∃ 𝑓 ∈ 𝑇 ∃ 𝑢 ( ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ∃ 𝑢 ∃ 𝑓 ∈ 𝑇 ( ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) )
22 anass ⊢ ( ( ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) )
23 22 exbii ⊢ ( ∃ 𝑢 ( ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ∃ 𝑢 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) )
24 fvex ⊢ ( 𝑅 ‘ 𝑓 ) ∈ V
25 neeq1 ⊢ ( 𝑢 = ( 𝑅 ‘ 𝑓 ) → ( 𝑢 ≠ 𝑋 ↔ ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ) )
26 neeq1 ⊢ ( 𝑢 = ( 𝑅 ‘ 𝑓 ) → ( 𝑢 ≠ 𝑌 ↔ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ) )
27 neeq1 ⊢ ( 𝑢 = ( 𝑅 ‘ 𝑓 ) → ( 𝑢 ≠ 𝑍 ↔ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) )
28 25 26 27 3anbi123d ⊢ ( 𝑢 = ( 𝑅 ‘ 𝑓 ) → ( ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ↔ ( ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) ) )
29 28 anbi2d ⊢ ( 𝑢 = ( 𝑅 ‘ 𝑓 ) → ( ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) ) ) )
30 24 29 ceqsexv ⊢ ( ∃ 𝑢 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ) ↔ ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) ) )
31 23 30 bitri ⊢ ( ∃ 𝑢 ( ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) ) )
32 31 rexbii ⊢ ( ∃ 𝑓 ∈ 𝑇 ∃ 𝑢 ( ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) ) )
33 r19.41v ⊢ ( ∃ 𝑓 ∈ 𝑇 ( ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ( ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) )
34 33 exbii ⊢ ( ∃ 𝑢 ∃ 𝑓 ∈ 𝑇 ( ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ∃ 𝑢 ( ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) )
35 21 32 34 3bitr3ri ⊢ ( ∃ 𝑢 ( ∃ 𝑓 ∈ 𝑇 ( 𝑢 = ( 𝑅 ‘ 𝑓 ) ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ≠ 𝑋 ∧ 𝑢 ≠ 𝑌 ∧ 𝑢 ≠ 𝑍 ) ) ↔ ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) ) )
36 20 35 sylib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅 ‘ 𝑓 ) ≠ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑌 ∧ ( 𝑅 ‘ 𝑓 ) ≠ 𝑍 ) ) )