Theorem 2atnelvolN

Description: The join of two atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	3atnelvol.j	⊢ ∨ = ( join ‘ 𝐾 )
	3atnelvol.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	3atnelvol.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion	2atnelvolN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		3atnelvol.j	⊢ ∨ = ( join ‘ 𝐾 )
2		3atnelvol.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		3atnelvol.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
4	1 2	hlatjidm	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑃 ) = 𝑃 )
5	4	3adant3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑃 ) = 𝑃 )
6	5	oveq1d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑃 ) ∨ 𝑄 ) = ( 𝑃 ∨ 𝑄 ) )
7		simp1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ HL )
8		simp2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
9		simp3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
10	1 2 3	3atnelvolN	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ¬ ( ( 𝑃 ∨ 𝑃 ) ∨ 𝑄 ) ∈ 𝑉 )
11	7 8 8 9 10	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ¬ ( ( 𝑃 ∨ 𝑃 ) ∨ 𝑄 ) ∈ 𝑉 )
12	6 11	eqneltrrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝑉 )