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 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 atelch ⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ )
2 chincl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Cℋ )
3 1 2 sylan2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ∩ 𝐵 ) ∈ Cℋ )
4 atcveq0 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )
5 3 4 sylancom ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) )
6 cvexch ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
7 1 6 sylan2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
8 5 7 bitr3d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )