llnle

Description: Any element greater than 0 and not an atom majorizes a lattice line. (Contributed by NM, 28-Jun-2012)

	Ref	Expression
Hypotheses	llnle.b	$⊢ B = {Base}_{K}$
	llnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	llnle.z	$⊢ \underset{˙}{0} = 0. (K)$
	llnle.a	$⊢ A = Atoms (K)$
	llnle.n	$⊢ N = LLines (K)$
Assertion	llnle	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to \exists y \in N y \underset{˙}{\leq} X$

Proof

Step	Hyp	Ref	Expression
1		llnle.b	$⊢ B = {Base}_{K}$
2		llnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		llnle.z	$⊢ \underset{˙}{0} = 0. (K)$
4		llnle.a	$⊢ A = Atoms (K)$
5		llnle.n	$⊢ N = LLines (K)$
6		simpll	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to K \in HL$
7		simplr	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to X \in B$
8		simprl	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to X \neq \underset{˙}{0}$
9	1 2 3 4	atle	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to \exists p \in A p \underset{˙}{\leq} X$
10	6 7 8 9	syl3anc	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to \exists p \in A p \underset{˙}{\leq} X$
11		simp1ll	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to K \in HL$
12	1 4	atbase	$⊢ p \in A \to p \in B$
13	12	3ad2ant2	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to p \in B$
14		simp1lr	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to X \in B$
15		simp3	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to p \underset{˙}{\leq} X$
16		simp2	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to p \in A$
17		simp1rr	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to \neg X \in A$
18		nelne2	$⊢ (p \in A \land \neg X \in A) \to p \neq X$
19	16 17 18	syl2anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to p \neq X$
20		eqid	$⊢ <_{K} = <_{K}$
21	2 20	pltval	$⊢ (K \in HL \land p \in A \land X \in B) \to (p <_{K} X \leftrightarrow (p \underset{˙}{\leq} X \land p \neq X))$
22	11 16 14 21	syl3anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to (p <_{K} X \leftrightarrow (p \underset{˙}{\leq} X \land p \neq X))$
23	15 19 22	mpbir2and	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to p <_{K} X$
24		eqid	$⊢ join (K) = join (K)$
25		eqid	$⊢ ⋖_{K} = ⋖_{K}$
26	1 2 20 24 25 4	hlrelat3	$⊢ ((K \in HL \land p \in B \land X \in B) \land p <_{K} X) \to \exists q \in A (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)$
27	11 13 14 23 26	syl31anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to \exists q \in A (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)$
28		simp1ll	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land (p \in A \land p \underset{˙}{\leq} X \land q \in A) \land (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)) \to K \in HL$
29		simp21	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land (p \in A \land p \underset{˙}{\leq} X \land q \in A) \land (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)) \to p \in A$
30		simp23	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land (p \in A \land p \underset{˙}{\leq} X \land q \in A) \land (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)) \to q \in A$
31	1 24 4	hlatjcl	$⊢ (K \in HL \land p \in A \land q \in A) \to p join (K) q \in B$
32	28 29 30 31	syl3anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land (p \in A \land p \underset{˙}{\leq} X \land q \in A) \land (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)) \to p join (K) q \in B$
33		simp3l	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land (p \in A \land p \underset{˙}{\leq} X \land q \in A) \land (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)) \to p ⋖_{K} (p join (K) q)$
34	1 25 4 5	llni	$⊢ ((K \in HL \land p join (K) q \in B \land p \in A) \land p ⋖_{K} (p join (K) q)) \to p join (K) q \in N$
35	28 32 29 33 34	syl31anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land (p \in A \land p \underset{˙}{\leq} X \land q \in A) \land (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)) \to p join (K) q \in N$
36		simp3r	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land (p \in A \land p \underset{˙}{\leq} X \land q \in A) \land (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)) \to (p join (K) q) \underset{˙}{\leq} X$
37		breq1	$⊢ y = p join (K) q \to (y \underset{˙}{\leq} X \leftrightarrow (p join (K) q) \underset{˙}{\leq} X)$
38	37	rspcev	$⊢ (p join (K) q \in N \land (p join (K) q) \underset{˙}{\leq} X) \to \exists y \in N y \underset{˙}{\leq} X$
39	35 36 38	syl2anc	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land (p \in A \land p \underset{˙}{\leq} X \land q \in A) \land (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X)) \to \exists y \in N y \underset{˙}{\leq} X$
40	39	3exp	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to ((p \in A \land p \underset{˙}{\leq} X \land q \in A) \to ((p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X) \to \exists y \in N y \underset{˙}{\leq} X))$
41	40	3expd	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to (p \in A \to (p \underset{˙}{\leq} X \to (q \in A \to ((p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X) \to \exists y \in N y \underset{˙}{\leq} X))))$
42	41	3imp	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to (q \in A \to ((p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X) \to \exists y \in N y \underset{˙}{\leq} X))$
43	42	rexlimdv	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to (\exists q \in A (p ⋖_{K} (p join (K) q) \land (p join (K) q) \underset{˙}{\leq} X) \to \exists y \in N y \underset{˙}{\leq} X)$
44	27 43	mpd	$⊢ (((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \land p \in A \land p \underset{˙}{\leq} X) \to \exists y \in N y \underset{˙}{\leq} X$
45	44	3exp	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to (p \in A \to (p \underset{˙}{\leq} X \to \exists y \in N y \underset{˙}{\leq} X))$
46	45	rexlimdv	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to (\exists p \in A p \underset{˙}{\leq} X \to \exists y \in N y \underset{˙}{\leq} X)$
47	10 46	mpd	$⊢ ((K \in HL \land X \in B) \land (X \neq \underset{˙}{0} \land \neg X \in A)) \to \exists y \in N y \underset{˙}{\leq} X$

Metamath Proof Explorer

Theorem llnle

Proof