2atjm

Description: The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012)

	Ref	Expression
Hypotheses	2atjm.b	$⊢ B = {Base}_{K}$
	2atjm.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2atjm.j	$⊢ \underset{˙}{\lor} = join (K)$
	2atjm.m	$⊢ \underset{˙}{\land} = meet (K)$
	2atjm.a	$⊢ A = Atoms (K)$
Assertion	2atjm	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X = P$

Proof

Step	Hyp	Ref	Expression
1		2atjm.b	$⊢ B = {Base}_{K}$
2		2atjm.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		2atjm.j	$⊢ \underset{˙}{\lor} = join (K)$
4		2atjm.m	$⊢ \underset{˙}{\land} = meet (K)$
5		2atjm.a	$⊢ A = Atoms (K)$
6		hllat	$⊢ K \in HL \to K \in Lat$
7	6	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to K \in Lat$
8		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \in A$
9	1 5	atbase	$⊢ P \in A \to P \in B$
10	8 9	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \in B$
11		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to Q \in A$
12	1 5	atbase	$⊢ Q \in A \to Q \in B$
13	11 12	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to Q \in B$
14	1 2 3	latlej1	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
15	7 10 13 14	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
16		simp3l	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \underset{˙}{\leq} X$
17		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to K \in HL$
18	1 3 5	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in B$
19	17 8 11 18	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \underset{˙}{\lor} Q \in B$
20		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to X \in B$
21	1 2 4	latlem12	$⊢ (K \in Lat \land (P \in B \land P \underset{˙}{\lor} Q \in B \land X \in B)) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} X) \leftrightarrow P \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} X))$
22	7 10 19 20 21	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} X) \leftrightarrow P \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} X))$
23	15 16 22	mpbi2and	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} X)$
24		hlatl	$⊢ K \in HL \to K \in AtLat$
25	24	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to K \in AtLat$
26	1 4	latmcom	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in B \land X \in B) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X = X \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
27	7 19 20 26	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X = X \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
28	20 8 11	3jca	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (X \in B \land P \in A \land Q \in A)$
29		nbrne2	$⊢ (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X) \to P \neq Q$
30	29	3ad2ant3	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \neq Q$
31		simp3r	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \neg Q \underset{˙}{\leq} X$
32	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Q \in B) \to X \underset{˙}{\lor} Q \in B$
33	7 20 13 32	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to X \underset{˙}{\lor} Q \in B$
34	1 2 3	latlej1	$⊢ (K \in Lat \land X \in B \land Q \in B) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
35	7 20 13 34	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
36	1 2 7 10 20 33 16 35	lattrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
37	1 2 3 4 5	cvrat3	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((P \neq Q \land \neg Q \underset{˙}{\leq} X \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A)$
38	37	imp	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land (P \neq Q \land \neg Q \underset{˙}{\leq} X \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to X \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A$
39	17 28 30 31 36 38	syl23anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to X \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A$
40	27 39	eqeltrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X \in A$
41	2 5	atcmp	$⊢ (K \in AtLat \land P \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} X \in A) \to (P \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} X) \leftrightarrow P = (P \underset{˙}{\lor} Q) \underset{˙}{\land} X)$
42	25 8 40 41	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (P \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} X) \leftrightarrow P = (P \underset{˙}{\lor} Q) \underset{˙}{\land} X)$
43	23 42	mpbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P = (P \underset{˙}{\lor} Q) \underset{˙}{\land} X$
44	43	eqcomd	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X = P$

Metamath Proof Explorer

Theorem 2atjm

Proof