2atm

Description: An atom majorized by two different atom joins (which could be atoms or lines) is equal to their intersection. (Contributed by NM, 30-Jun-2013)

	Ref	Expression
Hypotheses	2atm.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2atm.j	$⊢ \underset{˙}{\lor} = join (K)$
	2atm.m	$⊢ \underset{˙}{\land} = meet (K)$
	2atm.a	$⊢ A = Atoms (K)$
Assertion	2atm	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to T = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S)$

Proof

Step	Hyp	Ref	Expression
1		2atm.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2atm.j	$⊢ \underset{˙}{\lor} = join (K)$
3		2atm.m	$⊢ \underset{˙}{\land} = meet (K)$
4		2atm.a	$⊢ A = Atoms (K)$
5		simp31	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
6		simp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to T \underset{˙}{\leq} (R \underset{˙}{\lor} S)$
7		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to K \in Lat$
9		simp23	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to T \in A$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 4	atbase	$⊢ T \in A \to T \in {Base}_{K}$
12	9 11	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to T \in {Base}_{K}$
13		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to P \in A$
14	10 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
15	13 14	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to P \in {Base}_{K}$
16		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to Q \in A$
17	10 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
18	16 17	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to Q \in {Base}_{K}$
19	10 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
20	8 15 18 19	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
21		simp21	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to R \in A$
22		simp22	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to S \in A$
23	10 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
24	7 21 22 23	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to R \underset{˙}{\lor} S \in {Base}_{K}$
25	10 1 3	latlem12	$⊢ (K \in Lat \land (T \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K})) \to ((T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S)) \leftrightarrow T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S)))$
26	8 12 20 24 25	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S)) \leftrightarrow T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S)))$
27	5 6 26	mpbi2and	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S))$
28		hlatl	$⊢ K \in HL \to K \in AtLat$
29	7 28	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to K \in AtLat$
30	10 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in {Base}_{K}$
31	8 20 24 30	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in {Base}_{K}$
32		eqid	$⊢ 0. (K) = 0. (K)$
33	10 1 32 4	atlen0	$⊢ ((K \in AtLat \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in {Base}_{K} \land T \in A) \land T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq 0. (K)$
34	29 31 9 27 33	syl31anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq 0. (K)$
35	34	neneqd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to \neg (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = 0. (K)$
36		simp33	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S$
37	2 3 32 4	2atmat0	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = 0. (K))$
38	7 13 16 21 22 36 37	syl33anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = 0. (K))$
39	38	ord	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (\neg (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = 0. (K))$
40	35 39	mt3d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A$
41	1 4	atcmp	$⊢ (K \in AtLat \land T \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A) \to (T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S)) \leftrightarrow T = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S))$
42	29 9 40 41	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S)) \leftrightarrow T = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S))$
43	27 42	mpbid	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to T = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S)$

Metamath Proof Explorer

Theorem 2atm

Proof