This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )