lhpj1

Description: The join of a co-atom (hyperplane) and an element not under it is the lattice unity. (Contributed by NM, 7-Dec-2012)

	Ref	Expression
Hypotheses	lhpj1.b	$⊢ B = {Base}_{K}$
	lhpj1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhpj1.j	$⊢ \underset{˙}{\lor} = join (K)$
	lhpj1.u	$⊢ \underset{˙}{1} = 1. (K)$
	lhpj1.h	$⊢ H = LHyp (K)$
Assertion	lhpj1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} X = \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		lhpj1.b	$⊢ B = {Base}_{K}$
2		lhpj1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lhpj1.j	$⊢ \underset{˙}{\lor} = join (K)$
4		lhpj1.u	$⊢ \underset{˙}{1} = 1. (K)$
5		lhpj1.h	$⊢ H = LHyp (K)$
6		simpll	$⊢ ((K \in HL \land W \in H) \land X \in B) \to K \in HL$
7		simpr	$⊢ ((K \in HL \land W \in H) \land X \in B) \to X \in B$
8	1 5	lhpbase	$⊢ W \in H \to W \in B$
9	8	ad2antlr	$⊢ ((K \in HL \land W \in H) \land X \in B) \to W \in B$
10		eqid	$⊢ Atoms (K) = Atoms (K)$
11	1 2 10	hlrelat2	$⊢ (K \in HL \land X \in B \land W \in B) \to (\neg X \underset{˙}{\leq} W \leftrightarrow \exists p \in Atoms (K) (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W))$
12	6 7 9 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \in B) \to (\neg X \underset{˙}{\leq} W \leftrightarrow \exists p \in Atoms (K) (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W))$
13		simp1l	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
14		simp2	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to p \in Atoms (K)$
15		simp3r	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to \neg p \underset{˙}{\leq} W$
16	2 3 4 10 5	lhpjat1	$⊢ ((K \in HL \land W \in H) \land (p \in Atoms (K) \land \neg p \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} p = \underset{˙}{1}$
17	13 14 15 16	syl12anc	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} p = \underset{˙}{1}$
18		simp3l	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to p \underset{˙}{\leq} X$
19		simp1ll	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to K \in HL$
20	19	hllatd	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to K \in Lat$
21	1 10	atbase	$⊢ p \in Atoms (K) \to p \in B$
22	21	3ad2ant2	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to p \in B$
23		simp1r	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to X \in B$
24	9	3ad2ant1	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to W \in B$
25	1 2 3	latjlej2	$⊢ (K \in Lat \land (p \in B \land X \in B \land W \in B)) \to (p \underset{˙}{\leq} X \to (W \underset{˙}{\lor} p) \underset{˙}{\leq} (W \underset{˙}{\lor} X))$
26	20 22 23 24 25	syl13anc	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to (p \underset{˙}{\leq} X \to (W \underset{˙}{\lor} p) \underset{˙}{\leq} (W \underset{˙}{\lor} X))$
27	18 26	mpd	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to (W \underset{˙}{\lor} p) \underset{˙}{\leq} (W \underset{˙}{\lor} X)$
28	17 27	eqbrtrrd	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to \underset{˙}{1} \underset{˙}{\leq} (W \underset{˙}{\lor} X)$
29		hlop	$⊢ K \in HL \to K \in OP$
30	19 29	syl	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to K \in OP$
31	1 3	latjcl	$⊢ (K \in Lat \land W \in B \land X \in B) \to W \underset{˙}{\lor} X \in B$
32	20 24 23 31	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} X \in B$
33	1 2 4	op1le	$⊢ (K \in OP \land W \underset{˙}{\lor} X \in B) \to (\underset{˙}{1} \underset{˙}{\leq} (W \underset{˙}{\lor} X) \leftrightarrow W \underset{˙}{\lor} X = \underset{˙}{1})$
34	30 32 33	syl2anc	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to (\underset{˙}{1} \underset{˙}{\leq} (W \underset{˙}{\lor} X) \leftrightarrow W \underset{˙}{\lor} X = \underset{˙}{1})$
35	28 34	mpbid	$⊢ (((K \in HL \land W \in H) \land X \in B) \land p \in Atoms (K) \land (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} X = \underset{˙}{1}$
36	35	rexlimdv3a	$⊢ ((K \in HL \land W \in H) \land X \in B) \to (\exists p \in Atoms (K) (p \underset{˙}{\leq} X \land \neg p \underset{˙}{\leq} W) \to W \underset{˙}{\lor} X = \underset{˙}{1})$
37	12 36	sylbid	$⊢ ((K \in HL \land W \in H) \land X \in B) \to (\neg X \underset{˙}{\leq} W \to W \underset{˙}{\lor} X = \underset{˙}{1})$
38	37	impr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} X = \underset{˙}{1}$

Metamath Proof Explorer

Theorem lhpj1

Proof