Theorem lplnri1

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

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

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	islpln2ah	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) ) -> ( Y e. P <-> ( Q =/= R /\ -. S ( le ` K ) ( Q .\/ R ) ) ) )
7	6	biimp3a	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> ( Q =/= R /\ -. S ( le ` K ) ( Q .\/ R ) ) )
8	7	simpld	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> Q =/= R )