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

Metamath Proof Explorer

Theorem lvolnleat

Description: An atom cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012)

Ref Expression
Hypotheses lvolnleat.l ⊢ ≤ = ( le ‘ 𝐾 )
lvolnleat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lvolnleat.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lvolnleat ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑋 ≤ 𝑃 )

Proof

Step Hyp Ref Expression
1 lvolnleat.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lvolnleat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 lvolnleat.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
4 3simpa ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) )
5 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
6 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
7 1 6 2 3 lvolnle3at ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ) → ¬ 𝑋 ≤ ( ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) ( join ‘ 𝐾 ) 𝑃 ) )
8 4 5 5 5 7 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑋 ≤ ( ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) ( join ‘ 𝐾 ) 𝑃 ) )
9 6 2 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) = 𝑃 )
10 9 3adant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) = 𝑃 )
11 10 oveq1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) ( join ‘ 𝐾 ) 𝑃 ) = ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) )
12 11 10 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) ( join ‘ 𝐾 ) 𝑃 ) = 𝑃 )
13 12 breq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ≤ ( ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) ( join ‘ 𝐾 ) 𝑃 ) ↔ 𝑋 ≤ 𝑃 ) )
14 8 13 mtbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑋 ≤ 𝑃 )