Metamath Proof Explorer


Theorem hlexch4N

Description: A Hilbert lattice has the exchange property. Part of Definition 7.8 of MaedaMaeda p. 32. (Contributed by NM, 15-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses hlexch3.b B = Base K
hlexch3.l ˙ = K
hlexch3.j ˙ = join K
hlexch3.m ˙ = meet K
hlexch3.z 0 ˙ = 0. K
hlexch3.a A = Atoms K
Assertion hlexch4N K HL P A Q A X B P ˙ X = 0 ˙ P ˙ X ˙ Q X ˙ P = X ˙ Q

Proof

Step Hyp Ref Expression
1 hlexch3.b B = Base K
2 hlexch3.l ˙ = K
3 hlexch3.j ˙ = join K
4 hlexch3.m ˙ = meet K
5 hlexch3.z 0 ˙ = 0. K
6 hlexch3.a A = Atoms K
7 hlcvl K HL K CvLat
8 1 2 3 4 5 6 cvlexch4N K CvLat P A Q A X B P ˙ X = 0 ˙ P ˙ X ˙ Q X ˙ P = X ˙ Q
9 7 8 syl3an1 K HL P A Q A X B P ˙ X = 0 ˙ P ˙ X ˙ Q X ˙ P = X ˙ Q