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

Metamath Proof Explorer

Theorem hlsuprexch

Description: A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 hlsuprexch.b 
 |-  B = ( Base ` K )
2 hlsuprexch.l 
 |-  .<_ = ( le ` K )
3 hlsuprexch.j 
 |-  .\/ = ( join ` K )
4 hlsuprexch.a 
 |-  A = ( Atoms ` K )
5 eqid 
 |-  ( lt ` K ) = ( lt ` K )
6 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
7 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
8 1 2 5 3 6 7 4 ishlat2 
 |-  ( K e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ ( A. x e. A A. y e. A ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) ) )
9 simprl 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ ( A. x e. A A. y e. A ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) ) -> A. x e. A A. y e. A ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) ) )
10 8 9 sylbi 
 |-  ( K e. HL -> A. x e. A A. y e. A ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) ) )
11 neeq1 
 |-  ( x = P -> ( x =/= y <-> P =/= y ) )
12 neeq2 
 |-  ( x = P -> ( z =/= x <-> z =/= P ) )
13 oveq1 
 |-  ( x = P -> ( x .\/ y ) = ( P .\/ y ) )
14 13 breq2d 
 |-  ( x = P -> ( z .<_ ( x .\/ y ) <-> z .<_ ( P .\/ y ) ) )
15 12 14 3anbi13d 
 |-  ( x = P -> ( ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) <-> ( z =/= P /\ z =/= y /\ z .<_ ( P .\/ y ) ) ) )
16 15 rexbidv 
 |-  ( x = P -> ( E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) <-> E. z e. A ( z =/= P /\ z =/= y /\ z .<_ ( P .\/ y ) ) ) )
17 11 16 imbi12d 
 |-  ( x = P -> ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) <-> ( P =/= y -> E. z e. A ( z =/= P /\ z =/= y /\ z .<_ ( P .\/ y ) ) ) ) )
18 breq1 
 |-  ( x = P -> ( x .<_ z <-> P .<_ z ) )
19 18 notbid 
 |-  ( x = P -> ( -. x .<_ z <-> -. P .<_ z ) )
20 breq1 
 |-  ( x = P -> ( x .<_ ( z .\/ y ) <-> P .<_ ( z .\/ y ) ) )
21 19 20 anbi12d 
 |-  ( x = P -> ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) <-> ( -. P .<_ z /\ P .<_ ( z .\/ y ) ) ) )
22 oveq2 
 |-  ( x = P -> ( z .\/ x ) = ( z .\/ P ) )
23 22 breq2d 
 |-  ( x = P -> ( y .<_ ( z .\/ x ) <-> y .<_ ( z .\/ P ) ) )
24 21 23 imbi12d 
 |-  ( x = P -> ( ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) <-> ( ( -. P .<_ z /\ P .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ P ) ) ) )
25 24 ralbidv 
 |-  ( x = P -> ( A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) <-> A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ P ) ) ) )
26 17 25 anbi12d 
 |-  ( x = P -> ( ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) ) <-> ( ( P =/= y -> E. z e. A ( z =/= P /\ z =/= y /\ z .<_ ( P .\/ y ) ) ) /\ A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ P ) ) ) ) )
27 neeq2 
 |-  ( y = Q -> ( P =/= y <-> P =/= Q ) )
28 neeq2 
 |-  ( y = Q -> ( z =/= y <-> z =/= Q ) )
29 oveq2 
 |-  ( y = Q -> ( P .\/ y ) = ( P .\/ Q ) )
30 29 breq2d 
 |-  ( y = Q -> ( z .<_ ( P .\/ y ) <-> z .<_ ( P .\/ Q ) ) )
31 28 30 3anbi23d 
 |-  ( y = Q -> ( ( z =/= P /\ z =/= y /\ z .<_ ( P .\/ y ) ) <-> ( z =/= P /\ z =/= Q /\ z .<_ ( P .\/ Q ) ) ) )
32 31 rexbidv 
 |-  ( y = Q -> ( E. z e. A ( z =/= P /\ z =/= y /\ z .<_ ( P .\/ y ) ) <-> E. z e. A ( z =/= P /\ z =/= Q /\ z .<_ ( P .\/ Q ) ) ) )
33 27 32 imbi12d 
 |-  ( y = Q -> ( ( P =/= y -> E. z e. A ( z =/= P /\ z =/= y /\ z .<_ ( P .\/ y ) ) ) <-> ( P =/= Q -> E. z e. A ( z =/= P /\ z =/= Q /\ z .<_ ( P .\/ Q ) ) ) ) )
34 oveq2 
 |-  ( y = Q -> ( z .\/ y ) = ( z .\/ Q ) )
35 34 breq2d 
 |-  ( y = Q -> ( P .<_ ( z .\/ y ) <-> P .<_ ( z .\/ Q ) ) )
36 35 anbi2d 
 |-  ( y = Q -> ( ( -. P .<_ z /\ P .<_ ( z .\/ y ) ) <-> ( -. P .<_ z /\ P .<_ ( z .\/ Q ) ) ) )
37 breq1 
 |-  ( y = Q -> ( y .<_ ( z .\/ P ) <-> Q .<_ ( z .\/ P ) ) )
38 36 37 imbi12d 
 |-  ( y = Q -> ( ( ( -. P .<_ z /\ P .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ P ) ) <-> ( ( -. P .<_ z /\ P .<_ ( z .\/ Q ) ) -> Q .<_ ( z .\/ P ) ) ) )
39 38 ralbidv 
 |-  ( y = Q -> ( A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ P ) ) <-> A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ Q ) ) -> Q .<_ ( z .\/ P ) ) ) )
40 33 39 anbi12d 
 |-  ( y = Q -> ( ( ( P =/= y -> E. z e. A ( z =/= P /\ z =/= y /\ z .<_ ( P .\/ y ) ) ) /\ A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ P ) ) ) <-> ( ( P =/= Q -> E. z e. A ( z =/= P /\ z =/= Q /\ z .<_ ( P .\/ Q ) ) ) /\ A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ Q ) ) -> Q .<_ ( z .\/ P ) ) ) ) )
41 26 40 rspc2v 
 |-  ( ( P e. A /\ Q e. A ) -> ( A. x e. A A. y e. A ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) ) -> ( ( P =/= Q -> E. z e. A ( z =/= P /\ z =/= Q /\ z .<_ ( P .\/ Q ) ) ) /\ A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ Q ) ) -> Q .<_ ( z .\/ P ) ) ) ) )
42 10 41 mpan9 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A ) ) -> ( ( P =/= Q -> E. z e. A ( z =/= P /\ z =/= Q /\ z .<_ ( P .\/ Q ) ) ) /\ A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ Q ) ) -> Q .<_ ( z .\/ P ) ) ) )
43 42 3impb 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( P =/= Q -> E. z e. A ( z =/= P /\ z =/= Q /\ z .<_ ( P .\/ Q ) ) ) /\ A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ Q ) ) -> Q .<_ ( z .\/ P ) ) ) )