Metamath Proof Explorer


Theorem cvrp

Description: A Hilbert lattice satisfies the covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 18-Nov-2011)

Ref Expression
Hypotheses cvrp.b B=BaseK
cvrp.j ˙=joinK
cvrp.m ˙=meetK
cvrp.z 0˙=0.K
cvrp.c C=K
cvrp.a A=AtomsK
Assertion cvrp KHLXBPAX˙P=0˙XCX˙P

Proof

Step Hyp Ref Expression
1 cvrp.b B=BaseK
2 cvrp.j ˙=joinK
3 cvrp.m ˙=meetK
4 cvrp.z 0˙=0.K
5 cvrp.c C=K
6 cvrp.a A=AtomsK
7 hlomcmcv KHLKOMLKCLatKCvLat
8 1 2 3 4 5 6 cvlcvrp KOMLKCLatKCvLatXBPAX˙P=0˙XCX˙P
9 7 8 syl3an1 KHLXBPAX˙P=0˙XCX˙P