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

Metamath Proof Explorer

Theorem olj01

Description: An ortholattice element joined with zero equals itself. ( chj0 analog.) (Contributed by NM, 19-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 olj0.b 
 |-  B = ( Base ` K )
2 olj0.j 
 |-  .\/ = ( join ` K )
3 olj0.z 
 |-  .0. = ( 0. ` K )
4 olop 
 |-  ( K e. OL -> K e. OP )
5 1 3 op0cl 
 |-  ( K e. OP -> .0. e. B )
6 4 5 syl 
 |-  ( K e. OL -> .0. e. B )
7 6 adantr 
 |-  ( ( K e. OL /\ X e. B ) -> .0. e. B )
8 eqid 
 |-  ( le ` K ) = ( le ` K )
9 ollat 
 |-  ( K e. OL -> K e. Lat )
10 9 3ad2ant1 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> K e. Lat )
11 1 2 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ .0. e. B ) -> ( X .\/ .0. ) e. B )
12 9 11 syl3an1 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> ( X .\/ .0. ) e. B )
13 simp2 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> X e. B )
14 1 8 latref 
 |-  ( ( K e. Lat /\ X e. B ) -> X ( le ` K ) X )
15 9 14 sylan 
 |-  ( ( K e. OL /\ X e. B ) -> X ( le ` K ) X )
16 15 3adant3 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> X ( le ` K ) X )
17 1 8 3 op0le 
 |-  ( ( K e. OP /\ X e. B ) -> .0. ( le ` K ) X )
18 4 17 sylan 
 |-  ( ( K e. OL /\ X e. B ) -> .0. ( le ` K ) X )
19 18 3adant3 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> .0. ( le ` K ) X )
20 simp3 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> .0. e. B )
21 1 8 2 latjle12 
 |-  ( ( K e. Lat /\ ( X e. B /\ .0. e. B /\ X e. B ) ) -> ( ( X ( le ` K ) X /\ .0. ( le ` K ) X ) <-> ( X .\/ .0. ) ( le ` K ) X ) )
22 10 13 20 13 21 syl13anc 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> ( ( X ( le ` K ) X /\ .0. ( le ` K ) X ) <-> ( X .\/ .0. ) ( le ` K ) X ) )
23 16 19 22 mpbi2and 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> ( X .\/ .0. ) ( le ` K ) X )
24 1 8 2 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ .0. e. B ) -> X ( le ` K ) ( X .\/ .0. ) )
25 9 24 syl3an1 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> X ( le ` K ) ( X .\/ .0. ) )
26 1 8 10 12 13 23 25 latasymd 
 |-  ( ( K e. OL /\ X e. B /\ .0. e. B ) -> ( X .\/ .0. ) = X )
27 7 26 mpd3an3 
 |-  ( ( K e. OL /\ X e. B ) -> ( X .\/ .0. ) = X )