# Metamath Proof Explorer

## Theorem olm11

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

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

### Proof

Step Hyp Ref Expression
1 olm1.b
|-  B = ( Base ` K )
2 olm1.m
|-  ./\ = ( meet ` K )
3 olm1.u
|-  .1. = ( 1. ` K )
4 olop
|-  ( K e. OL -> K e. OP )
|-  ( ( K e. OL /\ X e. B ) -> K e. OP )
6 eqid
|-  ( 0. ` K ) = ( 0. ` K )
7 eqid
|-  ( oc ` K ) = ( oc ` K )
8 6 3 7 opoc1
|-  ( K e. OP -> ( ( oc ` K ) ` .1. ) = ( 0. ` K ) )
9 5 8 syl
|-  ( ( K e. OL /\ X e. B ) -> ( ( oc ` K ) ` .1. ) = ( 0. ` K ) )
10 9 oveq2d
|-  ( ( K e. OL /\ X e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` .1. ) ) = ( ( ( oc ` K ) ` X ) ( join ` K ) ( 0. ` K ) ) )
11 1 7 opoccl
|-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
12 4 11 sylan
|-  ( ( K e. OL /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
13 eqid
|-  ( join ` K ) = ( join ` K )
14 1 13 6 olj01
|-  ( ( K e. OL /\ ( ( oc ` K ) ` X ) e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( 0. ` K ) ) = ( ( oc ` K ) ` X ) )
15 12 14 syldan
|-  ( ( K e. OL /\ X e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( 0. ` K ) ) = ( ( oc ` K ) ` X ) )
16 10 15 eqtrd
|-  ( ( K e. OL /\ X e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` .1. ) ) = ( ( oc ` K ) ` X ) )
17 16 fveq2d
|-  ( ( K e. OL /\ X e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` .1. ) ) ) = ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) )
18 1 3 op1cl
|-  ( K e. OP -> .1. e. B )
19 5 18 syl
|-  ( ( K e. OL /\ X e. B ) -> .1. e. B )
20 1 13 2 7 oldmj4
|-  ( ( K e. OL /\ X e. B /\ .1. e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` .1. ) ) ) = ( X ./\ .1. ) )
21 19 20 mpd3an3
|-  ( ( K e. OL /\ X e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` .1. ) ) ) = ( X ./\ .1. ) )
22 1 7 opococ
|-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) = X )
23 4 22 sylan
|-  ( ( K e. OL /\ X e. B ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) = X )
24 17 21 23 3eqtr3d
|-  ( ( K e. OL /\ X e. B ) -> ( X ./\ .1. ) = X )