cvrat

Description: A nonzero Hilbert lattice element less than the join of two atoms is an atom. ( atcvati analog.) (Contributed by NM, 22-Nov-2011)

	Ref	Expression
Hypotheses	cvrat.b	$⊢ B = {Base}_{K}$
	cvrat.s	$⊢ \underset{˙}{<} = <_{K}$
	cvrat.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvrat.z	$⊢ \underset{˙}{0} = 0. (K)$
	cvrat.a	$⊢ A = Atoms (K)$
Assertion	cvrat	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q)) \to X \in A)$

Proof

Step	Hyp	Ref	Expression
1		cvrat.b	$⊢ B = {Base}_{K}$
2		cvrat.s	$⊢ \underset{˙}{<} = <_{K}$
3		cvrat.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cvrat.z	$⊢ \underset{˙}{0} = 0. (K)$
5		cvrat.a	$⊢ A = Atoms (K)$
6	1 2 3 4 5	cvratlem	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land (X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to (\neg P \leq_{K} X \to X \in A)$
7		hllat	$⊢ K \in HL \to K \in Lat$
8	7	adantr	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in Lat$
9		simpr2	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \in A$
10	1 5	atbase	$⊢ P \in A \to P \in B$
11	9 10	syl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \in B$
12		simpr3	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q \in A$
13	1 5	atbase	$⊢ Q \in A \to Q \in B$
14	12 13	syl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q \in B$
15	1 3	latjcom	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
16	8 11 14 15	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
17	16	breq2d	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \leftrightarrow X \underset{˙}{<} (Q \underset{˙}{\lor} P))$
18	17	anbi2d	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q)) \leftrightarrow (X \neq \underset{˙}{0} \land X \underset{˙}{<} (Q \underset{˙}{\lor} P)))$
19		simpl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in HL$
20		simpr1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to X \in B$
21	1 2 3 4 5	cvratlem	$⊢ ((K \in HL \land (X \in B \land Q \in A \land P \in A)) \land (X \neq \underset{˙}{0} \land X \underset{˙}{<} (Q \underset{˙}{\lor} P))) \to (\neg Q \leq_{K} X \to X \in A)$
22	21	ex	$⊢ (K \in HL \land (X \in B \land Q \in A \land P \in A)) \to ((X \neq \underset{˙}{0} \land X \underset{˙}{<} (Q \underset{˙}{\lor} P)) \to (\neg Q \leq_{K} X \to X \in A))$
23	19 20 12 9 22	syl13anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X \neq \underset{˙}{0} \land X \underset{˙}{<} (Q \underset{˙}{\lor} P)) \to (\neg Q \leq_{K} X \to X \in A))$
24	18 23	sylbid	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q)) \to (\neg Q \leq_{K} X \to X \in A))$
25	24	imp	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land (X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to (\neg Q \leq_{K} X \to X \in A)$
26		hlpos	$⊢ K \in HL \to K \in Poset$
27	26	adantr	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in Poset$
28	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q \in B$
29	8 11 14 28	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \underset{˙}{\lor} Q \in B$
30		eqid	$⊢ \leq_{K} = \leq_{K}$
31	1 30 2	pltnle	$⊢ ((K \in Poset \land X \in B \land P \underset{˙}{\lor} Q \in B) \land X \underset{˙}{<} (P \underset{˙}{\lor} Q)) \to \neg (P \underset{˙}{\lor} Q) \leq_{K} X$
32	31	ex	$⊢ (K \in Poset \land X \in B \land P \underset{˙}{\lor} Q \in B) \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to \neg (P \underset{˙}{\lor} Q) \leq_{K} X)$
33	27 20 29 32	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to \neg (P \underset{˙}{\lor} Q) \leq_{K} X)$
34	1 30 3	latjle12	$⊢ (K \in Lat \land (P \in B \land Q \in B \land X \in B)) \to ((P \leq_{K} X \land Q \leq_{K} X) \leftrightarrow (P \underset{˙}{\lor} Q) \leq_{K} X)$
35	8 11 14 20 34	syl13anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((P \leq_{K} X \land Q \leq_{K} X) \leftrightarrow (P \underset{˙}{\lor} Q) \leq_{K} X)$
36	35	biimpd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((P \leq_{K} X \land Q \leq_{K} X) \to (P \underset{˙}{\lor} Q) \leq_{K} X)$
37	33 36	nsyld	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to \neg (P \leq_{K} X \land Q \leq_{K} X))$
38		ianor	$⊢ \neg (P \leq_{K} X \land Q \leq_{K} X) \leftrightarrow (\neg P \leq_{K} X \lor \neg Q \leq_{K} X)$
39	37 38	syl6ib	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to (\neg P \leq_{K} X \lor \neg Q \leq_{K} X))$
40	39	imp	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land X \underset{˙}{<} (P \underset{˙}{\lor} Q)) \to (\neg P \leq_{K} X \lor \neg Q \leq_{K} X)$
41	40	adantrl	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land (X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to (\neg P \leq_{K} X \lor \neg Q \leq_{K} X)$
42	6 25 41	mpjaod	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land (X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to X \in A$
43	42	ex	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q)) \to X \in A)$

Metamath Proof Explorer

Theorem cvrat

Proof