atcvrj2b

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	atcvrj2b	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow 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		simpl3l	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to Q \neq R$
6	5	necomd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to R \neq Q$
7		simpl1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to K \in HL$
8		simpl23	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to R \in A$
9		simpl22	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to Q \in A$
10	2 3 4	atcvr2	$⊢ (K \in HL \land R \in A \land Q \in A) \to (R \neq Q \leftrightarrow R C (Q \underset{˙}{\lor} R))$
11	7 8 9 10	syl3anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to (R \neq Q \leftrightarrow R C (Q \underset{˙}{\lor} R))$
12	6 11	mpbid	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to R C (Q \underset{˙}{\lor} R)$
13		breq1	$⊢ P = R \to (P C (Q \underset{˙}{\lor} R) \leftrightarrow R C (Q \underset{˙}{\lor} R))$
14	13	adantl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to (P C (Q \underset{˙}{\lor} R) \leftrightarrow R C (Q \underset{˙}{\lor} R))$
15	12 14	mpbird	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P = R) \to P C (Q \underset{˙}{\lor} R)$
16		simpl1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P \neq R) \to K \in HL$
17		simpl2	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P \neq R) \to (P \in A \land Q \in A \land R \in A)$
18		simpr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P \neq R) \to P \neq R$
19		simpl3r	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P \neq R) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
20	1 2 3 4	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)$
21	16 17 18 19 20	syl112anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \land P \neq R) \to P C (Q \underset{˙}{\lor} R)$
22	15 21	pm2.61dane	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P C (Q \underset{˙}{\lor} R)$
23	22	3expia	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to P C (Q \underset{˙}{\lor} R))$
24		hlatl	$⊢ K \in HL \to K \in AtLat$
25	24	ad2antrr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to K \in AtLat$
26		simplr1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to P \in A$
27		eqid	$⊢ 0. (K) = 0. (K)$
28	27 4	atn0	$⊢ (K \in AtLat \land P \in A) \to P \neq 0. (K)$
29	25 26 28	syl2anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to P \neq 0. (K)$
30		simpll	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to K \in HL$
31		eqid	$⊢ {Base}_{K} = {Base}_{K}$
32	31 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
33	26 32	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to P \in {Base}_{K}$
34		simplr2	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to Q \in A$
35		simplr3	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to R \in A$
36		simpr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to P C (Q \underset{˙}{\lor} R)$
37	31 2 27 3 4	atcvrj0	$⊢ (K \in HL \land (P \in {Base}_{K} \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to (P = 0. (K) \leftrightarrow Q = R)$
38	30 33 34 35 36 37	syl131anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to (P = 0. (K) \leftrightarrow Q = R)$
39	38	necon3bid	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to (P \neq 0. (K) \leftrightarrow Q \neq R)$
40	29 39	mpbid	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to Q \neq R$
41		hllat	$⊢ K \in HL \to K \in Lat$
42	41	ad2antrr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to K \in Lat$
43	31 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
44	34 43	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to Q \in {Base}_{K}$
45	31 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
46	35 45	syl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to R \in {Base}_{K}$
47	31 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
48	42 44 46 47	syl3anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
49	30 33 48	3jca	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to (K \in HL \land P \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})$
50	31 1 3	cvrle	$⊢ ((K \in HL \land P \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land P C (Q \underset{˙}{\lor} R)) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
51	49 50	sylancom	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
52	40 51	jca	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land P C (Q \underset{˙}{\lor} R)) \to (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
53	52	ex	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P C (Q \underset{˙}{\lor} R) \to (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
54	23 53	impbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow P C (Q \underset{˙}{\lor} R))$

Metamath Proof Explorer

Theorem atcvrj2b

Proof