cvrat2

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. ( atcvat2i analog.) (Contributed by NM, 30-Nov-2011)

	Ref	Expression
Hypotheses	cvrat2.b	$⊢ B = {Base}_{K}$
	cvrat2.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvrat2.c	$⊢ C = ⋖_{K}$
	cvrat2.a	$⊢ A = Atoms (K)$
Assertion	cvrat2	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land (P \neq Q \land X C (P \underset{˙}{\lor} Q))) \to X \in A$

Proof

Step	Hyp	Ref	Expression
1		cvrat2.b	$⊢ B = {Base}_{K}$
2		cvrat2.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cvrat2.c	$⊢ C = ⋖_{K}$
4		cvrat2.a	$⊢ A = Atoms (K)$
5		eqid	$⊢ 0. (K) = 0. (K)$
6	1 2 5 3 4	atcvrj0	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land X C (P \underset{˙}{\lor} Q)) \to (X = 0. (K) \leftrightarrow P = Q)$
7	6	3expa	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land X C (P \underset{˙}{\lor} Q)) \to (X = 0. (K) \leftrightarrow P = Q)$
8	7	necon3bid	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land X C (P \underset{˙}{\lor} Q)) \to (X \neq 0. (K) \leftrightarrow P \neq Q)$
9		simpl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in HL$
10		simpr1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to X \in B$
11		hllat	$⊢ K \in HL \to K \in Lat$
12	11	adantr	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in Lat$
13		simpr2	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \in A$
14	1 4	atbase	$⊢ P \in A \to P \in B$
15	13 14	syl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \in B$
16		simpr3	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q \in A$
17	1 4	atbase	$⊢ Q \in A \to Q \in B$
18	16 17	syl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q \in B$
19	1 2	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q \in B$
20	12 15 18 19	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \underset{˙}{\lor} Q \in B$
21		eqid	$⊢ <_{K} = <_{K}$
22	1 21 3	cvrlt	$⊢ ((K \in HL \land X \in B \land P \underset{˙}{\lor} Q \in B) \land X C (P \underset{˙}{\lor} Q)) \to X <_{K} (P \underset{˙}{\lor} Q)$
23	22	ex	$⊢ (K \in HL \land X \in B \land P \underset{˙}{\lor} Q \in B) \to (X C (P \underset{˙}{\lor} Q) \to X <_{K} (P \underset{˙}{\lor} Q))$
24	9 10 20 23	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C (P \underset{˙}{\lor} Q) \to X <_{K} (P \underset{˙}{\lor} Q))$
25	1 21 2 5 4	cvrat	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X \neq 0. (K) \land X <_{K} (P \underset{˙}{\lor} Q)) \to X \in A)$
26	25	expcomd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X <_{K} (P \underset{˙}{\lor} Q) \to (X \neq 0. (K) \to X \in A))$
27	24 26	syld	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C (P \underset{˙}{\lor} Q) \to (X \neq 0. (K) \to X \in A))$
28	27	imp	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land X C (P \underset{˙}{\lor} Q)) \to (X \neq 0. (K) \to X \in A)$
29	8 28	sylbird	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land X C (P \underset{˙}{\lor} Q)) \to (P \neq Q \to X \in A)$
30	29	ex	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C (P \underset{˙}{\lor} Q) \to (P \neq Q \to X \in A))$
31	30	com23	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (P \neq Q \to (X C (P \underset{˙}{\lor} Q) \to X \in A))$
32	31	impd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((P \neq Q \land X C (P \underset{˙}{\lor} Q)) \to X \in A)$
33	32	3impia	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land (P \neq Q \land X C (P \underset{˙}{\lor} Q))) \to X \in A$

Metamath Proof Explorer

Theorem cvrat2

Proof