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

Metamath Proof Explorer

Theorem lvolnltN

Description: Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lvolnlt.s ⊢ < = ( lt ‘ 𝐾 )
lvolnlt.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lvolnltN ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑋 < 𝑌 )

Proof

Step Hyp Ref Expression
1 lvolnlt.s ⊢ < = ( lt ‘ 𝐾 )
2 lvolnlt.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
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 lvolcmp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ 𝑋 = 𝑌 ) )
11 9 10 sylibd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 < 𝑌 → 𝑋 = 𝑌 ) )
12 11 necon3ad ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ≠ 𝑌 → ¬ 𝑋 < 𝑌 ) )
13 7 12 pm2.61dne ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑋 < 𝑌 )