Theorem lplnllnneN

Description: Two lattice lines defined by atoms defining a lattice plane are not equal. (Contributed by NM, 9-Oct-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	lplnllnneN	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> ( Q .\/ S ) =/= ( 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		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		simpl1	|- ( ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) /\ ( Q .\/ S ) = ( R .\/ S ) ) -> K e. HL )
8		simpl21	|- ( ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) /\ ( Q .\/ S ) = ( R .\/ S ) ) -> Q e. A )
9		simpl23	|- ( ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) /\ ( Q .\/ S ) = ( R .\/ S ) ) -> S e. A )
10	5 1 2	hlatlej1	|- ( ( K e. HL /\ Q e. A /\ S e. A ) -> Q ( le ` K ) ( Q .\/ S ) )
11	7 8 9 10	syl3anc	|- ( ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) /\ ( Q .\/ S ) = ( R .\/ S ) ) -> Q ( le ` K ) ( Q .\/ S ) )
12		simpr	|- ( ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) /\ ( Q .\/ S ) = ( R .\/ S ) ) -> ( Q .\/ S ) = ( R .\/ S ) )
13	11 12	breqtrd	|- ( ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) /\ ( Q .\/ S ) = ( R .\/ S ) ) -> Q ( le ` K ) ( R .\/ S ) )
14	13	ex	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> ( ( Q .\/ S ) = ( R .\/ S ) -> Q ( le ` K ) ( R .\/ S ) ) )
15	14	necon3bd	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> ( -. Q ( le ` K ) ( R .\/ S ) -> ( Q .\/ S ) =/= ( R .\/ S ) ) )
16	6 15	mpd	|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> ( Q .\/ S ) =/= ( R .\/ S ) )