# Metamath Proof Explorer

## Theorem olj01

Description: An ortholattice element joined with zero equals itself. ( chj0 analog.) (Contributed by NM, 19-Oct-2011)

Ref Expression
Hypotheses olj0.b
`|- B = ( Base ` K )`
olj0.j
`|- .\/ = ( join ` K )`
olj0.z
`|- .0. = ( 0. ` K )`
Assertion olj01
`|- ( ( K e. OL /\ X e. B ) -> ( X .\/ .0. ) = X )`

### Proof

Step Hyp Ref Expression
1 olj0.b
` |-  B = ( Base ` K )`
2 olj0.j
` |-  .\/ = ( join ` K )`
3 olj0.z
` |-  .0. = ( 0. ` K )`
4 olop
` |-  ( K e. OL -> K e. OP )`
5 1 3 op0cl
` |-  ( K e. OP -> .0. e. B )`
6 4 5 syl
` |-  ( K e. OL -> .0. e. B )`
` |-  ( ( K e. OL /\ X e. B ) -> .0. e. B )`
8 eqid
` |-  ( le ` K ) = ( le ` K )`
9 ollat
` |-  ( K e. OL -> K e. Lat )`
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> K e. Lat )`
11 1 2 latjcl
` |-  ( ( K e. Lat /\ X e. B /\ .0. e. B ) -> ( X .\/ .0. ) e. B )`
12 9 11 syl3an1
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> ( X .\/ .0. ) e. B )`
13 simp2
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> X e. B )`
14 1 8 latref
` |-  ( ( K e. Lat /\ X e. B ) -> X ( le ` K ) X )`
15 9 14 sylan
` |-  ( ( K e. OL /\ X e. B ) -> X ( le ` K ) X )`
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> X ( le ` K ) X )`
17 1 8 3 op0le
` |-  ( ( K e. OP /\ X e. B ) -> .0. ( le ` K ) X )`
18 4 17 sylan
` |-  ( ( K e. OL /\ X e. B ) -> .0. ( le ` K ) X )`
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> .0. ( le ` K ) X )`
20 simp3
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> .0. e. B )`
21 1 8 2 latjle12
` |-  ( ( K e. Lat /\ ( X e. B /\ .0. e. B /\ X e. B ) ) -> ( ( X ( le ` K ) X /\ .0. ( le ` K ) X ) <-> ( X .\/ .0. ) ( le ` K ) X ) )`
22 10 13 20 13 21 syl13anc
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> ( ( X ( le ` K ) X /\ .0. ( le ` K ) X ) <-> ( X .\/ .0. ) ( le ` K ) X ) )`
23 16 19 22 mpbi2and
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> ( X .\/ .0. ) ( le ` K ) X )`
24 1 8 2 latlej1
` |-  ( ( K e. Lat /\ X e. B /\ .0. e. B ) -> X ( le ` K ) ( X .\/ .0. ) )`
25 9 24 syl3an1
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> X ( le ` K ) ( X .\/ .0. ) )`
26 1 8 10 12 13 23 25 latasymd
` |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> ( X .\/ .0. ) = X )`
27 7 26 mpd3an3
` |-  ( ( K e. OL /\ X e. B ) -> ( X .\/ .0. ) = X )`