atle

Description: Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		atle.b	$⊢ B = {Base}_{K}$
2		atle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atle.z	$⊢ \underset{˙}{0} = 0. (K)$
4		atle.a	$⊢ A = Atoms (K)$
5		simp1	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to K \in HL$
6		hlop	$⊢ K \in HL \to K \in OP$
7	6	3ad2ant1	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to K \in OP$
8	1 3	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in B$
9	7 8	syl	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to \underset{˙}{0} \in B$
10		simp2	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to X \in B$
11		simp3	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to X \neq \underset{˙}{0}$
12		eqid	$⊢ <_{K} = <_{K}$
13	1 12 3	opltn0	$⊢ (K \in OP \land X \in B) \to (\underset{˙}{0} <_{K} X \leftrightarrow X \neq \underset{˙}{0})$
14	7 10 13	syl2anc	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to (\underset{˙}{0} <_{K} X \leftrightarrow X \neq \underset{˙}{0})$
15	11 14	mpbird	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to \underset{˙}{0} <_{K} X$
16		eqid	$⊢ join (K) = join (K)$
17	1 2 12 16 4	hlrelat	$⊢ ((K \in HL \land \underset{˙}{0} \in B \land X \in B) \land \underset{˙}{0} <_{K} X) \to \exists p \in A (\underset{˙}{0} <_{K} (\underset{˙}{0} join (K) p) \land (\underset{˙}{0} join (K) p) \underset{˙}{\leq} X)$
18	5 9 10 15 17	syl31anc	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to \exists p \in A (\underset{˙}{0} <_{K} (\underset{˙}{0} join (K) p) \land (\underset{˙}{0} join (K) p) \underset{˙}{\leq} X)$
19		simpl1	$⊢ ((K \in HL \land X \in B \land X \neq \underset{˙}{0}) \land p \in A) \to K \in HL$
20		hlol	$⊢ K \in HL \to K \in OL$
21	19 20	syl	$⊢ ((K \in HL \land X \in B \land X \neq \underset{˙}{0}) \land p \in A) \to K \in OL$
22	1 4	atbase	$⊢ p \in A \to p \in B$
23	22	adantl	$⊢ ((K \in HL \land X \in B \land X \neq \underset{˙}{0}) \land p \in A) \to p \in B$
24	1 16 3	olj02	$⊢ (K \in OL \land p \in B) \to \underset{˙}{0} join (K) p = p$
25	21 23 24	syl2anc	$⊢ ((K \in HL \land X \in B \land X \neq \underset{˙}{0}) \land p \in A) \to \underset{˙}{0} join (K) p = p$
26	25	breq1d	$⊢ ((K \in HL \land X \in B \land X \neq \underset{˙}{0}) \land p \in A) \to ((\underset{˙}{0} join (K) p) \underset{˙}{\leq} X \leftrightarrow p \underset{˙}{\leq} X)$
27	26	biimpd	$⊢ ((K \in HL \land X \in B \land X \neq \underset{˙}{0}) \land p \in A) \to ((\underset{˙}{0} join (K) p) \underset{˙}{\leq} X \to p \underset{˙}{\leq} X)$
28	27	adantld	$⊢ ((K \in HL \land X \in B \land X \neq \underset{˙}{0}) \land p \in A) \to ((\underset{˙}{0} <_{K} (\underset{˙}{0} join (K) p) \land (\underset{˙}{0} join (K) p) \underset{˙}{\leq} X) \to p \underset{˙}{\leq} X)$
29	28	reximdva	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to (\exists p \in A (\underset{˙}{0} <_{K} (\underset{˙}{0} join (K) p) \land (\underset{˙}{0} join (K) p) \underset{˙}{\leq} X) \to \exists p \in A p \underset{˙}{\leq} X)$
30	18 29	mpd	$⊢ (K \in HL \land X \in B \land X \neq \underset{˙}{0}) \to \exists p \in A p \underset{˙}{\leq} X$

Metamath Proof Explorer

Theorem atle

Proof