atcvrj1

Description: Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012)

	Ref	Expression
Hypotheses	atcvrj1x.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atcvrj1x.j	$⊢ \underset{˙}{\lor} = join (K)$
	atcvrj1x.c	$⊢ C = ⋖_{K}$
	atcvrj1x.a	$⊢ A = Atoms (K)$
Assertion	atcvrj1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P C (Q \underset{˙}{\lor} R)$

Proof

Step	Hyp	Ref	Expression
1		atcvrj1x.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		atcvrj1x.j	$⊢ \underset{˙}{\lor} = join (K)$
3		atcvrj1x.c	$⊢ C = ⋖_{K}$
4		atcvrj1x.a	$⊢ A = Atoms (K)$
5		simp3l	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P \neq R$
6		hlatl	$⊢ K \in HL \to K \in AtLat$
7	6	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to K \in AtLat$
8		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P \in A$
9		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to R \in A$
10		eqid	$⊢ meet (K) = meet (K)$
11		eqid	$⊢ 0. (K) = 0. (K)$
12	10 11 4	atnem0	$⊢ (K \in AtLat \land P \in A \land R \in A) \to (P \neq R \leftrightarrow P meet (K) R = 0. (K))$
13	7 8 9 12	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (P \neq R \leftrightarrow P meet (K) R = 0. (K))$
14	5 13	mpbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P meet (K) R = 0. (K)$
15		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to K \in HL$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17	16 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
18	8 17	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P \in {Base}_{K}$
19	16 2 10 11 3 4	cvrp	$⊢ (K \in HL \land P \in {Base}_{K} \land R \in A) \to (P meet (K) R = 0. (K) \leftrightarrow P C (P \underset{˙}{\lor} R))$
20	15 18 9 19	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (P meet (K) R = 0. (K) \leftrightarrow P C (P \underset{˙}{\lor} R))$
21	14 20	mpbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P C (P \underset{˙}{\lor} R)$
22		simp3r	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
23	1 2 4	hlatexchb2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
24	23	3adant3r	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
25	22 24	mpbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
26	21 25	breqtrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P C (Q \underset{˙}{\lor} R)$

Metamath Proof Explorer

Theorem atcvrj1

Proof