Theorem hlsupr

Description: A Hilbert lattice has the superposition property. Theorem 13.2 in Crawley p. 107. (Contributed by NM, 30-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		hlsupr.l	|- .<_ = ( le ` K )
2		hlsupr.j	|- .\/ = ( join ` K )
3		hlsupr.a	|- A = ( Atoms ` K )
4		eqid	|- ( Base ` K ) = ( Base ` K )
5	4 1 2 3	hlsuprexch	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( P =/= Q -> E. r e. A ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) /\ A. r e. ( Base ` K ) ( ( -. P .<_ r /\ P .<_ ( r .\/ Q ) ) -> Q .<_ ( r .\/ P ) ) ) )
6	5	simpld	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P =/= Q -> E. r e. A ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) ) )
7	6	imp	|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> E. r e. A ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) )