# 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 syl5bb
` |-  ( ( 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 ) )`