Theorem lplnri3N

Description: Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lplnri1.j	|- .\/ = ( join ` K )
	lplnri1.a	|- A = ( Atoms ` K )
	lplnri1.p	|- P = ( LPlanes ` K )
	lplnri1.y	|- Y = ( ( Q .\/ R ) .\/ S )
Assertion	lplnri3N	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> R =/= S )

Proof

Step	Hyp	Ref	Expression
1		lplnri1.j	|- .\/ = ( join ` K )
2		lplnri1.a	|- A = ( Atoms ` K )
3		lplnri1.p	|- P = ( LPlanes ` K )
4		lplnri1.y	|- Y = ( ( Q .\/ R ) .\/ S )
5		simp1	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> K e. HL )
6		simp22	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> R e. A )
7		simp21	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> Q e. A )
8		simp23	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> S e. A )
9		eqid	|- ( le ` K ) = ( le ` K )
10	9 1 2 3 4	lplnribN	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> -. R ( le ` K ) ( Q .\/ S ) )
11	9 1 2	atnlej2	|- ( ( K e. HL /\ ( R e. A /\ Q e. A /\ S e. A ) /\ -. R ( le ` K ) ( Q .\/ S ) ) -> R =/= S )
12	5 6 7 8 10 11	syl131anc	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> R =/= S )