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

Metamath Proof Explorer

Theorem lhpexle1

Description: There exists an atom under a co-atom different from any given element. (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses lhpex1.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpex1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpex1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexle1 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhpex1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 lhpex1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 1 2 3 lhpexle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑊 )
5 tru ⊢ ⊤
6 5 jctr ⊢ ( 𝑝 ≤ 𝑊 → ( 𝑝 ≤ 𝑊 ∧ ⊤ ) )
7 6 reximi ⊢ ( ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑊 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ) )
8 4 7 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ) )
9 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
10 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐴 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
13 12 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
14 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
15 1 14 2 3 lhplt ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ( lt ‘ 𝐾 ) 𝑊 )
16 11 14 2 2atlt ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑊 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) )
17 9 10 13 15 16 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) )
18 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑝 ( lt ‘ 𝐾 ) 𝑊 )
19 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝐾 ∈ HL )
20 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑝 ∈ 𝐴 )
21 simp1lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑊 ∈ 𝐻 )
22 1 14 pltle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑝 ( lt ‘ 𝐾 ) 𝑊 → 𝑝 ≤ 𝑊 ) )
23 19 20 21 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → ( 𝑝 ( lt ‘ 𝐾 ) 𝑊 → 𝑝 ≤ 𝑊 ) )
24 18 23 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑝 ≤ 𝑊 )
25 trud ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → ⊤ )
26 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑝 ≠ 𝑋 )
27 24 25 26 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) )
28 27 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) → ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) ) )
29 28 reximdva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) ) )
30 17 29 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) )
31 8 30 lhpexle1lem ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) )
32 3simpb ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) → ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )
33 32 reximi ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )
34 31 33 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )