Theorem omllaw5N

Description: The orthomodular law. Remark in Kalmbach p. 22. ( pjoml5 analog.) (Contributed by NM, 14-Nov-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		omllaw5.b	|- B = ( Base ` K )
2		omllaw5.j	|- .\/ = ( join ` K )
3		omllaw5.m	|- ./\ = ( meet ` K )
4		omllaw5.o	|- ._|_ = ( oc ` K )
5		simp1	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OML )
6		simp2	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )
7		omllat	|- ( K e. OML -> K e. Lat )
8	1 2	latjcl	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
9	7 8	syl3an1	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
10	5 6 9	3jca	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( K e. OML /\ X e. B /\ ( X .\/ Y ) e. B ) )
11		eqid	|- ( le ` K ) = ( le ` K )
12	1 11 2	latlej1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X ( le ` K ) ( X .\/ Y ) )
13	7 12	syl3an1	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> X ( le ` K ) ( X .\/ Y ) )
14	1 11 2 3 4	omllaw2N	|- ( ( K e. OML /\ X e. B /\ ( X .\/ Y ) e. B ) -> ( X ( le ` K ) ( X .\/ Y ) -> ( X .\/ ( ( ._|_ ` X ) ./\ ( X .\/ Y ) ) ) = ( X .\/ Y ) ) )
15	10 13 14	sylc	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .\/ ( ( ._|_ ` X ) ./\ ( X .\/ Y ) ) ) = ( X .\/ Y ) )