Theorem 2atnelpln

Description: The join of two atoms is not a lattice plane. (Contributed by NM, 16-Jul-2012)

	Ref	Expression
Hypotheses	2atnelpln.j	|- .\/ = ( join ` K )
	2atnelpln.a	|- A = ( Atoms ` K )
	2atnelpln.p	|- P = ( LPlanes ` K )
Assertion	2atnelpln	|- ( ( K e. HL /\ Q e. A /\ R e. A ) -> -. ( Q .\/ R ) e. P )

Proof

Step	Hyp	Ref	Expression
1		2atnelpln.j	|- .\/ = ( join ` K )
2		2atnelpln.a	|- A = ( Atoms ` K )
3		2atnelpln.p	|- P = ( LPlanes ` K )
4		hllat	|- ( K e. HL -> K e. Lat )
5	4	3ad2ant1	|- ( ( K e. HL /\ Q e. A /\ R e. A ) -> K e. Lat )
6		eqid	|- ( Base ` K ) = ( Base ` K )
7	6 1 2	hlatjcl	|- ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
8		eqid	|- ( le ` K ) = ( le ` K )
9	6 8	latref	|- ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) ) -> ( Q .\/ R ) ( le ` K ) ( Q .\/ R ) )
10	5 7 9	syl2anc	|- ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) ( le ` K ) ( Q .\/ R ) )
11		simpl1	|- ( ( ( K e. HL /\ Q e. A /\ R e. A ) /\ ( Q .\/ R ) e. P ) -> K e. HL )
12		simpr	|- ( ( ( K e. HL /\ Q e. A /\ R e. A ) /\ ( Q .\/ R ) e. P ) -> ( Q .\/ R ) e. P )
13		simpl2	|- ( ( ( K e. HL /\ Q e. A /\ R e. A ) /\ ( Q .\/ R ) e. P ) -> Q e. A )
14		simpl3	|- ( ( ( K e. HL /\ Q e. A /\ R e. A ) /\ ( Q .\/ R ) e. P ) -> R e. A )
15	8 1 2 3	lplnnle2at	|- ( ( K e. HL /\ ( ( Q .\/ R ) e. P /\ Q e. A /\ R e. A ) ) -> -. ( Q .\/ R ) ( le ` K ) ( Q .\/ R ) )
16	11 12 13 14 15	syl13anc	|- ( ( ( K e. HL /\ Q e. A /\ R e. A ) /\ ( Q .\/ R ) e. P ) -> -. ( Q .\/ R ) ( le ` K ) ( Q .\/ R ) )
17	16	ex	|- ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( ( Q .\/ R ) e. P -> -. ( Q .\/ R ) ( le ` K ) ( Q .\/ R ) ) )
18	10 17	mt2d	|- ( ( K e. HL /\ Q e. A /\ R e. A ) -> -. ( Q .\/ R ) e. P )