Metamath Proof Explorer

Theorem lnnat

Description: A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 lnnat.j 
 |-  .\/ = ( join ` K )
2 lnnat.a 
 |-  A = ( Atoms ` K )
3 simpl1 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> K e. HL )
4 simpl2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> P e. A )
5 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
6 eqid 
 |-  (
7 5 6 2 atcvr0 
 |-  ( ( K e. HL /\ P e. A ) -> ( 0. ` K ) (
8 3 4 7 syl2anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( 0. ` K ) (
9 1 6 2 atcvr1 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> P (
10 9 biimpa 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> P (
11 hlop 
 |-  ( K e. HL -> K e. OP )
12 eqid 
 |-  ( Base ` K ) = ( Base ` K )
13 12 5 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
14 3 11 13 3syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( 0. ` K ) e. ( Base ` K ) )
15 12 2 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
16 4 15 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> P e. ( Base ` K ) )
17 3 hllatd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> K e. Lat )
18 simpl3 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> Q e. A )
19 12 2 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
20 18 19 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> Q e. ( Base ` K ) )
21 12 1 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
22 17 16 20 21 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. ( Base ` K ) )
23 12 6 cvrntr 
 |-  ( ( K e. HL /\ ( ( 0. ` K ) e. ( Base ` K ) /\ P e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) ) -> ( ( ( 0. ` K ) (  -. ( 0. ` K ) (
24 3 14 16 22 23 syl13anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( ( ( 0. ` K ) (  -. ( 0. ` K ) (
25 8 10 24 mp2and 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> -. ( 0. ` K ) (
26 simpll1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) /\ ( P .\/ Q ) e. A ) -> K e. HL )
27 5 6 2 atcvr0 
 |-  ( ( K e. HL /\ ( P .\/ Q ) e. A ) -> ( 0. ` K ) (
28 26 27 sylancom 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) /\ ( P .\/ Q ) e. A ) -> ( 0. ` K ) (
29 25 28 mtand 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> -. ( P .\/ Q ) e. A )
30 29 ex 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P =/= Q -> -. ( P .\/ Q ) e. A ) )
31 1 2 hlatjidm 
 |-  ( ( K e. HL /\ P e. A ) -> ( P .\/ P ) = P )
32 31 3adant3 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ P ) = P )
33 simp2 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> P e. A )
34 32 33 eqeltrd 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ P ) e. A )
35 oveq2 
 |-  ( P = Q -> ( P .\/ P ) = ( P .\/ Q ) )
36 35 eleq1d 
 |-  ( P = Q -> ( ( P .\/ P ) e. A <-> ( P .\/ Q ) e. A ) )
37 34 36 syl5ibcom 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P = Q -> ( P .\/ Q ) e. A ) )
38 37 necon3bd 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( -. ( P .\/ Q ) e. A -> P =/= Q ) )
39 30 38 impbid 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> -. ( P .\/ Q ) e. A ) )