Theorem islln2a

Description: The predicate "is a lattice line" in terms of atoms. (Contributed by NM, 15-Jul-2012)

	Ref	Expression
Hypotheses	islln2a.j	|- .\/ = ( join ` K )
	islln2a.a	|- A = ( Atoms ` K )
	islln2a.n	|- N = ( LLines ` K )
Assertion	islln2a	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( P .\/ Q ) e. N <-> P =/= Q ) )

Proof

Step	Hyp	Ref	Expression
1		islln2a.j	|- .\/ = ( join ` K )
2		islln2a.a	|- A = ( Atoms ` K )
3		islln2a.n	|- N = ( LLines ` K )
4		oveq1	|- ( P = Q -> ( P .\/ Q ) = ( Q .\/ Q ) )
5	1 2	hlatjidm	|- ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
6	5	3adant2	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( Q .\/ Q ) = Q )
7	4 6	sylan9eqr	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P = Q ) -> ( P .\/ Q ) = Q )
8	2 3	llnneat	|- ( ( K e. HL /\ Q e. N ) -> -. Q e. A )
9	8	adantlr	|- ( ( ( K e. HL /\ P e. A ) /\ Q e. N ) -> -. Q e. A )
10	9	ex	|- ( ( K e. HL /\ P e. A ) -> ( Q e. N -> -. Q e. A ) )
11	10	con2d	|- ( ( K e. HL /\ P e. A ) -> ( Q e. A -> -. Q e. N ) )
12	11	3impia	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> -. Q e. N )
13	12	adantr	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P = Q ) -> -. Q e. N )
14	7 13	eqneltrd	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P = Q ) -> -. ( P .\/ Q ) e. N )
15	14	ex	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P = Q -> -. ( P .\/ Q ) e. N ) )
16	15	necon2ad	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( P .\/ Q ) e. N -> P =/= Q ) )
17	1 2 3	llni2	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. N )
18	17	ex	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P =/= Q -> ( P .\/ Q ) e. N ) )
19	16 18	impbid	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( P .\/ Q ) e. N <-> P =/= Q ) )