This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )
5 4 adantr 
 |-  ( ( 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 )