Theorem lplnri2N

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	lplnri2N	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> Q =/= 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		eqid	|- ( le ` K ) = ( le ` K )
6	5 1 2 3 4	lplnriaN	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> -. Q ( le ` K ) ( R .\/ S ) )
7	5 1 2	atnlej2	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ -. Q ( le ` K ) ( R .\/ S ) ) -> Q =/= S )
8	6 7	syld3an3	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> Q =/= S )