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

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 )
5 4 adantr 
 |-  ( ( K e. OL /\ X e. B ) -> K e. Lat )
6 olop 
 |-  ( K e. OL -> K e. OP )
7 6 adantr 
 |-  ( ( 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 )