Metamath Proof Explorer


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 ˙=K
hlsupr.j ˙=joinK
hlsupr.a A=AtomsK
Assertion hlsupr KHLPAQAPQrArPrQr˙P˙Q

Proof

Step Hyp Ref Expression
1 hlsupr.l ˙=K
2 hlsupr.j ˙=joinK
3 hlsupr.a A=AtomsK
4 eqid BaseK=BaseK
5 4 1 2 3 hlsuprexch KHLPAQAPQrArPrQr˙P˙QrBaseK¬P˙rP˙r˙QQ˙r˙P
6 5 simpld KHLPAQAPQrArPrQr˙P˙Q
7 6 imp KHLPAQAPQrArPrQr˙P˙Q