Metamath Proof Explorer

Theorem cvlexchb1

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 cvlexch.b 
 |-  B = ( Base ` K )
2 cvlexch.l 
 |-  .<_ = ( le ` K )
3 cvlexch.j 
 |-  .\/ = ( join ` K )
4 cvlexch.a 
 |-  A = ( Atoms ` K )
5 cvllat 
 |-  ( K e. CvLat -> K e. Lat )
6 5 adantr 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> K e. Lat )
7 simpr3 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> X e. B )
8 simpr2 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> Q e. A )
9 1 4 atbase 
 |-  ( Q e. A -> Q e. B )
10 8 9 syl 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> Q e. B )
11 1 2 3 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ Q e. B ) -> X .<_ ( X .\/ Q ) )
12 6 7 10 11 syl3anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> X .<_ ( X .\/ Q ) )
13 12 3adant3 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> X .<_ ( X .\/ Q ) )
14 13 adantr 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> X .<_ ( X .\/ Q ) )
15 simpr 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> P .<_ ( X .\/ Q ) )
16 simpr1 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> P e. A )
17 1 4 atbase 
 |-  ( P e. A -> P e. B )
18 16 17 syl 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> P e. B )
19 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Q e. B ) -> ( X .\/ Q ) e. B )
20 6 7 10 19 syl3anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( X .\/ Q ) e. B )
21 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( X e. B /\ P e. B /\ ( X .\/ Q ) e. B ) ) -> ( ( X .<_ ( X .\/ Q ) /\ P .<_ ( X .\/ Q ) ) <-> ( X .\/ P ) .<_ ( X .\/ Q ) ) )
22 6 7 18 20 21 syl13anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( ( X .<_ ( X .\/ Q ) /\ P .<_ ( X .\/ Q ) ) <-> ( X .\/ P ) .<_ ( X .\/ Q ) ) )
23 22 3adant3 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( ( X .<_ ( X .\/ Q ) /\ P .<_ ( X .\/ Q ) ) <-> ( X .\/ P ) .<_ ( X .\/ Q ) ) )
24 23 adantr 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> ( ( X .<_ ( X .\/ Q ) /\ P .<_ ( X .\/ Q ) ) <-> ( X .\/ P ) .<_ ( X .\/ Q ) ) )
25 14 15 24 mpbi2and 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> ( X .\/ P ) .<_ ( X .\/ Q ) )
26 1 2 3 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> X .<_ ( X .\/ P ) )
27 6 7 18 26 syl3anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> X .<_ ( X .\/ P ) )
28 27 3adant3 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> X .<_ ( X .\/ P ) )
29 28 adantr 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> X .<_ ( X .\/ P ) )
30 1 2 3 4 cvlexch1 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) )
31 30 imp 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> Q .<_ ( X .\/ P ) )
32 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( X .\/ P ) e. B )
33 6 7 18 32 syl3anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( X .\/ P ) e. B )
34 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( X e. B /\ Q e. B /\ ( X .\/ P ) e. B ) ) -> ( ( X .<_ ( X .\/ P ) /\ Q .<_ ( X .\/ P ) ) <-> ( X .\/ Q ) .<_ ( X .\/ P ) ) )
35 6 7 10 33 34 syl13anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( ( X .<_ ( X .\/ P ) /\ Q .<_ ( X .\/ P ) ) <-> ( X .\/ Q ) .<_ ( X .\/ P ) ) )
36 35 3adant3 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( ( X .<_ ( X .\/ P ) /\ Q .<_ ( X .\/ P ) ) <-> ( X .\/ Q ) .<_ ( X .\/ P ) ) )
37 36 adantr 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> ( ( X .<_ ( X .\/ P ) /\ Q .<_ ( X .\/ P ) ) <-> ( X .\/ Q ) .<_ ( X .\/ P ) ) )
38 29 31 37 mpbi2and 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> ( X .\/ Q ) .<_ ( X .\/ P ) )
39 1 2 latasymb 
 |-  ( ( K e. Lat /\ ( X .\/ P ) e. B /\ ( X .\/ Q ) e. B ) -> ( ( ( X .\/ P ) .<_ ( X .\/ Q ) /\ ( X .\/ Q ) .<_ ( X .\/ P ) ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )
40 6 33 20 39 syl3anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( ( ( X .\/ P ) .<_ ( X .\/ Q ) /\ ( X .\/ Q ) .<_ ( X .\/ P ) ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )
41 40 3adant3 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( ( ( X .\/ P ) .<_ ( X .\/ Q ) /\ ( X .\/ Q ) .<_ ( X .\/ P ) ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )
42 41 adantr 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> ( ( ( X .\/ P ) .<_ ( X .\/ Q ) /\ ( X .\/ Q ) .<_ ( X .\/ P ) ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )
43 25 38 42 mpbi2and 
 |-  ( ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) /\ P .<_ ( X .\/ Q ) ) -> ( X .\/ P ) = ( X .\/ Q ) )
44 43 ex 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) -> ( X .\/ P ) = ( X .\/ Q ) ) )
45 1 2 3 latlej2 
 |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> P .<_ ( X .\/ P ) )
46 6 7 18 45 syl3anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> P .<_ ( X .\/ P ) )
47 breq2 
 |-  ( ( X .\/ P ) = ( X .\/ Q ) -> ( P .<_ ( X .\/ P ) <-> P .<_ ( X .\/ Q ) ) )
48 46 47 syl5ibcom 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( ( X .\/ P ) = ( X .\/ Q ) -> P .<_ ( X .\/ Q ) ) )
49 48 3adant3 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( ( X .\/ P ) = ( X .\/ Q ) -> P .<_ ( X .\/ Q ) ) )
50 44 49 impbid 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )