This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvp

Description: The Hilbert lattice satisfies the covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvp 
|- ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A

Proof

Step Hyp Ref Expression
1 atelch 
 |-  ( B e. HAtoms -> B e. CH )
2 chincl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A i^i B ) e. CH )
3 1 2 sylan2 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( A i^i B ) e. CH )
4 atcveq0 
 |-  ( ( ( A i^i B ) e. CH /\ B e. HAtoms ) -> ( ( A i^i B )  ( A i^i B ) = 0H ) )
5 3 4 sylancom 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B )  ( A i^i B ) = 0H ) )
6 cvexch 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( A i^i B )  A
7 1 6 sylan2 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B )  A
8 5 7 bitr3d 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A