Theorem 2llnma2rN

Description: Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 2-May-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2llnm.l	|- .<_ = ( le ` K )
	2llnm.j	|- .\/ = ( join ` K )
	2llnm.m	|- ./\ = ( meet ` K )
	2llnm.a	|- A = ( Atoms ` K )
Assertion	2llnma2rN	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ R ) ./\ ( Q .\/ R ) ) = R )

Proof

Step	Hyp	Ref	Expression
1		2llnm.l	|- .<_ = ( le ` K )
2		2llnm.j	|- .\/ = ( join ` K )
3		2llnm.m	|- ./\ = ( meet ` K )
4		2llnm.a	|- A = ( Atoms ` K )
5		simp1	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> K e. HL )
6		simp21	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> P e. A )
7		simp23	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> R e. A )
8	2 4	hlatjcom	|- ( ( K e. HL /\ P e. A /\ R e. A ) -> ( P .\/ R ) = ( R .\/ P ) )
9	5 6 7 8	syl3anc	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( P .\/ R ) = ( R .\/ P ) )
10		simp22	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> Q e. A )
11	2 4	hlatjcom	|- ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) = ( R .\/ Q ) )
12	5 10 7 11	syl3anc	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( Q .\/ R ) = ( R .\/ Q ) )
13	9 12	oveq12d	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ R ) ./\ ( Q .\/ R ) ) = ( ( R .\/ P ) ./\ ( R .\/ Q ) ) )
14	1 2 3 4	2llnma2	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( R .\/ P ) ./\ ( R .\/ Q ) ) = R )
15	13 14	eqtrd	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> ( ( P .\/ R ) ./\ ( Q .\/ R ) ) = R )