This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvlexch2

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012)

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

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 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 ) ) )
6 cvllat 
 |-  ( K e. CvLat -> K e. Lat )
7 6 3ad2ant1 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> K e. Lat )
8 simp22 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> 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 ) /\ -. P .<_ X ) -> Q e. B )
11 simp23 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> X e. B )
12 1 3 latjcom 
 |-  ( ( K e. Lat /\ Q e. B /\ X e. B ) -> ( Q .\/ X ) = ( X .\/ Q ) )
13 7 10 11 12 syl3anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( Q .\/ X ) = ( X .\/ Q ) )
14 13 breq2d 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( Q .\/ X ) <-> P .<_ ( X .\/ Q ) ) )
15 simp21 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> P e. A )
16 1 4 atbase 
 |-  ( P e. A -> P e. B )
17 15 16 syl 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> P e. B )
18 1 3 latjcom 
 |-  ( ( K e. Lat /\ P e. B /\ X e. B ) -> ( P .\/ X ) = ( X .\/ P ) )
19 7 17 11 18 syl3anc 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .\/ X ) = ( X .\/ P ) )
20 19 breq2d 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( Q .<_ ( P .\/ X ) <-> Q .<_ ( X .\/ P ) ) )
21 5 14 20 3imtr4d 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( Q .\/ X ) -> Q .<_ ( P .\/ X ) ) )