cvlcvrp

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

	Ref	Expression
Hypotheses	cvlcvrp.b	$⊢ B = {Base}_{K}$
	cvlcvrp.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvlcvrp.m	$⊢ \underset{˙}{\land} = meet (K)$
	cvlcvrp.z	$⊢ \underset{˙}{0} = 0. (K)$
	cvlcvrp.c	$⊢ C = ⋖_{K}$
	cvlcvrp.a	$⊢ A = Atoms (K)$
Assertion	cvlcvrp	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to (X \underset{˙}{\land} P = \underset{˙}{0} \leftrightarrow X C (X \underset{˙}{\lor} P))$

Proof

Step	Hyp	Ref	Expression
1		cvlcvrp.b	$⊢ B = {Base}_{K}$
2		cvlcvrp.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cvlcvrp.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cvlcvrp.z	$⊢ \underset{˙}{0} = 0. (K)$
5		cvlcvrp.c	$⊢ C = ⋖_{K}$
6		cvlcvrp.a	$⊢ A = Atoms (K)$
7		simp13	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to K \in CvLat$
8		cvllat	$⊢ K \in CvLat \to K \in Lat$
9	7 8	syl	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to K \in Lat$
10		simp2	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to X \in B$
11	1 6	atbase	$⊢ P \in A \to P \in B$
12	11	3ad2ant3	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to P \in B$
13	1 3	latmcom	$⊢ (K \in Lat \land X \in B \land P \in B) \to X \underset{˙}{\land} P = P \underset{˙}{\land} X$
14	9 10 12 13	syl3anc	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to X \underset{˙}{\land} P = P \underset{˙}{\land} X$
15	14	eqeq1d	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to (X \underset{˙}{\land} P = \underset{˙}{0} \leftrightarrow P \underset{˙}{\land} X = \underset{˙}{0})$
16		cvlatl	$⊢ K \in CvLat \to K \in AtLat$
17	7 16	syl	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to K \in AtLat$
18		simp3	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to P \in A$
19		eqid	$⊢ \leq_{K} = \leq_{K}$
20	1 19 3 4 6	atnle	$⊢ (K \in AtLat \land P \in A \land X \in B) \to (\neg P \leq_{K} X \leftrightarrow P \underset{˙}{\land} X = \underset{˙}{0})$
21	17 18 10 20	syl3anc	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to (\neg P \leq_{K} X \leftrightarrow P \underset{˙}{\land} X = \underset{˙}{0})$
22	1 19 2 5 6	cvlcvr1	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to (\neg P \leq_{K} X \leftrightarrow X C (X \underset{˙}{\lor} P))$
23	15 21 22	3bitr2d	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to (X \underset{˙}{\land} P = \underset{˙}{0} \leftrightarrow X C (X \underset{˙}{\lor} P))$

Metamath Proof Explorer

Theorem cvlcvrp

Proof