# Metamath Proof Explorer

## Theorem olm12

Description: The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012)

Ref Expression
Hypotheses olm1.b
`|- B = ( Base ` K )`
olm1.m
`|- ./\ = ( meet ` K )`
olm1.u
`|- .1. = ( 1. ` K )`
Assertion olm12
`|- ( ( K e. OL /\ X e. B ) -> ( .1. ./\ X ) = X )`

### Proof

Step Hyp Ref Expression
1 olm1.b
` |-  B = ( Base ` K )`
2 olm1.m
` |-  ./\ = ( meet ` K )`
3 olm1.u
` |-  .1. = ( 1. ` K )`
4 ollat
` |-  ( K e. OL -> K e. Lat )`
` |-  ( ( K e. OL /\ X e. B ) -> K e. Lat )`
6 olop
` |-  ( K e. OL -> K e. OP )`
` |-  ( ( K e. OL /\ X e. B ) -> K e. OP )`
8 1 3 op1cl
` |-  ( K e. OP -> .1. e. B )`
9 7 8 syl
` |-  ( ( K e. OL /\ X e. B ) -> .1. e. B )`
10 simpr
` |-  ( ( K e. OL /\ X e. B ) -> X e. B )`
11 1 2 latmcom
` |-  ( ( K e. Lat /\ .1. e. B /\ X e. B ) -> ( .1. ./\ X ) = ( X ./\ .1. ) )`
12 5 9 10 11 syl3anc
` |-  ( ( K e. OL /\ X e. B ) -> ( .1. ./\ X ) = ( X ./\ .1. ) )`
13 1 2 3 olm11
` |-  ( ( K e. OL /\ X e. B ) -> ( X ./\ .1. ) = X )`
14 12 13 eqtrd
` |-  ( ( K e. OL /\ X e. B ) -> ( .1. ./\ X ) = X )`