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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrp.j	⊢ ∨ = ( join ‘ 𝐾 )
	cvrp.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cvrp.z	⊢ 0 = ( 0. ‘ 𝐾 )
	cvrp.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	cvrp.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	cvrp	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 0 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cvrp.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvrp.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cvrp.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cvrp.z	⊢ 0 = ( 0. ‘ 𝐾 )
5		cvrp.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
6		cvrp.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7		hlomcmcv	⊢ ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) )
8	1 2 3 4 5 6	cvlcvrp	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 0 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )
9	7 8	syl3an1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 0 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )