cvlatcvr1

Description: An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	cvlatcvr1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvlatcvr1.c	$⊢ C = ⋖_{K}$
	cvlatcvr1.a	$⊢ A = Atoms (K)$
Assertion	cvlatcvr1	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P C (P \underset{˙}{\lor} Q))$

Step	Hyp	Ref	Expression
1		cvlatcvr1.j	$⊢ \underset{˙}{\lor} = join (K)$
2		cvlatcvr1.c	$⊢ C = ⋖_{K}$
3		cvlatcvr1.a	$⊢ A = Atoms (K)$
4		simp13	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to K \in CvLat$
5		cvlatl	$⊢ K \in CvLat \to K \in AtLat$
6	4 5	syl	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to K \in AtLat$
7		eqid	$⊢ meet (K) = meet (K)$
8		eqid	$⊢ 0. (K) = 0. (K)$
9	7 8 3	atnem0	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P meet (K) Q = 0. (K))$
10	6 9	syld3an1	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P meet (K) Q = 0. (K))$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
13	11 1 7 8 2 3	cvlcvrp	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in {Base}_{K} \land Q \in A) \to (P meet (K) Q = 0. (K) \leftrightarrow P C (P \underset{˙}{\lor} Q))$
14	12 13	syl3an2	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to (P meet (K) Q = 0. (K) \leftrightarrow P C (P \underset{˙}{\lor} Q))$
15	10 14	bitrd	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P C (P \underset{˙}{\lor} Q))$

Metamath Proof Explorer