Theorem cvlexch4N

Description: An atomic covering lattice has the exchange property. Part of Definition 7.8 of MaedaMaeda p. 32. (Contributed by NM, 5-Nov-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cvlexch3.b	|- B = ( Base ` K )
2		cvlexch3.l	|- .<_ = ( le ` K )
3		cvlexch3.j	|- .\/ = ( join ` K )
4		cvlexch3.m	|- ./\ = ( meet ` K )
5		cvlexch3.z	|- .0. = ( 0. ` K )
6		cvlexch3.a	|- A = ( Atoms ` K )
7		cvlatl	|- ( K e. CvLat -> K e. AtLat )
8	7	adantr	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> K e. AtLat )
9		simpr1	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> P e. A )
10		simpr3	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> X e. B )
11	1 2 4 5 6	atnle	|- ( ( K e. AtLat /\ P e. A /\ X e. B ) -> ( -. P .<_ X <-> ( P ./\ X ) = .0. ) )
12	8 9 10 11	syl3anc	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( -. P .<_ X <-> ( P ./\ X ) = .0. ) )
13	1 2 3 6	cvlexchb1	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )
14	13	3expia	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( -. P .<_ X -> ( P .<_ ( X .\/ Q ) <-> ( X .\/ P ) = ( X .\/ Q ) ) ) )
15	12 14	sylbird	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( ( P ./\ X ) = .0. -> ( P .<_ ( X .\/ Q ) <-> ( X .\/ P ) = ( X .\/ Q ) ) ) )
16	15	3impia	|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P ./\ X ) = .0. ) -> ( P .<_ ( X .\/ Q ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )