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

Metamath Proof Explorer

Theorem omllaw2N

Description: Variation of orthomodular law. Definition of OML law in Kalmbach p. 22. ( pjoml2i analog.) (Contributed by NM, 6-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses omllaw.b 
|- B = ( Base ` K )
omllaw.l 
|- .<_ = ( le ` K )
omllaw.j 
|- .\/ = ( join ` K )
omllaw.m 
|- ./\ = ( meet ` K )
omllaw.o 
|- ._|_ = ( oc ` K )
Assertion omllaw2N 
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( X .\/ ( ( ._|_ ` X ) ./\ Y ) ) = Y ) )

Proof

Step Hyp Ref Expression
1 omllaw.b 
 |-  B = ( Base ` K )
2 omllaw.l 
 |-  .<_ = ( le ` K )
3 omllaw.j 
 |-  .\/ = ( join ` K )
4 omllaw.m 
 |-  ./\ = ( meet ` K )
5 omllaw.o 
 |-  ._|_ = ( oc ` K )
6 1 2 3 4 5 omllaw 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> Y = ( X .\/ ( Y ./\ ( ._|_ ` X ) ) ) ) )
7 eqcom 
 |-  ( ( X .\/ ( ( ._|_ ` X ) ./\ Y ) ) = Y <-> Y = ( X .\/ ( ( ._|_ ` X ) ./\ Y ) ) )
8 omllat 
 |-  ( K e. OML -> K e. Lat )
9 8 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )
10 omlop 
 |-  ( K e. OML -> K e. OP )
11 1 5 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
12 10 11 sylan 
 |-  ( ( K e. OML /\ X e. B ) -> ( ._|_ ` X ) e. B )
13 12 3adant3 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
14 simp3 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )
15 1 4 latmcom 
 |-  ( ( K e. Lat /\ ( ._|_ ` X ) e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ./\ Y ) = ( Y ./\ ( ._|_ ` X ) ) )
16 9 13 14 15 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ./\ Y ) = ( Y ./\ ( ._|_ ` X ) ) )
17 16 oveq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .\/ ( ( ._|_ ` X ) ./\ Y ) ) = ( X .\/ ( Y ./\ ( ._|_ ` X ) ) ) )
18 17 eqeq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y = ( X .\/ ( ( ._|_ ` X ) ./\ Y ) ) <-> Y = ( X .\/ ( Y ./\ ( ._|_ ` X ) ) ) ) )
19 7 18 bitrid 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X .\/ ( ( ._|_ ` X ) ./\ Y ) ) = Y <-> Y = ( X .\/ ( Y ./\ ( ._|_ ` X ) ) ) ) )
20 6 19 sylibrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( X .\/ ( ( ._|_ ` X ) ./\ Y ) ) = Y ) )