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 ) ) ) )