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	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 ) )