Metamath Proof Explorer


Theorem hlexchb2

Description: A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012)

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

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 cvlexchb2 K CvLat P A Q A X B ¬ P ˙ X P ˙ Q ˙ X P ˙ X = Q ˙ X
7 5 6 syl3an1 K HL P A Q A X B ¬ P ˙ X P ˙ Q ˙ X P ˙ X = Q ˙ X