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 ` K )
	3atnelvol.a	|- A = ( Atoms ` K )
	3atnelvol.v	|- V = ( LVols ` K )
Assertion	2atnelvolN	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> -. ( P .\/ Q ) e. V )

Proof

Step	Hyp	Ref	Expression
1		3atnelvol.j	|- .\/ = ( join ` K )
2		3atnelvol.a	|- A = ( Atoms ` K )
3		3atnelvol.v	|- V = ( LVols ` K )
4	1 2	hlatjidm	|- ( ( K e. HL /\ P e. A ) -> ( P .\/ P ) = P )
5	4	3adant3	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ P ) = P )
6	5	oveq1d	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( P .\/ P ) .\/ Q ) = ( P .\/ Q ) )
7		simp1	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> K e. HL )
8		simp2	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> P e. A )
9		simp3	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> Q e. A )
10	1 2 3	3atnelvolN	|- ( ( K e. HL /\ ( P e. A /\ P e. A /\ Q e. A ) ) -> -. ( ( P .\/ P ) .\/ Q ) e. V )
11	7 8 8 9 10	syl13anc	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> -. ( ( P .\/ P ) .\/ Q ) e. V )
12	6 11	eqneltrrd	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> -. ( P .\/ Q ) e. V )