Metamath Proof Explorer


Theorem hlatlej1

Description: A join's first argument is less than or equal to the join. Special case of latlej1 to show an atom is on a line. (Contributed by NM, 15-May-2013)

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

Proof

Step Hyp Ref Expression
1 hlatlej.l
 |-  .<_ = ( le ` K )
2 hlatlej.j
 |-  .\/ = ( join ` K )
3 hlatlej.a
 |-  A = ( Atoms ` K )
4 hllat
 |-  ( K e. HL -> K e. Lat )
5 eqid
 |-  ( Base ` K ) = ( Base ` K )
6 5 3 atbase
 |-  ( P e. A -> P e. ( Base ` K ) )
7 5 3 atbase
 |-  ( Q e. A -> Q e. ( Base ` K ) )
8 5 1 2 latlej1
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> P .<_ ( P .\/ Q ) )
9 4 6 7 8 syl3an
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> P .<_ ( P .\/ Q ) )