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

Metamath Proof Explorer

Theorem cvr1

Description: A Hilbert lattice has the covering property. Proposition 1(ii) in Kalmbach p. 140 (and its converse). ( chcv1 analog.) (Contributed by NM, 17-Nov-2011)

		Ref	Expression
	Hypotheses	cvr1.b	$⊢ B = {Base}_{K}$
		cvr1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		cvr1.j	$⊢ \underset{˙}{\lor} = join (K)$
		cvr1.c	$⊢ C = ⋖_{K}$
		cvr1.a	$⊢ A = Atoms (K)$
	Assertion	cvr1	$⊢ (K \in HL \land X \in B \land P \in A) \to (\neg P \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} P))$

Proof

Step	Hyp	Ref	Expression
1		cvr1.b	$⊢ B = {Base}_{K}$
2		cvr1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvr1.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cvr1.c	$⊢ C = ⋖_{K}$
5		cvr1.a	$⊢ A = Atoms (K)$
6		hlomcmcv	$⊢ K \in HL \to (K \in OML \land K \in CLat \land K \in CvLat)$
7	1 2 3 4 5	cvlcvr1	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to (\neg P \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} P))$
8	6 7	syl3an1	$⊢ (K \in HL \land X \in B \land P \in A) \to (\neg P \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} P))$