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

Metamath Proof Explorer

Theorem cvlexch1

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

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

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 iscvlat 
 |-  ( K e. CvLat <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
6 5 simprbi 
 |-  ( K e. CvLat -> A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) )
7 breq1 
 |-  ( p = P -> ( p .<_ x <-> P .<_ x ) )
8 7 notbid 
 |-  ( p = P -> ( -. p .<_ x <-> -. P .<_ x ) )
9 breq1 
 |-  ( p = P -> ( p .<_ ( x .\/ q ) <-> P .<_ ( x .\/ q ) ) )
10 8 9 anbi12d 
 |-  ( p = P -> ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) <-> ( -. P .<_ x /\ P .<_ ( x .\/ q ) ) ) )
11 oveq2 
 |-  ( p = P -> ( x .\/ p ) = ( x .\/ P ) )
12 11 breq2d 
 |-  ( p = P -> ( q .<_ ( x .\/ p ) <-> q .<_ ( x .\/ P ) ) )
13 10 12 imbi12d 
 |-  ( p = P -> ( ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) <-> ( ( -. P .<_ x /\ P .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ P ) ) ) )
14 oveq2 
 |-  ( q = Q -> ( x .\/ q ) = ( x .\/ Q ) )
15 14 breq2d 
 |-  ( q = Q -> ( P .<_ ( x .\/ q ) <-> P .<_ ( x .\/ Q ) ) )
16 15 anbi2d 
 |-  ( q = Q -> ( ( -. P .<_ x /\ P .<_ ( x .\/ q ) ) <-> ( -. P .<_ x /\ P .<_ ( x .\/ Q ) ) ) )
17 breq1 
 |-  ( q = Q -> ( q .<_ ( x .\/ P ) <-> Q .<_ ( x .\/ P ) ) )
18 16 17 imbi12d 
 |-  ( q = Q -> ( ( ( -. P .<_ x /\ P .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ P ) ) <-> ( ( -. P .<_ x /\ P .<_ ( x .\/ Q ) ) -> Q .<_ ( x .\/ P ) ) ) )
19 breq2 
 |-  ( x = X -> ( P .<_ x <-> P .<_ X ) )
20 19 notbid 
 |-  ( x = X -> ( -. P .<_ x <-> -. P .<_ X ) )
21 oveq1 
 |-  ( x = X -> ( x .\/ Q ) = ( X .\/ Q ) )
22 21 breq2d 
 |-  ( x = X -> ( P .<_ ( x .\/ Q ) <-> P .<_ ( X .\/ Q ) ) )
23 20 22 anbi12d 
 |-  ( x = X -> ( ( -. P .<_ x /\ P .<_ ( x .\/ Q ) ) <-> ( -. P .<_ X /\ P .<_ ( X .\/ Q ) ) ) )
24 oveq1 
 |-  ( x = X -> ( x .\/ P ) = ( X .\/ P ) )
25 24 breq2d 
 |-  ( x = X -> ( Q .<_ ( x .\/ P ) <-> Q .<_ ( X .\/ P ) ) )
26 23 25 imbi12d 
 |-  ( x = X -> ( ( ( -. P .<_ x /\ P .<_ ( x .\/ Q ) ) -> Q .<_ ( x .\/ P ) ) <-> ( ( -. P .<_ X /\ P .<_ ( X .\/ Q ) ) -> Q .<_ ( X .\/ P ) ) ) )
27 13 18 26 rspc3v 
 |-  ( ( P e. A /\ Q e. A /\ X e. B ) -> ( A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) -> ( ( -. P .<_ X /\ P .<_ ( X .\/ Q ) ) -> Q .<_ ( X .\/ P ) ) ) )
28 6 27 mpan9 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( ( -. P .<_ X /\ P .<_ ( X .\/ Q ) ) -> Q .<_ ( X .\/ P ) ) )
29 28 exp4b 
 |-  ( K e. CvLat -> ( ( P e. A /\ Q e. A /\ X e. B ) -> ( -. P .<_ X -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) ) ) )
30 29 3imp 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) )