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

Metamath Proof Explorer

Theorem olj02

Description: An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 olj0.b 
 |-  B = ( Base ` K )
2 olj0.j 
 |-  .\/ = ( join ` K )
3 olj0.z 
 |-  .0. = ( 0. ` 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 1 3 op0cl 
 |-  ( K e. OP -> .0. e. B )
8 6 7 syl 
 |-  ( K e. OL -> .0. e. B )
9 8 adantr 
 |-  ( ( K e. OL /\ X e. B ) -> .0. e. B )
10 simpr 
 |-  ( ( K e. OL /\ X e. B ) -> X e. B )
11 1 2 latjcom 
 |-  ( ( K e. Lat /\ .0. e. B /\ X e. B ) -> ( .0. .\/ X ) = ( X .\/ .0. ) )
12 5 9 10 11 syl3anc 
 |-  ( ( K e. OL /\ X e. B ) -> ( .0. .\/ X ) = ( X .\/ .0. ) )
13 1 2 3 olj01 
 |-  ( ( K e. OL /\ X e. B ) -> ( X .\/ .0. ) = X )
14 12 13 eqtrd 
 |-  ( ( K e. OL /\ X e. B ) -> ( .0. .\/ X ) = X )