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

Metamath Proof Explorer

Theorem lplnnlt

Description: Two lattice planes cannot satisfy the less than relation. (Contributed by NM, 7-Jul-2012)

Ref Expression
Hypotheses lplnnlt.s ⊢ < = ( lt ‘ 𝐾 )
lplnnlt.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplnnlt ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ¬ 𝑋 < 𝑌 )

Proof

Step Hyp Ref Expression
1 lplnnlt.s ⊢ < = ( lt ‘ 𝐾 )
2 lplnnlt.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
3 1 pltirr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ¬ 𝑋 < 𝑋 )
4 3 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ¬ 𝑋 < 𝑋 )
5 breq2 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 < 𝑋 ↔ 𝑋 < 𝑌 ) )
6 5 notbid ⊢ ( 𝑋 = 𝑌 → ( ¬ 𝑋 < 𝑋 ↔ ¬ 𝑋 < 𝑌 ) )
7 4 6 syl5ibcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 = 𝑌 → ¬ 𝑋 < 𝑌 ) )
8 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 8 1 pltle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 < 𝑌 → 𝑋 ( le ‘ 𝐾 ) 𝑌 ) )
10 8 2 lplncmp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ 𝑋 = 𝑌 ) )
11 9 10 sylibd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 < 𝑌 → 𝑋 = 𝑌 ) )
12 11 necon3ad ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ≠ 𝑌 → ¬ 𝑋 < 𝑌 ) )
13 7 12 pm2.61dne ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ¬ 𝑋 < 𝑌 )