2atm2atN

Description: Two joins with a common atom have a nonzero meet. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2atm2at.j	$⊢ \underset{˙}{\lor} = join (K)$
	2atm2at.m	$⊢ \underset{˙}{\land} = meet (K)$
	2atm2at.z	$⊢ \underset{˙}{0} = 0. (K)$
	2atm2at.a	$⊢ A = Atoms (K)$
Assertion	2atm2atN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		2atm2at.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2atm2at.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2atm2at.z	$⊢ \underset{˙}{0} = 0. (K)$
4		2atm2at.a	$⊢ A = Atoms (K)$
5		hlop	$⊢ K \in HL \to K \in OP$
6	5	adantr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in OP$
7		simpr3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in A$
8		eqid	$⊢ <_{K} = <_{K}$
9	3 8 4	0ltat	$⊢ (K \in OP \land R \in A) \to \underset{˙}{0} <_{K} R$
10	6 7 9	syl2anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to \underset{˙}{0} <_{K} R$
11		simpl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in HL$
12		simpr1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \in A$
13		eqid	$⊢ \leq_{K} = \leq_{K}$
14	13 1 4	hlatlej1	$⊢ (K \in HL \land R \in A \land P \in A) \to R \leq_{K} (R \underset{˙}{\lor} P)$
15	11 7 12 14	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \leq_{K} (R \underset{˙}{\lor} P)$
16		simpr2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to Q \in A$
17	13 1 4	hlatlej1	$⊢ (K \in HL \land R \in A \land Q \in A) \to R \leq_{K} (R \underset{˙}{\lor} Q)$
18	11 7 16 17	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \leq_{K} (R \underset{˙}{\lor} Q)$
19		hllat	$⊢ K \in HL \to K \in Lat$
20	19	adantr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in Lat$
21		eqid	$⊢ {Base}_{K} = {Base}_{K}$
22	21 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
23	7 22	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in {Base}_{K}$
24	21 1 4	hlatjcl	$⊢ (K \in HL \land R \in A \land P \in A) \to R \underset{˙}{\lor} P \in {Base}_{K}$
25	11 7 12 24	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \underset{˙}{\lor} P \in {Base}_{K}$
26	21 1 4	hlatjcl	$⊢ (K \in HL \land R \in A \land Q \in A) \to R \underset{˙}{\lor} Q \in {Base}_{K}$
27	11 7 16 26	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \underset{˙}{\lor} Q \in {Base}_{K}$
28	21 13 2	latlem12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land R \underset{˙}{\lor} P \in {Base}_{K} \land R \underset{˙}{\lor} Q \in {Base}_{K})) \to ((R \leq_{K} (R \underset{˙}{\lor} P) \land R \leq_{K} (R \underset{˙}{\lor} Q)) \leftrightarrow R \leq_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q)))$
29	20 23 25 27 28	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((R \leq_{K} (R \underset{˙}{\lor} P) \land R \leq_{K} (R \underset{˙}{\lor} Q)) \leftrightarrow R \leq_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q)))$
30	15 18 29	mpbi2and	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \leq_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q))$
31		hlpos	$⊢ K \in HL \to K \in Poset$
32	31	adantr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in Poset$
33	21 3	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in {Base}_{K}$
34	6 33	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to \underset{˙}{0} \in {Base}_{K}$
35	21 2	latmcl	$⊢ (K \in Lat \land R \underset{˙}{\lor} P \in {Base}_{K} \land R \underset{˙}{\lor} Q \in {Base}_{K}) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) \in {Base}_{K}$
36	20 25 27 35	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) \in {Base}_{K}$
37	21 13 8	pltletr	$⊢ (K \in Poset \land (\underset{˙}{0} \in {Base}_{K} \land R \in {Base}_{K} \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) \in {Base}_{K})) \to ((\underset{˙}{0} <_{K} R \land R \leq_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q))) \to \underset{˙}{0} <_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q)))$
38	32 34 23 36 37	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((\underset{˙}{0} <_{K} R \land R \leq_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q))) \to \underset{˙}{0} <_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q)))$
39	10 30 38	mp2and	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to \underset{˙}{0} <_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q))$
40	21 8 3	opltn0	$⊢ (K \in OP \land (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) \in {Base}_{K}) \to (\underset{˙}{0} <_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q)) \leftrightarrow (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) \neq \underset{˙}{0})$
41	6 36 40	syl2anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (\underset{˙}{0} <_{K} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q)) \leftrightarrow (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) \neq \underset{˙}{0})$
42	39 41	mpbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem 2atm2atN

Proof