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

Metamath Proof Explorer

Theorem 2atneat

Description: The join of two distinct atoms is not an atom. (Contributed by NM, 12-Oct-2012)

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

Proof

Step Hyp Ref Expression
1 2atneat.j 
 |-  .\/ = ( join ` K )
2 2atneat.a 
 |-  A = ( Atoms ` K )
3 simpl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) ) -> K e. HL )
4 simpr1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) ) -> P e. A )
5 simpr2 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) ) -> Q e. A )
6 simpr3 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) ) -> P =/= Q )
7 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
8 1 2 7 llni2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. ( LLines ` K ) )
9 3 4 5 6 8 syl31anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) ) -> ( P .\/ Q ) e. ( LLines ` K ) )
10 2 7 llnneat 
 |-  ( ( K e. HL /\ ( P .\/ Q ) e. ( LLines ` K ) ) -> -. ( P .\/ Q ) e. A )
11 9 10 syldan 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ P =/= Q ) ) -> -. ( P .\/ Q ) e. A )