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 ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑋 ≤ 𝑃 )