Metamath Proof Explorer


Theorem hlexchb1

Description: A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011)

Ref Expression
Hypotheses hlsuprexch.b B = Base K
hlsuprexch.l ˙ = K
hlsuprexch.j ˙ = join K
hlsuprexch.a A = Atoms K
Assertion hlexchb1 K HL P A Q A X B ¬ P ˙ X P ˙ X ˙ Q X ˙ P = X ˙ Q

Proof

Step Hyp Ref Expression
1 hlsuprexch.b B = Base K
2 hlsuprexch.l ˙ = K
3 hlsuprexch.j ˙ = join K
4 hlsuprexch.a A = Atoms K
5 hlcvl K HL K CvLat
6 1 2 3 4 cvlexchb1 K CvLat P A Q A X B ¬ P ˙ X P ˙ X ˙ Q X ˙ P = X ˙ Q
7 5 6 syl3an1 K HL P A Q A X B ¬ P ˙ X P ˙ X ˙ Q X ˙ P = X ˙ Q