Metamath Proof Explorer


Theorem 2atmat0

Description: The meet of two unequal lines (expressed as joins of atoms) is an atom or zero. (Contributed by NM, 2-Dec-2012)

Ref Expression
Hypotheses 2atmatz.j
|- .\/ = ( join ` K )
2atmatz.m
|- ./\ = ( meet ` K )
2atmatz.z
|- .0. = ( 0. ` K )
2atmatz.a
|- A = ( Atoms ` K )
Assertion 2atmat0
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )

Proof

Step Hyp Ref Expression
1 2atmatz.j
 |-  .\/ = ( join ` K )
2 2atmatz.m
 |-  ./\ = ( meet ` K )
3 2atmatz.z
 |-  .0. = ( 0. ` K )
4 2atmatz.a
 |-  A = ( Atoms ` K )
5 simpl
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
6 simpr1
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> R e. A )
7 simpr2
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> S e. A )
8 7 orcd
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( S e. A \/ S = .0. ) )
9 simpr3
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( P .\/ Q ) =/= ( R .\/ S ) )
10 1 2 3 4 2at0mat0
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )
11 5 6 8 9 10 syl13anc
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) )