Theorem hlexch3

Description: A Hilbert lattice has the exchange property. ( atexch analog.) (Contributed by NM, 15-Nov-2011)

	Ref	Expression
Hypotheses	hlexch3.b	|- B = ( Base ` K )
	hlexch3.l	|- .<_ = ( le ` K )
	hlexch3.j	|- .\/ = ( join ` K )
	hlexch3.m	|- ./\ = ( meet ` K )
	hlexch3.z	|- .0. = ( 0. ` K )
	hlexch3.a	|- A = ( Atoms ` K )
Assertion	hlexch3	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P ./\ X ) = .0. ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) )

Proof

Step	Hyp	Ref	Expression
1		hlexch3.b	|- B = ( Base ` K )
2		hlexch3.l	|- .<_ = ( le ` K )
3		hlexch3.j	|- .\/ = ( join ` K )
4		hlexch3.m	|- ./\ = ( meet ` K )
5		hlexch3.z	|- .0. = ( 0. ` K )
6		hlexch3.a	|- A = ( Atoms ` K )
7		hlcvl	|- ( K e. HL -> K e. CvLat )
8	1 2 3 4 5 6	cvlexch3	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P ./\ X ) = .0. ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) )
9	7 8	syl3an1	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P ./\ X ) = .0. ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) )